<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
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 moz-do-not-send="true" href="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite" class="moz-txt-link-freetext">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 class="moz-cite-prefix">On 03/01/2022 19:20, Philip Wadler
wrote:<br>
</div>
<blockquote type="cite" cite="mid:CAESRbcpxgsJeA18-wy=82jOErFY8kj2pKJPQ98E1A8O1VeXNOA@mail.gmail.com">
<div style="background-color:#fff2e6; border:2px dotted #ff884d"><span style="font-size:12pt; font-family:sans-serif; color:black;
font-weight:bold; padding:.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/" originalsrc="http://substitution-fixed.lagda.md/" shash="WDSuIPrRryFLDDxBHt7+YKPrActo0DsWxEvloZerbnRoVjivvNqeO13YfGheo1XAwR/MWuWfcNTn2jodneXae1U+J22MiV5Jx4g+iZ16OP3i7MKbKPB381a/AP+ORAZN9+tA0A2PWYDNyryHJYwq0ML1txvqZiqWVda1jF2+7RM=" moz-do-not-send="true" title="Unmangled Microsoft
Safelink">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/" originalsrc="http://substitution-broken.lagda.md/" shash="D4MAZQv8yad/1GFJ2J1tWiCeEUBTLwjMK2W+wdE6THVc6HPnbzzH5q1gkYHW2ZnJTuLPfw+mBh/WxAoGGlP3TNRm9/+V7Y079ePNkf3t2ipLH11++5mSGKWLnzEgW2k3rnXapDN2XCTvSkP8XdACn7AgTmK3691U56fEhUvOoKU=" moz-do-not-send="true" title="Unmangled Microsoft
Safelink">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" 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" moz-do-not-send="true" class="moz-txt-link-freetext">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" moz-do-not-send="true" class="moz-txt-link-freetext">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" moz-do-not-send="true" class="moz-txt-link-freetext">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" moz-do-not-send="true" class="moz-txt-link-freetext">
http://homepages.inf.ed.ac.uk/wadler/</a><br>
><br>
> <<a href="http://substitution.lagda.md/" originalsrc="http://substitution.lagda.md/" shash="EkYE4ojIwx0DEtjDh7+/vcIOHRFLpWe0rtNro71t8sdsQiIReY+oEVIdkkTWs65k4Dm4CW/DTJcDfReguPr+rvaKJjvDFxpMPY4imP303bzH2cM3R+bQ3mTQ6TgsurLyPYjpDObTI1DaiacxNuLC2hZoLhcn1CTZrfenmECFRuE=" rel="noreferrer" target="_blank" moz-do-not-send="true" title="Unmangled Microsoft Safelink">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" moz-do-not-send="true" class="moz-txt-link-freetext">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" originalsrc="https://lists.chalmers.se/mailman/listinfo/agda" shash="sZMWi9B+souPwyrvhTvvgY+P5KNxfxl4d2hn4jonx6Zm5ojF7U+PvbEZeyx3xuyOG4o4UXGyltboaUoAJCF0dFiPO4jRJhw80NXEvwHDkgWk+ac7+wg7H4ndxi6t1q5Gi/VLOG8Q4qSwuLmmuN4V9CS0oi6lxddwXybZTSXvTiY=" rel="noreferrer" target="_blank" moz-do-not-send="true" title="Unmangled Microsoft Safelink" class="moz-txt-link-freetext">
https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
</blockquote>
</div>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
</body>
</html>