--------------------------------------------------------------------------------------- ( 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 --------------------------------------------------------------------------------------- data (----------! where (-------------! ; (--------------! ! Bool : * ) ! true : Bool ) ! false : Bool ) --------------------------------------------------------------------------------------- ( b : Bool ! let !--------------! ! not b : Bool ) not b <= case b { not true => false not false => true } --------------------------------------------------------------------------------------- ( a, b : A ; p : a = b ! let !-----------------------! ! sym p : b = a ) sym p <= case p { sym refl => refl } --------------------------------------------------------------------------------------- ( a, b, c : A ; p : a = b ; q : b = c ! let !---------------------------------------! ! trans p q : a = c ) trans p q <= case p { trans 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 } --------------------------------------------------------------------------------------- ( 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 --------------------------------------------------------------------------------------- inspect three => suc (suc (suc zero)) : Nat --------------------------------------------------------------------------------------- ( n : Nat ! let !---------------! ! even n : Bool ) even n <= rec n { even n <= case n { even zero => true even (suc n) => not (even n) } } --------------------------------------------------------------------------------------- let (---------------! ! absurd : Zero ) absurd => absurd --------------------------------------------------------------------------------------- inspect absurd => ? : Zero --------------------------------------------------------------------------------------- ( 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) } } --------------------------------------------------------------------------------------- inspect add two three => suc (suc (suc (suc (suc zero)))) : Nat --------------------------------------------------------------------------------------- ( m, n : Nat ! let !----------------! ! mult m n : Nat ) mult m n <= rec m { mult m n <= case m { mult zero n => zero mult (suc m) n => add (mult m n) n } } --------------------------------------------------------------------------------------- inspect mult two three => suc (suc (suc (suc (suc (suc zero))))) : Nat --------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! exp m n : Nat ) exp m n <= rec n { exp m n <= case n { exp m zero => one exp m (suc n) => mult (exp m n) m } } --------------------------------------------------------------------------------------- inspect exp two three => suc (suc (suc (suc (suc (suc (suc (suc zero))))))) : Nat --------------------------------------------------------------------------------------- inspect exp three two => suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) : Nat --------------------------------------------------------------------------------------- ( m, n : Nat ! let !---------------! ! ack m n : Nat ) ack m n <= rec m { ack m n <= case m { ack zero n => suc n ack (suc m) n <= rec n { ack (suc m) n <= case n { ack (suc m) zero => ack m one ack (suc m) (suc n) => ack m (ack (suc m) n) } } } } --------------------------------------------------------------------------------------- inspect ack two two => suc (suc (suc (suc (suc (suc (suc zero)))))) : Nat --------------------------------------------------------------------------------------- inspect ack three three => suc % (suc ! !% (suc !! ! !% (suc !!! ! ! !% (suc !!!! ! ! ! !% (suc !!!!! ! ! ! ! !% (suc !!!!!! ! ! ! ! ! !% (suc !!!!!!! ! ! ! ! ! ! !% (suc !!!!!!!! ! ! ! ! ! ! ! !% (suc !!!!!!!!! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% (suc !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! !% zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) : Nat --------------------------------------------------------------------------------------- ( n : Nat ! let !-------------------------------! ! addZeroLem n : n = add n zero ) addZeroLem n <= rec n { addZeroLem n <= case n { addZeroLem zero => refl addZeroLem (suc n) => eqResp suc (addZeroLem n) } } --------------------------------------------------------------------------------------- ( m, n : Nat ! let !-----------------------------------------------! ! addSucLem m n : suc (add m n) = add m (suc n) ) addSucLem m n <= rec m { addSucLem m n <= case m { addSucLem zero n => refl addSucLem (suc m) n => eqResp suc (addSucLem m n) } } --------------------------------------------------------------------------------------- ( 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 => addZeroLem n addCom (suc m) n => trans (eqResp suc (addCom m n)) (addSucLem n m) } } --------------------------------------------------------------------------------------- inspect (addCom two three) => refl : suc (suc (suc (suc (suc zero)))) = suc (suc (suc (suc (suc zero)))) --------------------------------------------------------------------------------------- ( m, n : Nat ! let !----------------! ! eqn m n : Bool ) eqn m n <= rec m { eqn m n <= case m { eqn zero n <= case n { eqn zero zero => true eqn zero (suc n) => false } eqn (suc m) n <= case n { eqn (suc m) zero => false eqn (suc m) (suc n) => eqn m n } } } --------------------------------------------------------------------------------------- inspect (eqn two three) => false : Bool --------------------------------------------------------------------------------------- inspect (eqn two two) => true : Bool --------------------------------------------------------------------------------------- ( P : * ! let !-----------! ! Dec P : * ) Dec P => Or P (Not P) --------------------------------------------------------------------------------------- ( m, n : Nat ! let !------------------------! ; eqn' m n [] ! eqn' m n : Dec (m = n) ) ---------------------------------------------------------------------------------------