[Agda] how to count 0..n-1

[Dominique Devriese]

Jason,

2011/2/11 Jason Dusek <jason.dusek at gmail.com>:
> On Sat, Feb 5, 2011 at 09:39, Nils Anders Danielsson <nad at chalmers.se> wrote:
>> On 2011-02-05 09:55, Jason Dusek wrote:
>> > Now, I think this is because `upto m' has type `Fin m' and
>> > not `Fin n'. Do I need an additional, perhaps implicit
>> > parameter? Perhaps a proof term?
>>
>> You could use weakening. See Data.Vec.allFin in the standard library.
>
>  Thanks for pointing me to that example. I don't understand
>  quite how the term "weakening" applies here; but then again,
>  this material is all new to me.
>
>  Going from a Vec (Fin m) m to a Vec (Fin m+1) m+1 by way of
>  map does seem unattractive, from an operational point of view
>  -- it's n^2 in instead of linear.
>
>  I have taken a stab at it (below my signature); but I can't
>  get the term `prf' to typecheck:

You definitely seem on the right track.

>    suc m' != m of type ℕ
>    when checking that the expression n≤′n+1 has type m' ≤′ m
>
>  I was hoping the `with' would handle this. If you can offer
>  any advice I would sure appreciate it.

The problem is that when using with, Agda doesn't remember the
relation between what you pattern match on and the variables in the
pattern.  There's a general solution to that using rewrite, but in
this case, you can more easily fix the problem by directly pattern
matching in the function definition itself:
 upto' : (m : ℕ) → (m ≤′ n) → Vec (Fin n) m
 upto' zero m≤′n = []
 upto' (suc m') m≤′n = fromℕ (suc m') ∷ upto' m' (middle prf m≤′n)
  where
   prf : m' ≤′ suc m'
   prf = n≤′n+1

However, then you'll see another problem in your code. The problem is
that fromℕ produces a Fin (suc (suc m')) instead of a Fin n. You
should use something like fromℕ≤ to fix this. That is defined for the
normal ≤ relation, not ≤' so you'll have to roll your own. However,
it's probably easier to use the normal ≤, then you can also replace
your middle with the standard trans, your n≤'n+1 with the normal n≤1+n
from Data.Nat.Properties.

Dominique