Fwd: [Agda] question about with

[Ulf Norell]

On Fri, Feb 29, 2008 at 9:03 PM, Dan Licata <drl at cs.cmu.edu> wrote:

> I have a question about refining goals using with.  Consider the
> following example:
>
>  data Nat : Set where
>    Z : Nat
>    S : Nat -> Nat
>
>  plus : Nat -> Nat -> Nat
>  plus n Z = n
>  plus n (S m) = S (plus n m)
>
>  data Id : Nat -> Nat -> Set where
>    Refl : {n : Nat} -> Id n n
>
>  plus-lh-z : (n : Nat) -> Id (plus Z n) n
>  plus-lh-z Z = Refl
>  plus-lh-z (S n) with (plus Z n) | plus-lh-z n
>  ...                | .n         | Refl = Refl
>
> This works fine.  Here, I'm using the with to replace instances of
> (plus Z n) with n in the context and goal, which is justified by the
> recursive call.  After this replacement, the goal is easy to prove.
>
> However, suppose I wanted to go the other way:
>
>  plus-lh-z' : (n : Nat) -> Id (plus Z n) n
>  plus-lh-z' Z = Refl
>  plus-lh-z' (S n) with n           | plus-lh-z' n
>  ...                 | .(plus Z n) | Refl = ?
>
> In this case, agda complains that
>
>  w != plus Z w of type Nat
>  when checking that the pattern Refl has type Id (plus Z w) w
>
> I don't understand why this refinement fails, when the above one
> succeeded.


What happens is that n is abstracted also from the type of plus-lh-z' so
you'll get two new arguments to your function (m : Nat)(p : Id (plus Z m)
m). Pattern matching on p doesn't work because we can't unify plus Z m and
m.

Of course, the second refinement isn't actually helpful in this case,
> but I have an analogous example where this is the direction I want to go
> (i.e., the goal type has the simple expression (analogous to n) but the
> term I want to write has the complicated expression (analogous to (plus
> Z n)) in its type, so I want to replace simple with complicated in the
> goal).
>

In this case you might get away with abstracting over that term as well. So
if you want to say

f x = rhs

where f : A -> T[u], rhs : T[v], p : u = v then you can try

f x with v | rhs | p
... | .u | z | refl = z

I also ran into an example where neither option worked.
>

Here you can try abstracting over both sides.

f x with u | v | rhs | p
... | y | .y | z | refl = z

I hope this helps.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080229/5cfba418/attachment.html