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

James Wood james.wood.100 at strath.ac.uk
Wed Jan 5 23:57:45 CET 2022

```Interesting; part 2 is beyond me. I've attached your file with what I
believe to be the desugaring of the relevant rewrite clause, but it
gives an error “can't solve w ≟ `_” for variable w. 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 rewrite fails silently.

As for part 1, I think it's all about understanding what
with-abstraction is for, and what it gives you over a (left-hand side)
case-expression. The difference between rewrite q and with refl ← q, for
q : M ≡ N, is that rewrite will simultaneously with-abstract over M. The
reason you'd want to with-abstract over M is because it's a complex
expression appearing elsewhere in the goal+context that will not unify
against N. When you replace all the occurrences of M by a fresh variable
m, the pattern-match of q (which now has type m ≡ N) to refl succeeds,
and m is replaced everywhere else by N.

Here's a quick example of a similar with-abstraction to what rewrite
gives you, but where rewrite itself is not applicable:

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

Note that a match on q before the with fails with a unification error
(because _+_ is not injective). Note also that rewrite q does not change
the goal – it is equivalent to with w ← suc (l + m) | refl ← q, and
because suc (l + m) does not occur anywhere else in the goal+context,
nothing else is rewritten. The correct with-abstraction is over either l
+ m or n + o. The with-abstraction over l + m rewrites the occurrences
in both q and the goal to a fresh variable p, leaving us proving ∀ l m n
o → suc p ≡ suc (n + o) → n + o ≡ p. The LHS and RHS of q now unify,
which we force by pattern-matching to refl, leaving the solution of p as
the dot-pattern .(n + o). With this pattern-match, the problem becomes ∀
l m n o → n + o ≡ n + o, which is easy.

Because of situations like that example, I tend to use rewrite as merely
a shorthand, having already thought up a purely with-based solution.
Coming up with the right with-abstractions is the real skill, which
probably requires a bit of practice.

All the best,

James

On 04/01/2022 16:36, Philip Wadler wrote:
> 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"!
>
> 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.
>
> 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?
>
> Thank you again! Go well, -- P
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
>
>
>
> On Tue, 4 Jan 2022 at 15:42, James Wood <james.wood.100 at strath.ac.uk>
> 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,
>
>     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
>     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
>>
>>
>>
>>     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
>>         >
>>         > 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
>>         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
>>         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)
>>         >
>>         > Go well, -- P
>>         >
>>         >
>>         >
>>         >
>>         > .   \ Philip Wadler, Professor of Theoretical Computer Science,
>>         > .   /\ School of Informatics, University of Edinburgh
>>         > .  /  \ and Senior Research Fellow, IOHK
>>         >
>>         > <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
>     _______________________________________________
>     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/20220105/9f19231b/attachment-0001.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Substitution-broken.lagda.md
Type: text/markdown
Size: 2806 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20220105/9f19231b/attachment-0001.bin>
```