<div dir="ltr">Thanks, James. Indeed, changing "with" to "rewrite" fixed that problem. Ironic, since the previous time I wrote to the list the fix was to change "rewrite" to "with", which is why I was using "with"!<div><br></div><div>1. Can you give me an intuition about when "with" is appropriate and when "rewrite" is appropriate? I could not work this out from reading the docs.<br><div><br></div><div>2, The rewrite does not have the desired effect of changing (subst (ext ids)) to (subst ids). See the revised file below. Any idea of how to complete the proof?</div><div><br></div><div>Thank you again! Go well, -- P</div><div><br clear="all"><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 4 Jan 2022 at 15:42, James Wood <<a href="mailto:james.wood.100@strath.ac.uk">james.wood.100@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<div style="background-color:rgb(255,242,230);border:2px dotted rgb(255,136,77)"><span style="font-size:12pt;font-family:sans-serif;color:black;font-weight:bold;padding:0.2em">This email was sent to you by someone outside the University.</span>
<div style="font-size:10pt;font-family:sans-serif;font-style:normal;padding:0.2em">
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.</div>
</div>
<div>Hi Phil,<br>
<p>The error message you see on the pattern-match of the <font face="monospace">with</font> more or less says that you should be using
<font face="monospace">rewrite</font> instead of <font face="monospace">with</font>.
<font face="monospace">exts</font> 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
<font face="monospace">refl</font>, which tries to unify the two equated terms (<font face="monospace">exts `_</font> and
<font face="monospace">`_</font>). <font face="monospace">rewrite</font> solves the problem by
<font face="monospace">with</font>-abstracting the LHS (<font face="monospace">exts `_</font>), turning it into a fresh variable that gets unified with the RHS (<font face="monospace">`_</font>). It looks like this is what you wanted. The documentation for
<font face="monospace">rewrite</font> (<a href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite" target="_blank">https://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite</a>)
gives another example.<br>
</p>
<p>Kind regards,</p>
<p>James<br>
</p>
<div>On 03/01/2022 19:20, Philip Wadler wrote:<br>
</div>
<blockquote type="cite">
<div style="background-color:rgb(255,242,230);border:2px dotted rgb(255,136,77)"><span style="font-size:12pt;font-family:sans-serif;color:black;font-weight:bold;padding:0.2em">CAUTION: This email originated outside the University. Check before clicking links
or attachments. </span><br>
</div>
<div>
<div dir="ltr">Thanks, Conor! As usual, that was blindingly fast!
<div><br>
</div>
<div>2. Your elegant, and elegantly named, solution that bypasses extensionality works brilliantly. Attached as
<a href="http://substitution-fixed.lagda.md/" title="Unmangled Microsoft
Safelink" target="_blank">
Substitution-fixed.lagda.md</a>.</div>
<div><br>
</div>
<div>1. I did my best to make explicit all of the implicit variables in extensionality, but it still complains. Attached as
<a href="http://substitution-broken.lagda.md/" title="Unmangled Microsoft
Safelink" target="_blank">
Substitution-broken.lagda.md</a>. 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.</div>
<div><br>
</div>
<div>Go well, -- P</div>
<div><br>
</div>
<div><br>
</div>
<div><br clear="all">
<div>
<div dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr">
<div dir="ltr">
<div>
<div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<br>
</div>
<div>. / \ and Senior Research Fellow, IOHK<br>
</div>
<div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div>
</div>
<div dir="ltr"><br>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, 3 Jan 2022 at 16:36, Conor McBride <<a href="mailto:conor@strictlypositive.org" target="_blank">conor@strictlypositive.org</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This email was sent to you by someone outside the University.<br>
You should only click on links or attachments if you are certain that the email is genuine and the content is safe.<br>
<br>
Hi Phil<br>
<br>
> On 3 Jan 2022, at 16:24, Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>> wrote:<br>
><br>
> 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:<br>
><br>
> 1. Why does Agda complain about my extensionality postulate? How do I fix it?<br>
<br>
For a start, Agda's moaning about the implicits that it can't infer in your with-expression.<br>
No type is pushed in to with-expressions, so there's nothing that will determing the<br>
missing information. I'm not sure with is what you need, but even if you were to use<br>
rewrite, the same would pertain. However...<br>
<br>
> 2. Is there a way to complete the proof without assuming extensionality?<br>
<br>
...you might consider making Henry Ford's extensional generalization of your goal. Any<br>
substitution will *behave* as the identity on terms if it *behaves* like the identity on<br>
variables, regardless of whether it's your *favourite* identity substitution. That statement<br>
pushes readily under lambda, because it talks about "any substitution", leaving you with<br>
an "as long as it behaves like the identity" condition to discharge.<br>
<br>
Cheers<br>
<br>
Conor<br>
<br>
><br>
> 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.<br>
><br>
> Go well, -- P<br>
><br>
><br>
><br>
><br>
> . \ Philip Wadler, Professor of Theoretical Computer Science,<br>
> . /\ School of Informatics, University of Edinburgh<br>
> . / \ and Senior Research Fellow, IOHK<br>
> . <a href="http://homepages.inf.ed.ac.uk/wadler/" rel="noreferrer" target="_blank">
http://homepages.inf.ed.ac.uk/wadler/</a><br>
><br>
> <<a href="http://substitution.lagda.md/" rel="noreferrer" title="Unmangled Microsoft Safelink" target="_blank">Substitution.lagda.md</a>>The
University of Edinburgh is a charitable body, registered in<br>
> Scotland, with registration number SC005336.<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">
Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" title="Unmangled Microsoft Safelink" target="_blank">
https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
</div>
<br>
<fieldset></fieldset>
<pre>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</div>
</div>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>