Bounds.agda

module Bounds where



data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

data _<_ : Nat -> Nat -> Set where
  z<s : forall {n}   ->                 zero < suc n
  s<s : forall {m n} ->   m < n   ->   suc m < suc n

data *<_ : Nat -> Set where
  z<s : forall {n} ->                       *< suc n
  s<s : forall {n} ->      *< n   ->        *< suc n

data Fin : Nat -> Set where
  fzero : forall {n} ->                   Fin (suc n)
  fsuc  : forall {n} ->   Fin n   ->      Fin (suc n)

-- These next three show how Nat/Fin/< form a vertical sequence
-- Fin is Nat indexed by an upper bound, < is Fin indexed by the Nat it represents
-- notice that modulo names, they're the same function!

-- < to fin, highest to middle
<-to-fin : forall {m n} -> m < n -> Fin n
<-to-fin z<s     = fzero
<-to-fin (s<s p) = fsuc (<-to-fin p)

-- fin to nat, middle to lowest
fin-to-nat : forall {n} -> Fin n -> Nat
fin-to-nat fzero    = zero
fin-to-nat (fsuc f) = suc (fin-to-nat f)

-- fin to vec, middle to highest by indexing how it converts to lowest
fin-to-< : forall {n} -> (f : Fin n) -> fin-to-nat f < n
fin-to-< fzero    = z<s
fin-to-< (fsuc f) = s<s (fin-to-< f)



data List (A : Set) : Set where
  nil : List A
  cons : A -> List A -> List A

data HasLength (A : Set) : List A -> Nat -> Set where
  nil-z  :                                                           HasLength A nil         zero
  cons-s : forall {xs n} ->   {x : A}   ->   HasLength A xs n   ->   HasLength A (cons x xs) (suc n)

data HasLength* (A : Set) : Nat -> Set where
  nil-z  :                                                           HasLength* A zero
  cons-s : forall {n} ->           A    ->   HasLength* A n     ->   HasLength* A (suc n)

data Vec (A : Set) : Nat -> Set where
  vnil :                                                             Vec A zero
  vcons : forall {n} ->            A    ->   Vec A n            ->   Vec A (suc n)

-- These next three show how List/Vec/HasLength form a vertical sequence
-- Vec is List indexed by length, HasLength is Vec indexed by the List it represents
-- notice that modulo names, they're the same function!

-- hl to vec, highest to middle
hl-to-vec : forall {A xs n} -> HasLength A xs n -> Vec A n
hl-to-vec nil-z              = vnil
hl-to-vec (cons-s {x = x} p) = vcons x (hl-to-vec p)

-- vec to list, middle to lowest
vec-to-list : forall {A n} -> Vec A n -> List A
vec-to-list vnil        = nil
vec-to-list (vcons x v) = cons x (vec-to-list v)

-- vec to hl, middle to highest by indexing how it converts to lowest
vec-to-hl : forall {A n} -> (v : Vec A n) -> HasLength A (vec-to-list v) n
vec-to-hl vnil        = nil-z
vec-to-hl (vcons x v) = cons-s (vec-to-hl v)

-- These next three show how Nat/List/Vec form a vertical sequence
-- List is Nat augmented with more data, Vec is List indexed by the un-augmented Nat that the list comes from
-- NOTE: list-to-nat is normally called length
-- notice that modulo names, they're the same function!

-- vec to list, highest to middle
{-
vec-to-list : forall {A n} -> Vec A n -> List A
vec-to-list vnil        = nil
vec-to-list (vcons x v) = cons x (vec-to-list v)
-}

-- list to nat, middle to lowest
list-to-nat : forall {A} -> List A -> Nat
list-to-nat nil         = zero
list-to-nat (cons x xs) = suc (list-to-nat xs)

-- list to vec, middle to highest by indexing how it converts to the lowest
list-to-vec : forall {A} -> (xs : List A) -> Vec A (list-to-nat xs)
list-to-vec nil         = vnil
list-to-vec (cons x xs) = vcons x (list-to-vec xs)