-- 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
Unfold pred
Rewrite primrecnat_O
Refl
Exit

Prove pred_Sm : @m:Nat. pred (S m) = m
Intro m
Unfold pred
Rewrite primrecnat_Sm
Refl
Exit

--------------------------------------
-- O and S are different injections --
--------------------------------------

Prove O_is_Sm_ : @m:Nat. Not (O=S m)
Intro
NotI
Let f := primrecnat false (\dummy:Nat.\b:Bool. true)
NotE false_is_true_
First f O = f (S m)
Rewrite H
Refl
Unfold f
Rewrite primrecnat_O
Rewrite primrecnat_Sm
Intro
Assumption
Exit

Prove Sm_is_O_ : @m:Nat. Not (S m=O)
Intros
NotI
NotE O_is_Sm_ On m
Apply is_sym
Assumption
Exit

Prove Sm_is_Sn_ : @m,n:Nat. S m = S n -> m = n
Intro m, n, H
Lewrite 2 pred_Sm
Lewrite 1 pred_Sm
Rewrite H
Refl
Exit

Prove m_is_Sm_ : @m:Nat. Not (m= S m)
Apply indnat
Apply O_is_Sm_
Intro m, H
Unfold Not
Intro H1
Apply H
Apply Sm_is_Sn_
Assumption
Exit

-------------
-- 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
Intros
Unfold iternat
Apply primrecnat_O
Exit

Prove iternat_Sm : @B:*s.@nv:B.@sv:B->B.@m:Nat. 
                       iternat nv sv (S m) = sv (iternat nv sv m)
Intros
Unfold iternat
Apply primrecnat_Sm
Exit

----------------------------
-- 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)
Intro R, H, H1, H2
Apply indnat
Assumption
Intro m, H3
Apply indnat
Apply H1
Intros
Apply H2
Apply H3
Exit


-------------------
-- 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
Unfold (<=)
Intro m, R, H1, H2 Then Assumption
Exit

Prove m_Le_Sn : @m,n:Nat. m<=n -> m<= S n
Intro m, n, H
Unfold (<=)
Intro R, H1, H2
Apply H2
Apply H Then Assumption
Exit

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
Intros
Apply H2 (\q:Nat. m<=q /\ P q)
Focus 3 
Intros Then Assumption
AndI
Apply Le_refl
Assumption
Intros
AndE H3
AndI
Apply m_Le_Sn
Assumption
Apply H1
Assumption
Assumption
Exit

Prove O_Le_m : @m:Nat. O <= m
Apply indnat
Apply Le_refl
Intro n, H
Apply m_Le_Sn
Assumption
Exit

Prove Sm_Le_Sn : @m,n:Nat. m <= n -> S m <= S n
Intro m, n, H
Pattern n
Apply H
Apply Le_refl
Intro p, H1
Apply m_Le_Sn
Assumption
Exit

Prove Le_trans : @m,n,p:Nat. m<=n -> n<=p -> m<=p
Intro m, n, p, H1, H2
Apply H2
Assumption
Intro p', H3
Apply m_Le_Sn
Assumption
Exit

Prove m_Le_Sm : @m:Nat. m <= S m
Intro m
Apply m_Le_Sn
Apply Le_refl
Exit

Prove predm_Le_m : @m:Nat. pred m <= m
Apply indnat
Rewrite pred_O
Apply Le_refl
Intro m, H
Rewrite pred_Sm
Apply m_Le_Sm
Exit

Prove Sm_Le_Sn_ : @m,n:Nat. S m <= S n -> m <= n
Intro m,n,H
Lewrite 2 pred_Sm
Lewrite pred_Sm
Pattern S n
Apply H
Apply Le_refl
Intro p,H1
Apply Le_trans On H1
Rewrite pred_Sm
Apply predm_Le_m
Exit

