-- File: nat2

-- defines eq, +, and max

Path "../lol"
Load "nat"

--------
-- eq --
--------

Def eq := iternat (\n:Nat. isZero n) (\eq_Pm:Nat->Bool. 
          primrecnat false (\Pn:Nat. \dummy:Bool. eq_Pm Pn))

Prove eq_O_O : eq O O = true
Unfold eq
Rewrite iternat_O
Apply isZero_O
Exit

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

Prove eq_Sm_O : @m:Nat. eq (S m) O = false
Intro
Unfold eq
Rewrite iternat_Sm
Apply primrecnat_O
Exit

Prove eq_Sm_Sn : @m,n:Nat. eq (S m) (S n) = eq m n
Intros
Unfold 1 eq
Rewrite iternat_Sm
Rewrite primrecnat_Sm
Refl
Exit

Prove eq__Eq : @m,n:Nat. eq m n = true -> m=n
Apply nat_double_ind
Apply indnat
Intro
Refl
Intro
Rewrite eq_O_Sm
Intros
FalseE
NotE false_is_true_
Exact H1
Intro
Rewrite eq_Sm_O
Intro
FalseE
Apply false_is_true_ On H
Intros 3
Rewrite eq_Sm_Sn
Intro
Rewrite H
Assumption
Refl
Exit

Prove eq_m_m : @m:Nat. eq m m = true
Apply indnat
Apply eq_O_O
Intros
Rewrite eq_Sm_Sn
Assumption
Exit

Prove eq_m_n : @m,n:Nat. Not (m=n) -> eq m n = false
Intros
OrE exh_bool (eq m n)
Forward eq__Eq On H1
FalseE
NotE H
Assumption
Assumption
Exit

Prove Not_eq__Not_Eq : @m,n:Nat. eq m n = false -> Not (m=n)
Intros
NotI
Cut eq m n = true
Intro
NotE false_is_true_
Lewrite H
Lewrite H2
Refl
Rewrite H1
Apply eq_m_m
Exit


----------
-- plus --
----------

-- Name in lemmas: plus
Def (+) := \m:Nat.\n:Nat. iternat n S m : Nat->Nat->Nat
Infix 5 (+)

Prove O_plus : @n:Nat. O+n = n
Intro n
Unfold (+)
Rewrite iternat_O
Refl
Exit

Prove Sm_plus : @m,n:Nat. S m + n = S (m + n)
Intro m, n
Unfold (+)
Rewrite iternat_Sm
Refl
Exit
    
Prove plus_O : @n:Nat. n+O = n
Apply indnat  

Rewrite O_plus
Refl

Intro n, H
Rewrite Sm_plus
Rewrite H
Refl
Exit

Prove plus_Sm : @m,n:Nat. m + S n = S (m+n)
Intros
Pattern m
Apply indnat
Repeat Rewrite O_plus
Refl
Intros
Repeat Rewrite Sm_plus
Rewrite H
Refl
Exit


Prove plus_comm : @m,n:Nat. m+n = n+m
Intro
Apply indnat
Rewrite plus_O
Rewrite O_plus
Refl
Intro n,H
Rewrite Sm_plus
Rewrite plus_Sm
Rewrite H
Refl
Exit


Prove plus_assoc : @m,n,p:Nat. (m+n)+p = m+(n+p)
Intros
Pattern m
Apply indnat

Repeat Rewrite O_plus
Refl

Intro m2, H
Repeat Rewrite Sm_plus
Rewrite H
Refl
Exit

InfixR 5 (+)


---------
-- max --
---------

Def max := \m,n:Nat. if (leq n m) m n

Prove Le_max1 : @m,n:Nat. m <= max m n 
Intros
Unfold max
OrE exh_bool On leq n m
Rewrite H1
Rewrite if_true
Apply Le_refl
Rewrite H1
Rewrite if_false
Apply m_Lt_n__m_Le_n
Apply leq_false__Gt
Assumption
Exit

Prove max_comm : @m,n:Nat. max m n = max n m
Intros
Unfold max
OrE Le_Or_Gt On m, n
OrE Le__Lt_Or_is On H1
Rewrite Le__leq_true On H1
Rewrite if_true
Rewrite Gt__leq_false On H3
Rewrite if_false
Refl
Repeat Rewrite H3
Refl
Forward m_Lt_n__m_Le_n On H1
Rewrite Le__leq_true On H2
Rewrite if_true
Rewrite Gt__leq_false On H1
Rewrite if_false
Refl
Exit

Prove Le_max2 : @m,n:Nat. n <= max m n 
Intros
Rewrite max_comm
Apply Le_max1
Exit

Prove max_assoc : @m,n,p:Nat. max (max m n) p = max m (max n p)
Intros
Unfold max
OrE exh_bool On leq n m
Repeat Rewrite H1
Repeat Rewrite if_true
OrE exh_bool On leq p n
Repeat Rewrite H3
Repeat Rewrite if_true
Rewrite H1
Rewrite if_true
Forward leq_true__Le On H1
Forward leq_true__Le On H3
Forward Le_trans On H5, H4
Rewrite Le__leq_true On H6
Rewrite if_true
Refl
Repeat Rewrite H3
Repeat Rewrite if_false
Refl
Repeat Rewrite H1
Repeat Rewrite if_false
OrE exh_bool On leq p n
Repeat Rewrite H3
Repeat Rewrite if_true
Rewrite H1
Rewrite if_false
Refl
Repeat Rewrite H3
Repeat Rewrite if_false
Forward leq_false__Gt On H1
Forward leq_false__Gt On H3
Forward Lt_trans On H4, H5
Rewrite Gt__leq_false On H6
Rewrite if_false
Refl
Exit