-- 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