Import "plus".
Define times : nat -> nat -> nat -> prop by
times z N z := nat N
; times (s M) N P := exists Q, times M N Q /\ plus N Q P.
Set search_depth 200.
Query times z (s^3 z) N.
Query times (s^3 z) z N.
Query times (s^2 z) (s^3 z) N.
Query times (s^5 z) (s^5 z) N.
Set search_depth 5.
Theorem times_types : forall M N P, times M N P -> (nat M /\ nat N /\ nat P).
induction on 1. intros. case H1. search.
apply IH to H2. apply plus_types to H3. search.
Theorem times_total : forall N M, nat N -> nat M -> exists P, times N M P.
induction on 1. intros. case H1.
witness z. unfold. search.
apply IH to H3 H2. apply times_types to H4. apply plus_total to H6 H7.
witness K. unfold. witness P. search.
Theorem times_det : forall M N P Q, times M N P -> times M N Q -> P = Q.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H5. apply plus_det to H4 H6. search.
Theorem times_zero : forall N M, nat N -> times N z M -> M = z.
induction on 1. intros. case H1.
case H2. search.
case H2. apply IH to H3 H4. case H5. search.
Theorem times_zero1 : forall N, nat N -> times N z z.
induction on 1. intros. case H1.
search. apply IH to H2. unfold. witness z. search.
Theorem plus_zero2 : forall M N, plus N z M -> N = M.
induction on 1. intros. case H1. search. apply IH to H2. search.
Theorem times_one : forall M, nat M -> times M (s z) M.
induction on 1. intros. case H1. search. apply IH to H2. unfold. witness N. search.
Theorem plus_double_times_2 : forall M N, nat M -> plus M M N -> times (s (s z)) M N.
induction on 1. intros. case H1. case H2. search.
case H2. apply plus_comm to H4. case H5. apply IH to H3 H6. unfold. witness (s N1). split.
unfold. witness z. split. search. backchain plus_comm. search.
Theorem plus_half_det_aux : forall P Q R, nat P -> nat Q -> plus P P R -> plus Q Q R -> P = Q.
induction on 1. induction on 2. intros. case H1. case H3. case H4. search.
case H2. case H4. case H3. case H3. case H4. apply plus_comm to H7.
apply plus_comm to H8. case H9. case H10.
apply IH1 to H5 H6 H11 H12. search.
Theorem plus_half_det : forall P Q R, plus P P R -> plus Q Q R -> P = Q.
intros. apply plus_types to H1. clear H4. apply plus_types to H2. clear H7.
apply plus_half_det_aux to H3 H6 H1 H2. search.
Theorem times_2_is_double : forall M P, times (s (s z)) M P -> plus M M P.
intros. case H1. case H2. case H4. apply plus_comm to H5. case H7. search.
Theorem double_cancel_left : forall M M' P, times (s (s z)) M P -> times (s (s z)) M' P -> M = M'.
intros. apply times_2_is_double to H1. apply times_2_is_double to H2.
apply plus_half_det to H3 H4. search.
Theorem times_succ : forall M N MN, times M N MN -> exists K, nat K /\ plus MN M K /\ times M (s N) K.
induction on 1. intros. apply times_types to H1. case H1. search.
apply IH to H5.
apply plus_total to H4 H2. witness K1. split. search. search.
fchain 2 plus_comm plus_det.
case H14. unfold. witness K. split. search. unfold.
apply plus_swaprl to H11. case H16.
fchain 3 plus_assoc plus_comm plus_det plus_left_cancel plus_right_cancel.
search.
Theorem times_comm : forall M N K, times M N K -> times N M K.
induction on 1. intros. apply times_types to H1. case H1.
apply times_zero1 to H3. search.
case H2. apply times_types to H5.
apply IH to H5.
fchain plus_comm.
apply times_succ to H11.
fchain 2 plus_comm plus_det. search.
% Distributivity of multiplication over addition. First, a simple
% theorem: inversion on one of the clauses defining times.
Theorem times_incr : forall A B AB ABB, nat ABB ->
times A B AB -> plus AB B ABB -> times (s A) B ABB.
intros. unfold. witness AB. split. search. backchain plus_comm.
Theorem times_distrib : forall X Y Z YpZ T, nat X -> plus Y Z YpZ -> times X YpZ T ->
exists XtY XtZ, nat XtY /\ nat XtZ /\ times X Y XtY /\ times X Z XtZ /\ plus XtY XtZ T.
induction on 1. intros. apply plus_types to H2. apply times_types to H3. case H1.
case H3. search.
case H3. apply plus_types to H12. clear H15.
fchain IH. fchain plus_perm4. fchain plus_types times_types. search.
