% Various properties of addition for the natural numbers
Import "nats".
Define plus : nat -> nat -> nat -> prop by
plus z N N := nat N
; plus (s M) N (s K) := plus M N K.
Theorem plus_types : forall M N P, plus M N P -> (nat M /\ nat N /\ nat P).
induction on 1. intros. case H1. search. apply IH to H2. search.
Theorem plus_total : forall M N, nat M -> nat N -> exists K, nat K /\ plus M N K.
induction on 1. intros. case H1.
exists N. search.
apply IH to H3 H2. search.
Theorem plus_det : forall A B C D, plus A B C -> plus A B D -> C = D.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
Theorem plus_zero : forall N, nat N -> plus N z N.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_zero_converse : forall N M, plus N z M -> N = M.
induction on 1. intros. case H1. search. apply IH to H2. search.
Theorem plus_succ : forall M N K, plus M N K -> plus M (s N) (s K).
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem plus_comm : forall M N K, plus M N K -> plus N M K.
induction on 1. intros. case H1.
apply plus_zero to H2. search.
apply IH to H2. apply plus_succ to H3. search.
Theorem plus_assoc : forall A B C AB ABC,
plus A B AB -> plus AB C ABC -> exists BC, plus B C BC /\ plus A BC ABC.
induction on 1. intros. apply plus_types to H1. apply plus_types to H2.
case H1. search.
case H2. apply IH to H9 H10.
witness BC. search.
Theorem plus_with_succ_impossible : forall N M, plus (s N) M N -> false.
induction on 1. intros. case H1. apply IH to H2.
Theorem plus_left_cancel : forall A B C D, plus A B C -> plus A D C -> B = D.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. search.
Theorem plus_right_cancel : forall A B C D, plus A B C -> plus D B C -> A = D.
intros. apply plus_comm to H1. apply plus_comm to H2. apply plus_left_cancel to H3 H4. search.
Theorem plus_swaprl : forall A B C, plus A (s B) C -> plus (s A) B C.
induction on 1. intros. case H1. case H2. search. apply IH to H2. search.
Theorem plus_swaplr : forall A B C, plus (s A) B C -> plus A (s B) C.
intros. case H1. apply plus_succ to H2. search.
% Another way to write plus_assoc, using the self-dual notion of functions.
Theorem plus_assoc1 : forall A B C AB ABC BC ABC',
plus A B AB -> plus AB C ABC -> plus B C BC -> plus A BC ABC' -> ABC = ABC'.
intros. apply plus_assoc to H1 H2. apply plus_det to H3 H5. clear H5.
apply plus_det to H4 H6. clear H6. search.
Theorem plus_assoc_rl : forall A B C BC ABC, plus B C BC -> plus A BC ABC ->
exists AB, plus A B AB /\ plus AB C ABC.
intros. apply plus_comm to H1. apply plus_comm to H2. apply plus_assoc to H3 H4.
apply plus_comm to H5. apply plus_comm to H6. search.
% The proof of this presentation involves only plus_comm and plus_assoc only
Theorem plus_assoc_rl1 : forall A B C BC AB ABC ABC',
plus B C BC -> plus A BC ABC -> plus A B AB -> plus AB C ABC' -> ABC = ABC'.
intros. apply plus_comm to H2. apply plus_comm to H1. apply plus_types to H3. apply plus_types to H6.
apply plus_total to H12 H7. apply plus_assoc to H6 H14. apply plus_comm to H15.
apply plus_det to H3 H17. clear H17. apply plus_comm to H16. apply plus_det to H5 H14. clear H14.
apply plus_det to H4 H18. clear H18. search.
% (A + B) + (C + D) = (A + C) + (B + D)
Theorem plus_perm4 : forall A B C D AB CD ABCD, plus A B AB -> plus C D CD ->
plus AB CD ABCD -> exists AC BD, plus A C AC /\ plus B D BD /\ plus AC BD ABCD.
intros. apply plus_assoc_rl to H2 H3. apply plus_assoc to H1 H4. apply plus_comm to H6.
apply plus_assoc_rl to H8 H7. apply plus_assoc to H10 H5. search.
Theorem plus_one : forall N, nat N -> plus N (s z) (s N).
intros. backchain plus_comm.
Theorem plus_zero_only_right_unit : forall N M, plus M N M -> N = z.
intros. apply plus_types to H1. assert plus M z M. backchain plus_zero.
apply plus_left_cancel to H1 H5. search.
Theorem plus_zero_only_left_unit : forall N M, plus N M M -> N = z.
intros. apply plus_comm to H1. apply plus_zero_only_right_unit to H2. search.
Theorem plus_unit_appears : forall N P Q, plus Q N P -> plus P N Q -> N = z.
induction on 1. intros. case H1. case H2. search. case H2. apply IH to H3 H4. search.
Theorem nat_dichotomy : forall N M, nat N -> nat M -> (exists P, plus N P M \/ plus M P N).
induction on 1. induction on 2. intros. case H1.
witness M. left. search.
case H2. witness (s N1). right. search.
apply IH to H3 H4. apply IH1 to H3 H4.
case H5. witness P. left. search. witness P. right. search.
Set search_depth 20.
Query plus (s^2 z) (s^1 z) N.
Query plus (s^3 z) (s^4 z) N.
Set search_depth 5.
