[Agda] With and the inspect idiom

[Ulf Norell]

On Sun, May 11, 2008 at 3:56 PM, Shin-Cheng Mu <scm at iis.sinica.edu.tw>
wrote:

> I just realised that my previous message was sent with wrong
> encoding (Big5 rather than UTF-8). Hope this message could be
> displayed correctly on your computer, if the previous one
> did not. Sorry for duplicated posting.
>
>    ----------
>
> Hi,
>
> I asked this question before but I probably have not made myself
> understood. I recently encountered the same problem, so I would
> like to bring up the topic again..
>
> Suppose I am defining such a function:
>
>   foo <something else> f b  with f b
>   ...| (c , d) = { }0
>
> by performing "with f b", the types of some arguments in
> <something else> that involve (f b) would be refined to more
> specific types.
>
> Strangely, however, after "with f b", Agda does not seem to
> have the knowledge that (f b) equals (c , d). If I need a term
> of type f b ≡ (c , d) in { }0, I cannot simply use ≡-refl.
> To get such a term, I could use the "inspect idiom":
>
>   foo <something else> f b with inspect (f b)
>   ...| (c , d) with-≡ fb≡cd = { }0
>
> The type of fb≡cd is f b ≡ (c , d).
>
> However, now the types of other arguments in <something else>
> don't get refined! How do I achieve both?
>
> We found this weird trick using "with" twice:
>
>   foo <something else> with inspect (f b)
>   ... | v with-≡ v≡fb    with f b | v≡fb
>   ...    | (c , d) | v≡cd = { }0
>
> After "with f b", the types of arguments in <something else>
> do get refined. Furthermore, we now have two proofs having type:
>
>     v≡fb   : v ≡ f b
>     v≡cd   : v ≡ (c , d)
>
> So I get a proof of f b ≡ (c , d) by transitivity:
>
>     ≡-trans (≡-sym v≡fb) v≡cd   :   f b ≡ (c , d)


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...

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080511/3362e7dc/attachment.html