[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
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
>
> 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
> (https://agda.readthedocs.io/en/latest/language/with-abstraction.html#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
>> . 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 <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>
More information about the Agda
mailing list