[Agda] Re: problem using "with"

[Guillermo Calderón]

On 12/05/12 04:17, Ulf Norell wrote:
>
> On Fri, May 11, 2012 at 9:52 PM, Guillermo Calderón
> <calderon at fing.edu.uy
> <mailto:calderon at fing.edu.uy>> wrote:
>
>     On 11/05/12 16:24, Ulf Norell wrote:
>
>
>         On Fri, May 11, 2012 at 7:36 PM, Guillermo Calderón
>         <calderon at fing.edu.uy
>         <mailto:calderon at fing.edu.uy>
>         <mailto:calderon at fing.edu.uy
>         <mailto: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.
>
>
>     Ulf,
>     Thanks for your answer.
>     As far as i known, the same problem should happen for the case (no  ¬p).
>
>
>      > ... | no  ¬p   =  f1 n
>
>     However,  no error is reported by agda at this level and  (f1 n)  is
>     accepted as well typed.
>     ¿what is the difference between   both cases?
>
>
> In the no case you don't need the g n in f2 to reduce. The g n in the
> goal gets abstracted over
> without problems when you do the with.
>

Thanks again.
I tested your proposal and it works:

 > 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



 From your explanations, I do understand how  the "with" works.
But  this behaviour results rather counter-intuitive to me.

Guillermo