Prove Sm_Le_n_ : @m,n:Nat. S m <= n -> m <= n
Intro m, n, H
Apply Le_trans On H
Apply m_Le_Sm
Exit

Prove Sm_Le_O_ : @m:Nat. Not (S m <= O)
Intro Then NotI
Let R := \m:Nat. Not (O=m)
Cut R O
Unfold R Then Intro H1
NotE H1
Refl
Apply H
Unfold R
Apply O_is_Sm_
Intro p, H1
Unfold R
Apply O_is_Sm_
Exit

Prove Sm_Le_m_ : @m:Nat. Not (S m <= m)
Apply indnat
Apply Sm_Le_O_
Intro m, H
NotI
Apply H
Apply Sm_Le_Sn_
Assumption
Exit

Prove Le_antisym : @m,n:Nat. m<=n -> n<=m -> m=n
Intro m,n,H
Apply H
Intro Then Refl
Intro p,H1,H2
FalseE
Apply Sm_Le_m_ p
Apply Le_trans On H2
Forward Sm_Le_n_ On H2
Forward H1 On H3
Rewrite H4
Apply Le_refl
Exit

Prove m_Le_O_ : @m:Nat. m <= O -> m=O
Intro m, H
Apply Le_antisym Then Try Assumption
Apply O_Le_m
Exit

---------------
-- 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
Intros
Assumption
Exit

Prove Sm_Le_n__m_Lt_n : @m,n:Nat. S m <= n -> m<n
Intros
Assumption
Exit

-- We try to define the same lemmas, in the same order, as for <=.

Prove m_Lt_Sm : @m:Nat. m < S m
Unfold (<)
Intro
Apply Sm_Le_Sn
Apply Le_refl
Exit

Prove m_Lt_Sn : @m,n:Nat. m < n -> m < S n
Intros
Unfold (<)
Apply m_Le_Sn
Assumption
Exit

Prove O_Lt_Sm : @m:Nat. O < S m
Unfold (<)
Intro
Apply Sm_Le_Sn
Apply O_Le_m
Exit

Prove Sm_Lt_Sn : @m,n:Nat. m < n -> S m < S n
Unfold (<)
Intros
Apply Sm_Le_Sn
Assumption
Exit

Prove Sm_Lt_Sn_ :  @m,n:Nat. S m < S n -> m < n
Unfold (<)
Intros
Apply Sm_Le_Sn_
Assumption
Exit

Prove m_Lt_O_ : @m:Nat. Not (m<O)
Intro
Unfold (<)
Apply Sm_Le_O_
Exit

Prove m_Lt_m_ : @m:Nat. Not (m<m)
Exact Sm_Le_m_
Exit

Prove m_Lt_Sn__m_Le_n : @m,n:Nat. m < S n -> m <= n
Intros
Apply Sm_Le_Sn_
Assumption
Exit

Prove m_Le_n__m_Lt_Sn : @m,n:Nat. m<=n -> m < S n
Intros
Unfold (<)
Apply Sm_Le_Sn
Assumption
Exit

Prove m_Lt_n__m_Le_n : @m,n:Nat. m<n -> m<=n
Intros
Apply Sm_Le_n_
Assumption
Exit


Prove O_nis_m__O_Lt_m : @m:Nat. Not (O=m) -> O<m
Apply indnat
Intro
FalseE
Apply H
Refl
Intros
Apply O_Lt_Sm
Exit

Prove Lt__nis : @m,n:Nat. m<n -> Not (m=n)
Intros
NotI
Unfold (<) In H
NotE Sm_Le_m_ On m
Rewrite 2 H1
Assumption
Exit

Prove Lt_trans : @n,m,p:Nat. m<n -> n<p -> m<p
Unfold (<)
Intros
Apply Le_trans On H
Apply Sm_Le_n_
Assumption
Exit

Prove Lt_Le_trans : @n,m,p:Nat. m<n -> n<=p -> m<p
Unfold (<)
Intros
Apply Le_trans On H
Assumption
Exit

