Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
data Nat : Set where
zero : Nat
suc : Nat -> Nat
data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
data Fin : Nat -> Set where
fzero : {n : Nat} -> Fin (suc n)
fsuc : {n : Nat} -> Fin n -> Fin (suc n)
infixl 20 _∘_
_∘_ : {A : Set}{B : A -> Set}{C : (x : A) -> B x -> Set}
(f : {x : A}(y : B x) -> C x y)(g : (x : A) -> B x)
(x : A) -> C x (g x)
(f ∘ g) x = f (g x)
infixl 20 _!_
_!_ : {n : Nat}{A : Set} -> Vec A n -> Fin n -> A
[] ! ()
(x :: xs) ! fzero = x
(x :: xs) ! (fsuc i) = xs ! i
tabulate : {n : Nat}{A : Set} -> (Fin n -> A) -> Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f fzero :: tabulate (f ∘ fsuc)
data _==_ {A : Set}(x : A) : A -> Set where
refl : x == x
lem-tab-! : forall {A n} (xs : Vec A n) -> tabulate (_!_ xs) == xs
lem-tab-! [] = refl
lem-tab-! (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs
... | .xs | refl = refl
lem-!-tab : forall {A n} (f : Fin n -> A)(i : Fin n) -> tabulate f ! i == f i
lem-!-tab {n = zero} f ()
lem-!-tab {n = suc m} f fzero = refl
lem-!-tab {n = suc m} f (fsuc i) with tabulate f
lem-!-tab {n = suc m} f (fsuc i) | (x :: xs) with tabulate (_!_ xs) | lem-tab-! xs | lem-!-tab (_!_ xs) i
lem-!-tab {n = suc m} f (fsuc i) | (x :: xs) | .xs | refl | refl = refl
-- compiler error:
-- tabulate (λ x₁ → f (fsuc x₁)) ! i != f (fsuc i) of type .A
-- when checking that the expression refl has type
-- (tabulate (λ x → f (fsuc x)) ! i) == f (fsuc i)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.