[Agda] problem using "with"

[Ulf Norell]

On Fri, May 11, 2012 at 7:36 PM, Guillermo Calderón <calderon at fing.edu.uy>wrote:

> hello,
>
> I have a problem using  "with".  The  code below  is a simplified version
> to illustrate the case:
>
> > g :  ℕ  → ℕ
> > g a with  a ≤? 5
> > ... |  yes _  = a
> > ... |  no  _  = suc a
> >
> > prop-g  : ∀ n  -> (R :  ℕ  → Set)
> >                -> (∀ m -> R (suc m))
> >                -> (∀ n -> n ≤ 5 -> R (g n))
> >                -> R (g n)
> > prop-g n R f1 f2  with n ≤? 5
> > ... | no  ¬p   =  f1 n
> > ... | yes p    =  f2 n p- -*** ERROR here ***
> >
>

The problem is that the abstraction happens at the point of the
with. At that point you haven't applied f2 yet, so the n in the type
of f2 is a different n from the one in n ≤? 5, thus it doesn't abstract.

One solution is to also abstract over the application of f2. Untested
code:

> prop-g  : ∀ n  -> (R :  ℕ  → Set)
>                -> (∀ m -> R (suc m))
>                -> (∀ n -> n ≤ 5 -> R (g n))
>                -> R (g n)
> prop-g n R f1 f2  with n ≤? 5 | f2 n
> ... | no  ¬p   | _   =  f1 n
> ... | yes p    | f2n =  f2n p

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120511/43e72879/attachment.html