[Agda] With and the inspect idiom

[Ulf Norell]

2008/5/14 Shin-Cheng Mu <scm at iis.sinica.edu.tw>:

>
> On May 11, 2008, at 11:19 PM, Ulf Norell wrote:
>
>> Rather than resorting to transitivity lemmas you can pattern match on the
>> first (or second) proof:
>>
>>  foo <something else> with inspect (f b)
>>  foo <something else> | v with-≡ v≡fb    with f b | v≡fb
>>  foo <something else> | .(f b) with-≡ ≡-refl | (c , d) | fb≡cd = { }0
>>
>> Now fb≡cd : f b ≡ (c , d) which is exactly what we wanted. That's as
>> simple
>> as I can manage I'm afraid...
>>
>
> Thanks! It looks like a nice solution.
>
> However, I am not sure I understand how it works. It seems that before
> "with f b", v≡fb has type v ≡ fb. I suppose that after the second "with",
> Agda somehow know that it v equals f b, therefore v≡fb also has type
> f b ≡ f b and may thus be matched with ≡-refl. But how did that happen?
>

When you match v≡fb against ≡-refl you force v to become equal to f b, it
wasn't equal before the matching.

> And how come v≡fb also has type f b ≡ (c , d) in the last pattern?
>

 It started out as v ≡ f b, then we abstracted over f b to get v ≡ z (for a
fresh variable z). Next we pattern matched on a proof that v ≡ f b
instantiating v to f b yielding the type f b ≡ z. Finally we pattern match
on z with the pattern (c , d) and so we get the type f b ≡ (c , d).

I should get clearer if you walk through the steps manually and look at the
context in each step.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080514/54025c41/attachment.html