Prove Le_Lt_trans : @n,m,p:Nat. m<=n -> n<p -> m<p
Unfold (<)
Intros
Apply Le_trans On H1
Apply Sm_Le_Sn
Assumption
Exit

Prove Le__Lt_Or_is : @m,n:Nat. m<=n -> m<n \/ m=n
Intro
Apply Le_ind
OrIR
Refl
Intros
OrIL
OrE H1
Apply m_Lt_Sn
Assumption
Rewrite H2
Apply m_Lt_Sm
Exit

Prove Le_Or_Gt : @m,n:Nat. m<=n \/ n<m
Apply nat_double_ind
Intro
OrIL
Apply O_Le_m
Intro
OrIR
Apply O_Lt_Sm
Intros
OrE H
OrIL
Apply Sm_Le_Sn
Assumption
OrIR
Apply Sm_Lt_Sn
Assumption
Exit

Prove Le__Not_Gt : @m,n:Nat. m<=n -> Not (n<m)
Apply nat_double_ind
Intros
Apply m_Lt_O_
Intros
FalseE
Apply Sm_Le_O_ On H
Intros
NotI
NotE H
Apply Sm_Le_Sn_
Assumption
Apply Sm_Lt_Sn_
Assumption
Exit

Prove Not_Gt__Le : @m,n:Nat.  Not (n<m) -> m<=n
Apply nat_double_ind
Intros
Apply O_Le_m
Intros
FalseE
NotE H
Apply O_Lt_Sm
Intros
Apply Sm_Le_Sn
Apply H
NotI
NotE H1
Apply Sm_Lt_Sn
Assumption
Exit

-----------------------------------
-- boolean comparison of numbers --
-----------------------------------

-- is_zero

Def isZero := iternat true (\b:Bool. false) : Nat -> Bool

Prove isZero_O : isZero O = true
Unfold isZero
Apply iternat_O
Exit

Prove isZero_Sm : @m:Nat. isZero (S m) = false
Intro
Unfold isZero
Apply iternat_Sm
Exit

-- 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
Unfold leq
Apply indnat
Rewrite iternat_O
Apply isZero_O
Intros
Rewrite iternat_Sm
Rewrite pred_O
Assumption
Exit

Prove leq_Sm_O : @m:Nat. leq (S m) O = false
Intro
Unfold leq
Rewrite iternat_O
Apply isZero_Sm
Exit

Prove leq_Sm_Sn : @m,n:Nat. leq (S m) (S n) = leq m n
Intros
Unfold 1 leq
Rewrite iternat_Sm
Rewrite pred_Sm
Refl
Exit


Prove leq_true__Le : @m,n:Nat. leq m n = true -> m <= n
Apply nat_double_ind
Intros
Apply O_Le_m
Intros
FalseE
NotE false_is_true_
Lewrite H
Rewrite leq_Sm_O
Refl
Intros
Apply Sm_Le_Sn
Apply H
Lewrite H1
Rewrite leq_Sm_Sn
Refl
Exit

Prove Le__leq_true : @m,n:Nat. m <= n -> leq m n = true
Apply nat_double_ind
Intros
Apply leq_O_m
Intros
FalseE
Apply Sm_Le_O_ On H
Intros
Rewrite leq_Sm_Sn
Apply H
Apply Sm_Le_Sn_
Assumption
Exit

Prove Gt__leq_false : @m,n:Nat. n < m -> leq m n = false
Intros
OrE exh_bool On leq m n Then Try Assumption
Forward leq_true__Le On H2
FalseE
Apply Le__Not_Gt On H3
Assumption
Exit

Prove leq_false__Gt : @m,n:Nat. leq m n = false -> n < m
Intros
Apply classic
NotI
Forward Not_Gt__Le On H1
Forward Le__leq_true On H2
NotE false_is_true_
Lewrite H
Lewrite H3
Refl
Exit