-- File: nat -- This file introduces the natural numbers. -- It consists of two parts. -- 1. Axioms, corresponding to Section 4.5 -- 2. Library, corresponding to Section 4.6 -- naming conventions for lemmas: -- variables for Nats are m,n,p Load "lambdaL" Load "logic" Load "bool" ----------------------- ----------------------- -- -- -- 1. A X I O M S -- -- -- ----------------------- ----------------------- Var Nat : *s Var O : Nat Var S : Nat -> Nat Var primrecnat : @B:*s.B->(Nat->B->B)-> Nat -> B Implicit 1 primrecnat Var primrecnat_O : @B:*s.@nv:B.@sv:Nat->B->B. primrecnat nv sv O = nv Var primrecnat_Sm : @B:*s.@nv:B.@sv:Nat->B->B.@m:Nat. primrecnat nv sv (S m) = sv m (primrecnat nv sv m) Var indnat : @P:Nat->*p. (P O) -> (@m:Nat.P m -> P (S m)) -> (@m:Nat.P m) ------------------------- ------------------------- -- -- -- 2. L I B R A R Y -- -- -- ------------------------- ------------------------- ----------------- -- predecessor -- ----------------- Def pred := primrecnat O (\m,n:Nat.m) Prove pred_O : pred O = O Prove pred_Sm : @m:Nat. pred (S m) = m -------------------------------------- -- O and S are different injections -- -------------------------------------- Prove O_is_Sm_ : @m:Nat. Not (O=S m) Prove Sm_is_O_ : @m:Nat. Not (S m=O) Prove Sm_is_Sn_ : @m,n:Nat. S m = S n -> m = n Prove m_is_Sm_ : @m:Nat. Not (m= S m) ------------- -- iternat -- ------------- Def iternat := \B:*s. \nv:B. \sv: B->B. primrecnat nv (\dummy:Nat. sv) : @B:*s.B->(B->B)-> Nat -> B Implicit 1 iternat Prove iternat_O : @B:*s.@nv:B.@sv: B->B. iternat nv sv O = nv Prove iternat_Sm : @B:*s.@nv:B.@sv:B->B.@m:Nat. iternat nv sv (S m) = sv (iternat nv sv m) ---------------------------- -- double induction lemma -- ---------------------------- -- This lemma of double induction will be very useful for proving properties -- about functions that compare two natural numbers in some way. Prove nat_double_ind : @R:Nat->Nat->*p. (@m:Nat.R O m) -> (@m:Nat. R (S m) O) -> (@m,n:Nat. R m n -> R (S m) (S n)) -> (@m,n:Nat. R m n) ------------------- -- less or equal -- ------------------- -- Name in lemmas: Le Def (<=) := \m,n:Nat. @R:Nat->*p. R m -> (@p:Nat. R p -> R (S p)) -> R n Prove Le_refl : @m:Nat. m<=m Prove m_Le_Sn : @m,n:Nat. m<=n -> m<= S n Prove Le_ind : @m:Nat. @P:Nat->*p. P m -> (@n:Nat. m<=n -> P n -> P (S n)) -> @n:Nat. m<=n -> P n Prove O_Le_m : @m:Nat. O <= m Prove Sm_Le_Sn : @m,n:Nat. m <= n -> S m <= S n Prove Le_trans : @m,n,p:Nat. m<=n -> n<=p -> m<=p Prove m_Le_Sm : @m:Nat. m <= S m Prove predm_Le_m : @m:Nat. pred m <= m Prove Sm_Le_Sn_ : @m,n:Nat. S m <= S n -> m <= n Prove Sm_Le_n_ : @m,n:Nat. S m <= n -> m <= n Prove Sm_Le_O_ : @m:Nat. Not (S m <= O) Prove Sm_Le_m_ : @m:Nat. Not (S m <= m) Prove Le_antisym : @m,n:Nat. m<=n -> n<=m -> m=n Prove m_Le_O_ : @m:Nat. m <= O -> m=O --------------- -- Less than -- --------------- -- Name in lemmas: Lt Def (<) := \m,n:Nat. S m <= n Prove m_Lt_n__Sm_Le_n : @m,n:Nat. m<n -> S m <= n Prove Sm_Le_n__m_Lt_n : @m,n:Nat. S m <= n -> m<n -- We try to define the same lemmas, in the same order, as for <=. Prove m_Lt_Sm : @m:Nat. m < S m Prove m_Lt_Sn : @m,n:Nat. m < n -> m < S n Prove O_Lt_Sm : @m:Nat. O < S m Prove Sm_Lt_Sn : @m,n:Nat. m < n -> S m < S n Prove Sm_Lt_Sn_ : @m,n:Nat. S m < S n -> m < n Prove m_Lt_O_ : @m:Nat. Not (m<O) Prove m_Lt_m_ : @m:Nat. Not (m<m) Prove m_Lt_Sn__m_Le_n : @m,n:Nat. m < S n -> m <= n Prove m_Le_n__m_Lt_Sn : @m,n:Nat. m<=n -> m < S n Prove m_Lt_n__m_Le_n : @m,n:Nat. m<n -> m<=n Prove O_nis_m__O_Lt_m : @m:Nat. Not (O=m) -> O<m Prove Lt__nis : @m,n:Nat. m<n -> Not (m=n) Prove Lt_trans : @n,m,p:Nat. m<n -> n<p -> m<p Prove Lt_Le_trans : @n,m,p:Nat. m<n -> n<=p -> m<p Prove Le_Lt_trans : @n,m,p:Nat. m<=n -> n<p -> m<p Prove Le__Lt_Or_is : @m,n:Nat. m<=n -> m<n \/ m=n Prove Le_Or_Gt : @m,n:Nat. m<=n \/ n<m Prove Le__Not_Gt : @m,n:Nat. m<=n -> Not (n<m) Prove Not_Gt__Le : @m,n:Nat. Not (n<m) -> m<=n ----------------------------------- -- boolean comparison of numbers -- ----------------------------------- -- is_zero Def isZero := iternat true (\b:Bool. false) : Nat -> Bool Prove isZero_O : isZero O = true Prove isZero_Sm : @m:Nat. isZero (S m) = false -- leq Def leq := \m,n:Nat. iternat (\m:Nat.isZero m) ( \le_Pn:Nat->Bool. \m:Nat.le_Pn (pred m)) n m: Nat -> Nat -> Bool Prove leq_O_m : @m:Nat. leq O m = true Prove leq_Sm_O : @m:Nat. leq (S m) O = false Prove leq_Sm_Sn : @m,n:Nat. leq (S m) (S n) = leq m n Prove leq_true__Le : @m,n:Nat. leq m n = true -> m <= n Prove Le__leq_true : @m,n:Nat. m <= n -> leq m n = true Prove Gt__leq_false : @m,n:Nat. n < m -> leq m n = false Prove leq_false__Gt : @m,n:Nat. leq m n = false -> n < m