--------------------------------------------------------------------------------------- [] --------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ! ( b : B ! data !------------! where !-----------------! ; !------------------! ! Or A B : * ) ! left a : Or A B ) ! right b : Or A B ) --------------------------------------------------------------------------------------- ( A, B : * ! ( a : A ; b : B ! data !-------------! where !--------------------! ! And A B : * ) ! pair a b : And A B ) --------------------------------------------------------------------------------------- ( A : * ! let !-----------! ! Not A : * ) Not A => A -> Zero --------------------------------------------------------------------------------------- ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) --------------------------------------------------------------------------------------- let (-----------! ! one : Nat ) one => suc zero --------------------------------------------------------------------------------------- let (-----------! ! two : Nat ) two => suc one --------------------------------------------------------------------------------------- let (-------------! ! three : Nat ) three => suc two --------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! add m n : Nat ) add m n <= rec m { add m n <= case m { add zero n => n add (suc m) n => suc (add m n) } } --------------------------------------------------------------------------------------- ( a, b : A ; p : a = b ! let !-----------------------! ! eqSym p : b = a ) eqSym p <= case p { eqSym refl => refl } --------------------------------------------------------------------------------------- ( a, b, c : A ; p : a = b ; q : b = c ! let !---------------------------------------! ! eqTrans p q : a = c ) eqTrans p q <= case p { eqTrans refl q => q } --------------------------------------------------------------------------------------- ( f : A -> B ; p : a = b ! let !----------------------------! ! eqResp f p : (f a) = (f b) ) eqResp f p <= case p { eqResp f refl => refl } --------------------------------------------------------------------------------------- ( f : A -> B -> C ; p : a = b ; q : c = d ! let !-------------------------------------------! ! eqResp2 f p q : f a c = f b d ) eqResp2 f p q <= case p { eqResp2 f refl q <= case q { eqResp2 f refl refl => refl } } --------------------------------------------------------------------------------------- ( P : A -> * ; a, b : A ; q : a = b ; p : P a ! let !------------------------------------------------! ! eqSubst q p : P b ) eqSubst q p <= case q { eqSubst refl p => p } --------------------------------------------------------------------------------------- ( P : * ! let !-----------! ! Dec P : * ) Dec P => Or P (Not P) --------------------------------------------------------------------------------------- ( p : zero = suc n ! let !------------------! ! znes p : Empty ) znes p <= case p --------------------------------------------------------------------------------------- ( p : suc m = suc n ! let !-------------------! ! injSuc p : m = n ) injSuc p <= case p { injSuc refl => refl } --------------------------------------------------------------------------------------- ( p : Dec (m = n) ! let !-----------------------------------! ! eqSuc p : Dec ((suc m) = (suc n)) ) eqSuc p <= case p { eqSuc (left refl) => left refl eqSuc (right b) => right (lam p => b (injSuc p)) } --------------------------------------------------------------------------------------- ( m, n : Nat ! let !-----------------------! ! eq' m n : Dec (m = n) ) eq' m n <= rec m { eq' m n <= case m { eq' zero n <= case n { eq' zero zero => left refl eq' zero (suc n) => right (lam p => znes p) } eq' (suc m) n <= case n { eq' (suc m) zero => right (lam p => znes (eqSym p)) eq' (suc m) (suc n) => eqSuc (eq' m n) } } } --------------------------------------------------------------------------------------- inspect eq' one two => right (lam p => znes (injSuc p)) : Or (suc zero = suc (suc zero)) (all x : suc zero = suc (suc zero) => Zero) --------------------------------------------------------------------------------------- inspect eq' two two => left refl : Or (suc (suc zero) = suc (suc zero)) % (all x : suc (suc zero) = suc (suc zero) => Zero) --------------------------------------------------------------------------------------- ( A : * ! ( a : A ; as : List A ! data !------------! where (--------------! ; !----------------------! ! List A : * ) ! nil : List A ) ! cons a as : List A ) --------------------------------------------------------------------------------------- let (-----------------! ! l123 : List Nat ) l123 => cons one (cons two (cons three nil)) --------------------------------------------------------------------------------------- ( as : List A ! let !----------------! ! count as : Nat ) count as <= rec as { count as <= case as { count nil => zero count (cons a as) => suc (count as) } } --------------------------------------------------------------------------------------- inspect count l123 => suc (suc (suc zero)) : Nat --------------------------------------------------------------------------------------- ( as, bs : List A ! let !-----------------------! ! append as bs : List A ) append as bs <= rec as { append as bs <= case as { append nil bs => bs append (cons a as) bs => cons a (append as bs) } } --------------------------------------------------------------------------------------- inspect append l123 l123 => cons (suc zero) (cons (suc (suc zero)) ! : List Nat !% (cons (suc (suc (suc zero))) !! ! !% (cons (suc zero) !!! ! ! !% (cons (suc (suc zero)) !!!! ! ! ! !% (cons (suc (suc (suc zero))) nil))))) --------------------------------------------------------------------------------------- ( as : List A ! let !-----------------! ! rev as : List A ) rev as <= rec as { rev as <= case as { rev nil => nil rev (cons a as) => append (rev as) (cons a nil) } } --------------------------------------------------------------------------------------- inspect rev l123 => cons (suc (suc (suc zero))) (cons (suc (suc zero)) (cons (suc zero) nil)) : List Nat --------------------------------------------------------------------------------------- ( a : A ; as : List A ! let !--------------------------------------------------! ; revlemlem a as [] ! revlemlem a as : ! ! rev (append as (cons a nil)) = cons a (rev as) ) --------------------------------------------------------------------------------------- ( as : List A ! let !-------------------------------! ! revLem as : rev (rev as) = as ) revLem as <= rec as { revLem as <= case as { revLem nil => refl revLem (cons a as) => eqTrans (revlemlem a (rev as)) (eqResp (cons a) (revLem as)) } } ---------------------------------------------------------------------------------------