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

[Jason Dusek]

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:

    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.

--
Jason Dusek
Linux User #510144 | http://counter.li.org/




module upto where

open import Data.Nat
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)

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


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

middle : {l m n : ℕ} → l ≤′ m → m ≤′ n → l ≤′ n
middle p q₀ with q₀
... | ≤′-refl    = p
... | ≤′-step q₁ = ≤′-step (middle p q₁)

upto : (n : ℕ) → Vec (Fin n) n
upto n = upto' n ≤′-refl
 where
  upto' : (m : ℕ) → (m ≤′ n) → Vec (Fin n) m
  upto' m m≤′n with m
  ... | zero   = []
  ... | suc m' = fromℕ m ∷ upto' m' (middle prf m≤′n)
   where
    prf : m' ≤′ m
    prf = n≤′n+1