NZAdd.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   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 Import NZAxioms NZBase.

Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).

Hint Rewrite
 pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
Hint Rewrite one_succ two_succ : nz'.
Ltac nzsimpl := autorewrite with nz.
Ltac nzsimpl' := autorewrite with nz nz'.

Theorem add_0_r : forall n, n + 0 == n.forall n : t, n + 0 == n
Proof.forall n : t, n + 0 == n
  nzinduct n.0 + 0 == 0
forall n : t, n + 0 == n <-> S n + 0 == S n
  -0 + 0 == 0 now nzsimpl.
  -forall n : t, n + 0 == n <-> S n + 0 == S n intro.n:t
n + 0 == n <-> S n + 0 == S n nzsimpl.n:t
n + 0 == n <-> S (n + 0) == S n now rewrite succ_inj_wd.
Qed.

Theorem add_succ_r : forall n m, n + S m == S (n + m).forall n m : t, n + S m == S (n + m)
Proof.forall n m : t, n + S m == S (n + m)
  intros n m; nzinduct n.m:t
0 + S m == S (0 + m)
m:t
forall n : t,
n + S m == S (n + m) <-> S n + S m == S (S n + m)
  -m:t
0 + S m == S (0 + m) now nzsimpl.
  -m:t
forall n : t,
n + S m == S (n + m) <-> S n + S m == S (S n + m) intro.m, n:t
n + S m == S (n + m) <-> S n + S m == S (S n + m) nzsimpl.m, n:t
n + S m == S (n + m) <-> S (n + S m) == S (S (n + m)) now rewrite succ_inj_wd.
Qed.

Theorem add_succ_comm : forall n m, S n + m == n + S m.forall n m : t, S n + m == n + S m
Proof.forall n m : t, S n + m == n + S m
intros n m.n, m:t
S n + m == n + S m now rewrite add_succ_r, add_succ_l.
Qed.

Hint Rewrite add_0_r add_succ_r : nz.

Theorem add_comm : forall n m, n + m == m + n.forall n m : t, n + m == m + n
Proof.forall n m : t, n + m == m + n
  intros n m; nzinduct n.m:t
0 + m == m + 0
m:t
forall n : t, n + m == m + n <-> S n + m == m + S n
  -m:t
0 + m == m + 0 now nzsimpl.
  -m:t
forall n : t, n + m == m + n <-> S n + m == m + S n intro.m, n:t
n + m == m + n <-> S n + m == m + S n nzsimpl.m, n:t
n + m == m + n <-> S (n + m) == S (m + n) now rewrite succ_inj_wd.
Qed.

Theorem add_1_l : forall n, 1 + n == S n.forall n : t, 1 + n == S n
Proof.forall n : t, 1 + n == S n
intro n; now nzsimpl'.
Qed.

Theorem add_1_r : forall n, n + 1 == S n.forall n : t, n + 1 == S n
Proof.forall n : t, n + 1 == S n
intro n; now nzsimpl'.
Qed.

Hint Rewrite add_1_l add_1_r : nz.

Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.forall n m p : t, n + (m + p) == n + m + p
Proof.forall n m p : t, n + (m + p) == n + m + p
  intros n m p; nzinduct n.m, p:t
0 + (m + p) == 0 + m + p
m, p:t
forall n : t,
n + (m + p) == n + m + p <->
S n + (m + p) == S n + m + p
  -m, p:t
0 + (m + p) == 0 + m + p now nzsimpl.
  -m, p:t
forall n : t,
n + (m + p) == n + m + p <->
S n + (m + p) == S n + m + p intro.m, p, n:t
n + (m + p) == n + m + p <->
S n + (m + p) == S n + m + p nzsimpl.m, p, n:t
n + (m + p) == n + m + p <->
S (n + (m + p)) == S (n + m + p) now rewrite succ_inj_wd.
Qed.

Theorem add_cancel_l : forall n m p, p + n == p + m <-> n == m.forall n m p : t, p + n == p + m <-> n == m
Proof.forall n m p : t, p + n == p + m <-> n == m
intros n m p; nzinduct p.n, m:t
0 + n == 0 + m <-> n == m
n, m:t
forall n0 : t,
(n0 + n == n0 + m <-> n == m) <->
(S n0 + n == S n0 + m <-> n == m)
-n, m:t
0 + n == 0 + m <-> n == m now nzsimpl.
-n, m:t
forall n0 : t,
(n0 + n == n0 + m <-> n == m) <->
(S n0 + n == S n0 + m <-> n == m) intro p.n, m, p:t
(p + n == p + m <-> n == m) <->
(S p + n == S p + m <-> n == m) nzsimpl.n, m, p:t
(p + n == p + m <-> n == m) <->
(S (p + n) == S (p + m) <-> n == m) now rewrite succ_inj_wd.
Qed.

Theorem add_cancel_r : forall n m p, n + p == m + p <-> n == m.forall n m p : t, n + p == m + p <-> n == m
Proof.forall n m p : t, n + p == m + p <-> n == m
intros n m p.n, m, p:t
n + p == m + p <-> n == m rewrite (add_comm n p), (add_comm m p).n, m, p:t
p + n == p + m <-> n == m apply add_cancel_l.
Qed.

Theorem add_shuffle0 : forall n m p, n+m+p == n+p+m.forall n m p : t, n + m + p == n + p + m
Proof.forall n m p : t, n + m + p == n + p + m
intros n m p.n, m, p:t
n + m + p == n + p + m rewrite <- 2 add_assoc, add_cancel_l.n, m, p:t
m + p == p + m apply add_comm.
Qed.

Theorem add_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q).forall n m p q : t, n + m + (p + q) == n + p + (m + q)
Proof.forall n m p q : t, n + m + (p + q) == n + p + (m + q)
intros n m p q.n, m, p, q:t
n + m + (p + q) == n + p + (m + q) rewrite 2 add_assoc, add_cancel_r.n, m, p, q:t
n + m + p == n + p + m apply add_shuffle0.
Qed.

Theorem add_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p).forall n m p q : t, n + m + (p + q) == n + q + (m + p)
Proof.forall n m p q : t, n + m + (p + q) == n + q + (m + p)
intros n m p q.n, m, p, q:t
n + m + (p + q) == n + q + (m + p) rewrite (add_comm p).n, m, p, q:t
n + m + (q + p) == n + q + (m + p) apply add_shuffle1.
Qed.

Theorem add_shuffle3 : forall n m p, n + (m + p) == m + (n + p).forall n m p : t, n + (m + p) == m + (n + p)
Proof.forall n m p : t, n + (m + p) == m + (n + p)
intros n m p.n, m, p:t
n + (m + p) == m + (n + p) now rewrite add_comm, <- add_assoc, (add_comm p).
Qed.

Theorem sub_1_r : forall n, n - 1 == P n.forall n : t, n - 1 == P n
Proof.forall n : t, n - 1 == P n
intro n; now nzsimpl'.
Qed.

Hint Rewrite sub_1_r : nz.

End NZAddProp.