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

[Philip Wadler]

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.

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. 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>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
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220103/973dd24c/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Substitution-fixed.lagda.md
Type: text/markdown
Size: 4552 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220103/973dd24c/attachment-0002.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Substitution-broken.lagda.md
Type: text/markdown
Size: 3945 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220103/973dd24c/attachment-0003.bin>