------------------------------------------------------------------------------------------------ ( 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 ------------------------------------------------------------------------------------------------ ( P : * ! let !-----------! ! Dec P : * ) Dec P => Or P (Not P) ------------------------------------------------------------------------------------------------ ( 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 P q p : P b ) eqSubst P q p <= case q { eqSubst P refl p => p } ------------------------------------------------------------------------------------------------ ( n : Nat ; A : * ! ( a : A ; as : Vec n A ! data !------------------! where (-------------------! ; !----------------------------! ! Vec n A : * ) ! vnil : Vec zero A ) ! vcons a as : Vec (suc n) A ) ------------------------------------------------------------------------------------------------ let (----------------------! ! v123 : Vec three Nat ) v123 => vcons one (vcons two (vcons three vnil)) ------------------------------------------------------------------------------------------------ ( v : Vec (suc n) A ! let !-------------------! ! vhd v : A ) vhd v <= case v { vhd (vcons a av) => a } ------------------------------------------------------------------------------------------------ ( as : Vec n A ; bs : Vec m A ! let !---------------------------------! ! vappend as bs : Vec (add n m) A ) vappend as bs <= rec as { vappend as bs <= case as { vappend vnil bs => bs vappend (vcons a as) bs => vcons a (vappend as bs) } } ------------------------------------------------------------------------------------------------ [-------------------------------------------------------------------------------------------------------------------------------------------! ! ( as : Vec n A ! ! !let !-------------------! ! ! ! vrev as : Vec n A ) ! ! ! ! vrev as <= rec as ! ! { vrev as <= case as ! ! { vrev vnil => vnil ! ! vrev (vcons a as) => [vappend (vrev as) (vcons a vnil)] ! ! } ! ! } ] ------------------------------------------------------------------------------------------------ ( n : Nat ! let !-------------------------------! ! addComZero n : n = add n zero ) addComZero n <= rec n { addComZero n <= case n { addComZero zero => refl addComZero (suc n) => eqResp suc (addComZero n) } } ------------------------------------------------------------------------------------------------ ( n, m : Nat ! let !-----------------------------------------------! ! addComSuc n m : suc (add n m) = add n (suc m) ) addComSuc n m <= rec n { addComSuc n m <= case n { addComSuc zero m => refl addComSuc (suc n) m => eqResp suc (addComSuc n m) } } ------------------------------------------------------------------------------------------------ ( m, n : Nat ! let !------------------------------------! ! addCom m n : (add m n) = (add n m) ) addCom m n <= rec m { addCom m n <= case m { addCom zero n => addComZero n addCom (suc m) n => eqTrans (eqResp suc (addCom m n)) (addComSuc n m) } } ------------------------------------------------------------------------------------------------ ( as : Vec n A ! let !----------------------! ! vrev _n as : Vec n A ) vrev _ n as <= rec as { vrev _ n as <= case as { vrev _ zero vnil => vnil vrev _ (suc n) (vcons a as) => eqSubst (lam i => Vec i A) (addCom n (suc zero)) (vappend (vrev as) (vcons a vnil)) } } ------------------------------------------------------------------------------------------------ inspect vrev v123 => ? : Vec (suc (suc (suc zero))) Nat ------------------------------------------------------------------------------------------------ ( as : Vec n A ; a : A ! let !----------------------------! ! vsnoc as a : Vec (suc n) A ) vsnoc as a <= rec as { vsnoc as a <= case as { vsnoc vnil a => vcons a vnil vsnoc (vcons a as) a' => vcons a (vsnoc as a') } } ------------------------------------------------------------------------------------------------ ( as : Vec n A ! let !--------------------! ! vrev' as : Vec n A ) vrev' as <= rec as { vrev' as <= case as { vrev' vnil => vnil vrev' (vcons a as) => vsnoc (vrev' as) a } } ------------------------------------------------------------------------------------------------ ( m, n : Nat ! ( p : Le m n ! data !------------! where (-----------------! ; !----------------------------! ! Le m n : * ) ! le0 : Le zero n ) ! leS p : Le (suc m) (suc n) ) ------------------------------------------------------------------------------------------------ let (---------------------! ! le23 : Le two three ) le23 => leS (leS le0) ------------------------------------------------------------------------------------------------ ( n : Nat ! let !-------------------! ! leRefl n : Le n n ) leRefl n <= rec n { leRefl n <= case n { leRefl zero => le0 leRefl (suc n) => leS (leRefl n) } } ------------------------------------------------------------------------------------------------ ( p : Le m n ; q : Le n o ! let !--------------------------! ! leTrans p q : Le m o ) leTrans p q <= rec p { leTrans p q <= case p { leTrans le0 q => le0 leTrans (leS p) q <= case q { leTrans (leS p) (leS q) => leS (leTrans p q) } } } ------------------------------------------------------------------------------------------------ ( p : Le m n ; q : Le n m ! let !--------------------------! ! leAntiSym p q : m = n ) leAntiSym p q <= rec q { leAntiSym p q <= case p { leAntiSym le0 q <= case q { leAntiSym le0 le0 => refl } leAntiSym (leS p) q <= case q { leAntiSym (leS p) (leS q) => eqResp suc (leAntiSym p q) } } } ------------------------------------------------------------------------------------------------ ( p : Le (suc m) zero ! let !---------------------! ! lesmz p : Zero ) lesmz p <= case p ------------------------------------------------------------------------------------------------ ( p : Le (suc m) (suc n) ! let !------------------------! ! leSinv p : Le m n ) leSinv p <= case p { leSinv (leS p) => p } ------------------------------------------------------------------------------------------------ ( p : Dec (Le m n) ! let !------------------------------------! ! leSuc p : Dec (Le (suc m) (suc n)) ) leSuc p <= case p { leSuc (left a) => left (leS a) leSuc (right b) => right (lam q => b (leSinv q)) } ------------------------------------------------------------------------------------------------ ( m, n : Nat ! let !-----------------------! ! le m n : Dec (Le m n) ) le m n <= rec m { le m n <= case m { le zero n => left le0 le (suc m) n <= case n { le (suc m) zero => right lesmz le (suc m) (suc n) => leSuc (le m n) } } } ------------------------------------------------------------------------------------------------