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

[Dominique Devriese]

Jason,

2011/2/18 Jason Dusek <jason.dusek at gmail.com>:
>  With your help, I've managed to produce the much shorter module
>  below my signature.

Looks nice indeed, some small comments below.

>  The interaction between the '\le' shortcut and the letter 'n' is
>  most unfortunate.

In the emacs input mode, you mean? If so, I completely agree :) Emacs
also doesn't let you use the agda input mode in the interactive
search, which is very annoying. I've experimented using a custom
.XCompose for unicode input and it looks promising, but I have to work
it out further.

>  This was quite difficult to get sorted; I have no idea where
>  `trans' is actually defined for `DecTotalOrder', for example. I
>  just read `Relation.Binary' and guessed that I would find `trans'
>  where I found `refl'.

What I typically do is click around with the middle mouse button until
I find what I need ;) Most of the stuff in the std lib makes a lot of
sense when you get used to the paradigm.

> module upto where
>
> open import Data.Nat
> open import Data.Nat.Properties
> open import Relation.Binary
> open DecTotalOrder Data.Nat.decTotalOrder using (trans; refl)
> open import Data.Fin using (Fin; suc; zero; fromℕ≤)
>
>
> data Vec (A : Set) : ℕ → Set where
>  []  : Vec A zero
>  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

Any reason you're not using Data.Vec?

>
> infixl 100 _!_
> _!_ : {n : ℕ}{A : Set} → Vec A n → Fin n → A
> []       ! ()
> (x ∷ xs) ! zero = x
> (x ∷ xs) ! (suc i) = xs ! i

using Data.Vec:
_!_ = flip lookup

> n≤n+1 : {m : ℕ} → m ≤ suc m
> n≤n+1 = ≤-step refl

No need to define this yourself, it's already in Data.Nat.Properties,
called n≤1+n (explicit m though).

> upto : (n : ℕ) → Vec (Fin n) n
> upto n = upto' n refl
>  where
>  upto' : (m : ℕ) → (m ≤ n) → Vec (Fin n) m
>  upto' zero m≤n  = []
>  upto' (suc m') m≤n = fromℕ≤ m≤n ∷ upto' m' (trans n≤n+1 m≤n)

This is the same as what I wrote. There are more experienced people
reading this list though ;)

Dominique