<html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body>
Interesting; part 2 is beyond me. I've attached your file with what
I believe to be the desugaring of the relevant <font face="monospace">rewrite</font> clause, but it gives an error
“can't solve <font face="monospace">w ≟ `_</font>” for variable <font face="monospace">w</font>. It's maybe unusual for being of
function type (I can imagine it's doing an η-expansion to make the
unification problem harder), but I don't know whether that's what's
causing the problem. Even if an error is the correct response, it
seems like it's a bug that <font face="monospace">rewrite</font>
fails silently.<br>
<p>As for part 1, I think it's all about understanding what <font face="monospace">with</font>-abstraction is for, and what it
gives you over a (left-hand side) <font face="monospace">case</font>-expression.
The difference between <font face="monospace">rewrite q</font>
and <font face="monospace">with refl ← q</font>, for <font face="monospace">q : M ≡ N</font>, is that rewrite will
simultaneously <font face="monospace">with</font>-abstract over <font face="monospace">M</font>. The reason you'd want to <font face="monospace">with</font>-abstract over <font face="monospace">M</font> is because it's a complex expression
appearing elsewhere in the goal+context that will not unify
against <font face="monospace">N</font>. When you replace all the
occurrences of <font face="monospace">M</font> by a fresh
variable <font face="monospace">m</font>, the pattern-match of <font face="monospace">q</font> (which now has type <font face="monospace">m ≡ N</font>) to <font face="monospace">refl</font>
succeeds, and <font face="monospace">m</font> is replaced
everywhere else by <font face="monospace">N</font>.</p>
<p>Here's a quick example of a similar <font face="monospace">with</font>-abstraction
to what <font face="monospace">rewrite</font> gives you, but
where <font face="monospace">rewrite</font> itself is not
applicable:<br>
</p>
<pre>open import Data.Nat
open import Relation.Binary.PropositionalEquality
foo : ∀ l m n o → suc (l + m) ≡ suc (n + o) → n + o ≡ l + m
foo l m n o q with l + m
foo l m n o refl | .(n + o) = refl
</pre>
<p>Note that a match on <font face="monospace">q</font> before the
<font face="monospace">with</font> fails with a unification error
(because <font face="monospace">_+_</font> is not injective).
Note also that <font face="monospace">rewrite q</font> does not
change the goal – it is equivalent to with <font face="monospace">w
← suc (l + m) | refl ← q</font>, and because <font face="monospace">suc (l + m)</font> does not occur anywhere else
in the goal+context, nothing else is rewritten. The correct <font face="monospace">with</font>-abstraction is over either <font face="monospace">l + m</font> or <font face="monospace">n + o</font>.
The <font face="monospace">with</font>-abstraction over <font face="monospace">l + m</font> rewrites the occurrences in both <font face="monospace">q</font> and the goal to a fresh variable <font face="monospace">p</font>, leaving us proving <font face="monospace">∀ l m n o → suc p ≡ suc (n + o) → n + o ≡ p</font>.
The LHS and RHS of <font face="monospace">q</font> now unify,
which we force by pattern-matching to <font face="monospace">refl</font>,
leaving the solution of <font face="monospace">p</font> as the
dot-pattern <font face="monospace">.(n + o)</font>. With this
pattern-match, the problem becomes <font face="monospace">∀ l m n
o → n + o ≡ n + o</font>, which is easy.</p>
<p>Because of situations like that example, I tend to use <font face="monospace">rewrite</font> as merely a shorthand, having
already thought up a purely <font face="monospace">with</font>-based
solution. Coming up with the right <font face="monospace">with</font>-abstractions
is the real skill, which probably requires a bit of practice.</p>
<p>All the best,</p>
<p>James<br>
</p>
<div class="moz-cite-prefix">On 04/01/2022 16:36, Philip Wadler
wrote:<br>
</div>
<blockquote type="cite" cite="mid:CAESRbcrOGs_+sSEQ_8ETmrxDNG6RG9ASgHp5_CFZEpVoL4UTiA@mail.gmail.com">
<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" 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>
</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" moz-do-not-send="true" class="moz-txt-link-freetext">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" originalsrc="https://agda.readthedocs.io/en/latest/language/with-abstraction.html#rewrite" shash="dT8pTlSKSnOAFjwME5oaXBN2wyGQe0QxJHH0+Sfu8qPZE73yItGgXudXymH2lMZWTNi//gKm9JxCbPwyCodaODCtswa6UbeFhe920cslOK/j+U9WXX3rXjW3+5ozsPQn/mCjm5i7fETRhGTI2PhSzw+8kMxlbEO8LrHX7E/JU3E=" target="_blank" moz-do-not-send="true" title="Unmangled Microsoft Safelink" 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>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/" originalsrc="http://substitution-fixed.lagda.md/" shash="V3joExewq7U+6MaUnT4AC7csEI6ndpxF8S85WAA2P6NdaJpE49+kDaa8ieik943GzKxh8okQbS2vC6FwGoSBFQQGLeVt0QcncGn8tfwonPkHX/12GUEiV04wlWgE3oN7VQmvAJGjqqhTw/GWrIlYCel7XmT9vsksn0sbLOuwL8E=" title="Unmangled Microsoft Safelink" target="_blank" moz-do-not-send="true">
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="xNdHxtb+mbSZqma6KkWesqFHPRFysiwBwFydTLiu9s27os95cBit+MFAaOzFfPpjTwymqpyU70FZKD2a95fq9hCncK28BqnLHTQH4OqlYl+M/zzpmrCwzlTtc9NA6QsuK8GH1wj278ha9HcmcGSrCnHEBWbaaDhS9/tbkueopZI=" title="Unmangled Microsoft Safelink" target="_blank" moz-do-not-send="true">
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" 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" target="_blank" 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="re+EoOLXpsMHo3yGasS8Qri46UdbMNXCtZ9eBVkwL2yBU0KkkSLkwgNvggV7EbrAYvIe8dqCvpv1P3x5W1uzNTn2ZfUUinCuN2Oc3ghQ7rA0gJfl3O22Xbgguq/MmmdF3N00ibvVBvrPnU/C2Nh2ktEuuja+IwICDUGJSLOGPxQ=" rel="noreferrer" title="Unmangled Microsoft
Safelink" target="_blank" moz-do-not-send="true">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="fqCNQtKndZcPPaqYx0MnBoI5USVWTUZzCB1MHHFx4VzXpa+svHG5SZAsqTBHjFp8/C47a/GVl/oWK6HCh0/AGuLNGYPQpFLDO0mAHKFR5ECpuYvVjjn7Q2pJrupjUHsOWjfn9Abu6UujbXJIkuxmpDo2O1fBwrAGnSWOJMPIhbs=" rel="noreferrer" title="Unmangled Microsoft
Safelink" target="_blank" moz-do-not-send="true" class="moz-txt-link-freetext">
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" moz-do-not-send="true" class="moz-txt-link-freetext">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" originalsrc="https://lists.chalmers.se/mailman/listinfo/agda" shash="fqCNQtKndZcPPaqYx0MnBoI5USVWTUZzCB1MHHFx4VzXpa+svHG5SZAsqTBHjFp8/C47a/GVl/oWK6HCh0/AGuLNGYPQpFLDO0mAHKFR5ECpuYvVjjn7Q2pJrupjUHsOWjfn9Abu6UujbXJIkuxmpDo2O1fBwrAGnSWOJMPIhbs=" target="_blank" moz-do-not-send="true" title="Unmangled Microsoft Safelink" class="moz-txt-link-freetext">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" 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="lIxgzCz68tVou5TFd9119dh6WfTB70mopXm1yvK0n6F3Z3dWidotjzIkQzWVXwIfZ/tjMQn5+9Wkuq0mvWpV3PKeKC2yrmE4UUToCdjtd7JvNL8dgJWw1T3gqN1ibmeJYM4wPH4/VRzYbJQ8vKXENomKKceIzxO1kJBjdjxWGFU=" 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>
</blockquote>
</div>
</blockquote>
</body>
</html>