Agda-2.3.2.2: src/prototyping/termrep/lambdapi/prelude.lp
-- identity and const
let id = (\ a x -> x) : forall (a : *) . a -> a
let const = (\ a b x y -> x) : forall (a : *) (b : *) . a -> b -> a
-- addition of natural numbers
let plus =
natElim
( \ _ -> Nat -> Nat ) -- motive
( \ n -> n ) -- case for Zero
( \ p rec n -> Succ (rec n) ) -- case for Succ
-- predecessor, mapping 0 to 0
let pred =
natElim
( \ _ -> Nat )
Zero
( \ n' _rec -> n' )
-- a simpler elimination scheme for natural numbers
let natFold =
( \ m mz ms -> natElim
( \ _ -> m )
mz
( \ n' rec -> ms rec ) )
: forall (m : *) . m -> (m -> m) -> Nat -> m
-- an eliminator for natural numbers that has special
-- cases for 0 and 1
let nat1Elim =
( \ m m0 m1 ms -> natElim m m0
(\ p rec -> natElim (\ n -> m (Succ n)) m1 ms p) )
: forall (m : Nat -> *) . m 0 -> m 1 ->
(forall n : Nat . m (Succ n) -> m (Succ (Succ n))) ->
forall (n : Nat) . m n
-- an eliminator for natural numbers that has special
-- cases for 0, 1 and 2
let nat2Elim =
( \ m m0 m1 m2 ms -> nat1Elim m m0 m1
(\ p rec -> natElim (\ n -> m (Succ (Succ n))) m2 ms p) )
: forall (m : Nat -> *) . m 0 -> m 1 -> m 2 ->
(forall n : Nat . m (Succ (Succ n)) -> m (Succ (Succ (Succ n)))) ->
forall (n : Nat) . m n
-- increment by one
let inc = natFold Nat (Succ Zero) Succ
-- embed Fin into Nat
let finNat = finElim (\ _ _ -> Nat)
(\ _ -> Zero)
(\ _ _ rec -> Succ rec)
-- unit type
let Unit = Fin 1
-- constructor
let U = FZero 0
-- eliminator
let unitElim =
( \ m mu -> finElim ( nat1Elim (\ n -> Fin n -> *)
(\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit) )
( natElim (\ n -> natElim (\ n -> Fin (Succ n) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FZero n))
mu
(\ _ _ -> U) )
( \ n f _ -> finElim (\ n f -> natElim (\ n -> Fin (Succ n) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc n f))
(\ _ -> U)
(\ _ _ _ -> U)
n f )
1 )
: forall (m : Unit -> *) . m U -> forall (u : Unit) . m u
-- empty type
let Void = Fin 0
-- eliminator
let voidElim =
( \ m -> finElim (natElim (\ n -> Fin n -> *)
(\ x -> m x)
(\ _ _ _ -> Unit))
(\ _ -> U)
(\ _ _ _ -> U)
0 )
: forall (m : Void -> *) (v : Void) . m v
-- type of booleans
let Bool = Fin 2
-- constructors
let False = FZero 1
let True = FSucc 1 (FZero 0)
-- eliminator
let boolElim =
( \ m mf mt -> finElim ( nat2Elim (\ n -> Fin n -> *)
(\ _ -> Unit) (\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit) )
( nat1Elim ( \ n -> nat1Elim (\ n -> Fin (Succ n) -> *)
(\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FZero n))
U mf (\ _ _ -> U) )
( \ n f _ -> finElim ( \ n f -> nat1Elim (\ n -> Fin (Succ n) -> *)
(\ _ -> Unit)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc n f) )
( natElim
( \ n -> natElim
(\ n -> Fin (Succ (Succ n)) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc (Succ n) (FZero n)) )
mt (\ _ _ -> U) )
( \ n f _ -> finElim
(\ n f -> natElim
(\ n -> Fin (Succ (Succ n)) -> *)
(\ x -> m x)
(\ _ _ _ -> Unit)
n (FSucc (Succ n) (FSucc n f)))
(\ _ -> U)
(\ _ _ _ -> U)
n f )
n f )
2 )
: forall (m : Bool -> *) . m False -> m True -> forall (b : Bool) . m b
-- boolean not, and, or, equivalence, xor
let not = boolElim (\ _ -> Bool) True False
let and = boolElim (\ _ -> Bool -> Bool) (\ _ -> False) (id Bool)
let or = boolElim (\ _ -> Bool -> Bool) (id Bool) (\ _ -> True)
let iff = boolElim (\ _ -> Bool -> Bool) not (id Bool)
let xor = boolElim (\ _ -> Bool -> Bool) (id Bool) not
-- even, odd, isZero, isSucc
let even = natFold Bool True not
let odd = natFold Bool False not
let isZero = natFold Bool True (\ _ -> False)
let isSucc = natFold Bool False (\ _ -> True)
-- equality on natural numbers
let natEq =
natElim
( \ _ -> Nat -> Bool )
( natElim
( \ _ -> Bool )
True
( \ n' _ -> False ) )
( \ m' rec_m' -> natElim
( \ _ -> Bool )
False
( \ n' _ -> rec_m' n' ))
-- "oh so true"
let Prop = boolElim (\ _ -> *) Void Unit
-- reflexivity of equality on natural numbers
let pNatEqRefl =
natElim
(\ n -> Prop (natEq n n))
U
(\ n' rec -> rec)
: forall (n : Nat) . Prop (natEq n n)
-- alias for type-level negation
let Not = (\ a -> a -> Void) : * -> *
-- Leibniz prinicple (look at the type signature)
let leibniz =
( \ a b f -> eqElim a
(\ x y eq_x_y -> Eq b (f x) (f y))
(\ x -> Refl b (f x)) )
: forall (a : *) (b : *) (f : a -> b) (x : a) (y : a) .
Eq a x y -> Eq b (f x) (f y)
-- symmetry of (general) equality
let symm =
( \ a -> eqElim a
(\ x y eq_x_y -> Eq a y x)
(\ x -> Refl a x) )
: forall (a : *) (x : a) (y : a) .
Eq a x y -> Eq a y x
-- transitivity of (general) equality
let tran =
( \ a x y z eq_x_y -> eqElim a
(\ x y eq_x_y -> forall (z : a) . Eq a y z -> Eq a x z)
(\ x z eq_x_z -> eq_x_z)
x y eq_x_y z )
: forall (a : *) (x : a) (y : a) (z : a) .
Eq a x y -> Eq a y z -> Eq a x z
-- apply an equality proof on two types
let apply =
eqElim * (\ a b _ -> a -> b) (\ _ x -> x)
: forall (a : *) (b : *) (p : Eq * a b) . a -> b
-- proof that 1 is not 0
let p1IsNot0 =
(\ p -> apply Unit Void
(leibniz Nat *
(natElim (\ _ -> *) Void (\ _ _ -> Unit))
1 0 p)
U)
: Not (Eq Nat 1 0)
-- proof that 0 is not 1
let p0IsNot1 =
(\ p -> p1IsNot0 (symm Nat 0 1 p))
: Not (Eq Nat 0 1)
-- proof that zero is not a successor
let p0IsNoSucc =
natElim
( \ n -> Not (Eq Nat 0 (Succ n)) )
p0IsNot1
( \ n' rec_n' eq_0_SSn' ->
rec_n' (leibniz Nat Nat pred Zero (Succ (Succ n')) eq_0_SSn') )
-- generate a vector of given length from a specified element (replicate)
let replicate =
( natElim
( \ n -> forall (a : *) . a -> Vec a n )
( \ a _ -> Nil a )
( \ n' rec_n' a x -> Cons a n' x (rec_n' a x) ) )
: forall (n : Nat) . forall (a : *) . a -> Vec a n
-- alternative definition of replicate
let replicate' =
(\ a n x -> natElim (Vec a)
(Nil a)
(\ n' rec_n' -> Cons a n' x rec_n') n)
: forall (a : *) (n : Nat) . a -> Vec a n
-- generate a vector of given length n, containing the natural numbers smaller than n
let fromto =
natElim
( \ n -> Vec Nat n )
( Nil Nat )
( \ n' rec_n' -> Cons Nat n' n' rec_n' )
-- append two vectors
let append =
( \ a -> vecElim a
(\ m _ -> forall (n : Nat) . Vec a n -> Vec a (plus m n))
(\ _ v -> v)
(\ m v vs rec n w -> Cons a (plus m n) v (rec n w)))
: forall (a : *) (m : Nat) (v : Vec a m) (n : Nat) (w : Vec a n).
Vec a (plus m n)
-- helper function for tail, see below
let tail' =
(\ a -> vecElim a ( \ m v -> forall (n : Nat) . Eq Nat m (Succ n) -> Vec a n )
( \ n eq_0_SuccN -> voidElim ( \ _ -> Vec a n )
( p0IsNoSucc n eq_0_SuccN ) )
( \ m' v vs rec_m' n eq_SuccM'_SuccN ->
eqElim Nat
(\ m' n e -> Vec a m' -> Vec a n)
(\ _ v -> v)
m' n
(leibniz Nat Nat pred (Succ m') (Succ n) eq_SuccM'_SuccN) vs))
: forall (a : *) (m : Nat) . Vec a m -> forall (n : Nat) . Eq Nat m (Succ n) -> Vec a n
-- compute the tail of a vector
let tail =
(\ a n v -> tail' a (Succ n) v n (Refl Nat (Succ n)))
: forall (a : *) (n : Nat) . Vec a (Succ n) -> Vec a n
-- projection out of a vector
let at =
(\ a -> vecElim a ( \ n v -> Fin n -> a )
( \ f -> voidElim (\ _ -> a) f )
( \ n' v vs rec_n' f_SuccN' ->
finElim ( \ n _ -> Eq Nat n (Succ n') -> a )
( \ n e -> v )
( \ n f_N _ eq_SuccN_SuccN' ->
rec_n' (eqElim Nat
(\ x y e -> Fin x -> Fin y)
(\ _ f -> f)
n n'
(leibniz Nat Nat pred
(Succ n) (Succ n') eq_SuccN_SuccN')
f_N))
(Succ n')
f_SuccN'
(Refl Nat (Succ n'))))
: forall (a : *) (n : Nat) . Vec a n -> Fin n -> a
-- head of a vector
let head =
(\ a n v -> at a (Succ n) v (FZero n))
: forall (a : *) (n : Nat) . Vec a (Succ n) -> a
-- vector map
let map =
(\ a b f -> vecElim a ( \ n _ -> Vec b n )
( Nil b )
( \ n x _ rec -> Cons b n (f x) rec ))
: forall (a : *) (b : *) (f : a -> b) (n : Nat) . Vec a n -> Vec b n
-- proofs that 0 is the neutral element of addition
-- one direction is trivial by definition of plus:
let p0PlusNisN =
Refl Nat
: forall n : Nat . Eq Nat (plus 0 n) n
-- the other direction requires induction on N:
let pNPlus0isN =
natElim ( \ n -> Eq Nat (plus n 0) n )
( Refl Nat 0 )
( \ n' rec -> leibniz Nat Nat Succ (plus n' 0) n' rec )
: forall n : Nat . Eq Nat (plus n 0) n