[Agda] Re: problem using "with"

[Ulf Norell]

On Fri, May 11, 2012 at 9:52 PM, Guillermo Calderón <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>> 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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120512/8ac2d119/attachment.html