[Agda] A stupid question to start off the New Year

[James Wood]

Hi Phil,

The error message you see on the pattern-match of the with more or less 
says that you should be using rewrite instead of with. exts is not 
(obviously) injective, so the unifier will give up when trying to unify 
it with anything other than a variable. The unification problem was 
triggered by the pattern-match to refl, which tries to unify the two 
equated terms (exts `_ and `_). rewrite solves the problem by 
with-abstracting the LHS (exts `_), turning it into a fresh variable 
that gets unified with the RHS (`_). It looks like this is what you 
wanted. The documentation for rewrite 
(https://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite) 
gives another example.

Kind regards,

James

On 03/01/2022 19:20, Philip Wadler wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> Thanks, Conor! As usual, that was blindingly fast!
>
> 2. Your elegant, and elegantly named, solution that bypasses 
> extensionality works brilliantly. Attached as 
> Substitution-fixed.lagda.md <http://substitution-fixed.lagda.md/>.
>
> 1. I did my best to make explicit all of the implicit variables in 
> extensionality, but it still complains. Attached as 
> Substitution-broken.lagda.md <http://substitution-broken.lagda.md/>. 
> Any idea of what is wrong or how to fix it? I've been stymied by 
> similar errors several times over the last few days, so I'm keen to 
> have a better understanding.
>
> Go well, -- P
>
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
>
> On Mon, 3 Jan 2022 at 16:36, Conor McBride 
> <conor at strictlypositive.org> wrote:
>
>     This email was sent to you by someone outside the University.
>     You should only click on links or attachments if you are certain
>     that the email is genuine and the content is safe.
>
>     Hi Phil
>
>     > On 3 Jan 2022, at 16:24, Philip Wadler <wadler at inf.ed.ac.uk> wrote:
>     >
>     > I'm trying to prove a basic fact about substitution and failing.
>     What I'd like to prove is that substitution by the identity map is
>     the identity, which should be straightforward. My failed proof is
>     attached. Questions:
>     >
>     > 1. Why does Agda complain about my extensionality postulate? How
>     do I fix it?
>
>     For a start, Agda's moaning about the implicits that it can't
>     infer in your with-expression.
>     No type is pushed in to with-expressions, so there's nothing that
>     will determing the
>     missing information. I'm not sure with is what you need, but even
>     if you were to use
>     rewrite, the same would pertain. However...
>
>     > 2. Is there a way to complete the proof without assuming
>     extensionality?
>
>     ...you might consider making Henry Ford's extensional
>     generalization of your goal. Any
>     substitution will *behave* as the identity on terms if it
>     *behaves* like the identity on
>     variables, regardless of whether it's your *favourite* identity
>     substitution. That statement
>     pushes readily under lambda, because it talks about "any
>     substitution", leaving you with
>     an "as long as it behaves like the identity" condition to discharge.
>
>     Cheers
>
>     Conor
>
>     >
>     > Many thanks for your help. This group is invaluable! The New
>     Year is a good time to take a moment to express my thanks to you
>     all, both for your work in Agda (and related topics) and for your
>     help.
>     >
>     > Go well, -- P
>     >
>     >
>     >
>     >
>     > .   \ Philip Wadler, Professor of Theoretical Computer Science,
>     > .   /\ School of Informatics, University of Edinburgh
>     > .  /  \ and Senior Research Fellow, IOHK
>     > . http://homepages.inf.ed.ac.uk/wadler/
>     >
>     > <Substitution.lagda.md <http://substitution.lagda.md/>>The
>     University of Edinburgh is a charitable body, registered in
>     > Scotland, with registration number SC005336.
>     > _______________________________________________
>     > Agda mailing list
>     > Agda at lists.chalmers.se
>     > https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220104/0d1f7b7e/attachment.html>