(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Export NBase.

Module NAddProp (Import N : NAxiomsMiniSig').
Include NBaseProp N.

Theorem eq_add_0 : forall n m, n + m == 0 <-> n == 0 /\ m == 0.
forall n m : t, n + m == 0 <-> n == 0 /\ m == 0
Proof.
forall n m : t, n + m == 0 <-> n == 0 /\ m == 0
intros n m; induct n.
m:t
0 + m == 0 <-> 0 == 0 /\ m == 0
m:t
forall n : t,
n + m == 0 <-> n == 0 /\ m == 0 ->
S n + m == 0 <-> S n == 0 /\ m == 0
nzsimpl; intuition.
m:t
forall n : t,
n + m == 0 <-> n == 0 /\ m == 0 ->
S n + m == 0 <-> S n == 0 /\ m == 0
intros n IH.
m, n:t
IH:n + m == 0 <-> n == 0 /\ m == 0
S n + m == 0 <-> S n == 0 /\ m == 0 nzsimpl.
m, n:t
IH:n + m == 0 <-> n == 0 /\ m == 0
S (n + m) == 0 <-> S n == 0 /\ m == 0
setoid_replace (S (n + m) == 0) with False by
 (apply neg_false; apply neq_succ_0).
m, n:t
IH:n + m == 0 <-> n == 0 /\ m == 0
False <-> S n == 0 /\ m == 0
setoid_replace (S n == 0) with False by
 (apply neg_false; apply neq_succ_0).
m, n:t
IH:n + m == 0 <-> n == 0 /\ m == 0
False <-> False /\ m == 0 tauto.
Qed.

Theorem eq_add_succ :
  forall n m, (exists p, n + m == S p) <->
              (exists n', n == S n') \/ (exists m', m == S m').
forall n m : t,
(exists p : t, n + m == S p) <->
(exists n' : t, n == S n') \/
(exists m' : t, m == S m')
Proof.
forall n m : t,
(exists p : t, n + m == S p) <->
(exists n' : t, n == S n') \/
(exists m' : t, m == S m')
intros n m; cases n.
m:t
(exists p : t, 0 + m == S p) <->
(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
split; intro H.
m:t
H:exists p : t, 0 + m == S p
(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
m:t
H:(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
exists p : t, 0 + m == S p
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
destruct H as [p H].
m, p:t
H:0 + m == S p
(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
m:t
H:(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
exists p : t, 0 + m == S p
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m') rewrite add_0_l in H; right; now exists p.
m:t
H:(exists n' : t, 0 == S n') \/
(exists m' : t, m == S m')
exists p : t, 0 + m == S p
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
destruct H as [[n' H] | [m' H]].
m, n':t
H:0 == S n'
exists p : t, 0 + m == S p
m, m':t
H:m == S m'
exists p : t, 0 + m == S p
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
symmetry in H; false_hyp H neq_succ_0.
m, m':t
H:m == S m'
exists p : t, 0 + m == S p
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
exists m'; now rewrite add_0_l.
m:t
forall n : t,
(exists p : t, S n + m == S p) <->
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
intro n; split; intro H.
m, n:t
H:exists p : t, S n + m == S p
(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
m, n:t
H:(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
exists p : t, S n + m == S p
left; now exists n.
m, n:t
H:(exists n' : t, S n == S n') \/
(exists m' : t, m == S m')
exists p : t, S n + m == S p
exists (n + m); now rewrite add_succ_l.
Qed.

Theorem eq_add_1 : forall n m,
  n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
forall n m : t,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1
Proof.
forall n m : t,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1
intros n m.
n, m:t
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1 rewrite one_succ.
n, m:t
n + m == S 0 ->
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0 intro H.
n, m:t
H:n + m == S 0
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
assert (H1 : exists p, n + m == S p) by now exists 0.
n, m:t
H:n + m == S 0
H1:exists p : t, n + m == S p
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
apply eq_add_succ in H1.
n, m:t
H:n + m == S 0
H1:(exists n' : t, n == S n') \/
(exists m' : t, m == S m')
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0 destruct H1 as [[n' H1] | [m' H1]].
n, m:t
H:n + m == S 0
n':t
H1:n == S n'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
left.
n, m:t
H:n + m == S 0
n':t
H1:n == S n'
n == S 0 /\ m == 0
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0 rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
n, m, n':t
H:n' + m == 0
H1:n == S n'
n == S 0 /\ m == 0
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
apply eq_add_0 in H.
n, m, n':t
H:n' == 0 /\ m == 0
H1:n == S n'
n == S 0 /\ m == 0
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0 destruct H as [H2 H3]; rewrite H2 in H1; now split.
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == S 0 /\ m == 0 \/ n == 0 /\ m == S 0
right.
n, m:t
H:n + m == S 0
m':t
H1:m == S m'
n == 0 /\ m == S 0 rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
n, m, m':t
H:n + m' == 0
H1:m == S m'
n == 0 /\ m == S 0
apply eq_add_0 in H.
n, m, m':t
H:n == 0 /\ m' == 0
H1:m == S m'
n == 0 /\ m == S 0 destruct H as [H2 H3]; rewrite H3 in H1; now split.
Qed.

Theorem succ_add_discr : forall n m, m ~= S (n + m).
forall n m : t, m ~= S (n + m)
Proof.
forall n m : t, m ~= S (n + m)
intro n; induct m.
n:t
0 ~= S (n + 0)
n:t
forall n0 : t,
n0 ~= S (n + n0) -> S n0 ~= S (n + S n0)
apply neq_sym.
n:t
S (n + 0) ~= 0
n:t
forall n0 : t,
n0 ~= S (n + n0) -> S n0 ~= S (n + S n0) apply neq_succ_0.
n:t
forall n0 : t,
n0 ~= S (n + n0) -> S n0 ~= S (n + S n0)
intros m IH H.
n, m:t
IH:m ~= S (n + m)
H:S m == S (n + S m)
False apply succ_inj in H.
n, m:t
IH:m ~= S (n + m)
H:m == n + S m
False rewrite add_succ_r in H.
n, m:t
IH:m ~= S (n + m)
H:m == S (n + m)
False
unfold not in IH; now apply IH.
Qed.

Theorem add_pred_l : forall n m, n ~= 0 -> P n + m == P (n + m).
forall n m : t, n ~= 0 -> P n + m == P (n + m)
Proof.
forall n m : t, n ~= 0 -> P n + m == P (n + m)
intros n m; cases n.
m:t
0 ~= 0 -> P 0 + m == P (0 + m)
m:t
forall n : t, S n ~= 0 -> P (S n) + m == P (S n + m)
intro H; now elim H.
m:t
forall n : t, S n ~= 0 -> P (S n) + m == P (S n + m)
intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ.
Qed.

Theorem add_pred_r : forall n m, m ~= 0 -> n + P m == P (n + m).
forall n m : t, m ~= 0 -> n + P m == P (n + m)
Proof.
forall n m : t, m ~= 0 -> n + P m == P (n + m)
intros n m H; rewrite (add_comm n (P m));
rewrite (add_comm n m); now apply add_pred_l.
Qed.

End NAddProp.