[Agda] Re: problem using "with"
Guillermo Calderón
calderon at fing.edu.uy
Mon May 14 17:50:46 CEST 2012
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
More information about the Agda
mailing list