NZMul.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 NZAdd.

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

Theorem mul_0_r : forall n, n * 0 == 0.forall n : t, n * 0 == 0
Proof.forall n : t, n * 0 == 0
nzinduct n; intros; now nzsimpl.
Qed.

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

Hint Rewrite mul_0_r mul_succ_r : nz.

Theorem mul_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 <-> n * m + m == m * n + m now rewrite add_cancel_r.
Qed.

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

Theorem mul_add_distr_l : forall n m p, n * (m + p) == n * m + n * p.forall n m p : t, n * (m + p) == n * m + n * p
Proof.forall n m p : t, n * (m + p) == n * m + n * p
intros n m p.n, m, p:t
n * (m + p) == n * m + n * p
rewrite (mul_comm n (m + p)), (mul_comm n m), (mul_comm n p).n, m, p:t
(m + p) * n == m * n + p * n
apply mul_add_distr_r.
Qed.

Theorem mul_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 n.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 <->
n * (m * p) + m * p == (n * m + m) * p rewrite mul_add_distr_r.m, p, n:t
n * (m * p) == n * m * p <->
n * (m * p) + m * p == n * m * p + m * p
    now rewrite add_cancel_r.
Qed.

Theorem mul_1_l : forall n, 1 * n == n.forall n : t, 1 * n == n
Proof.forall n : t, 1 * n == n
intro n.n:t
1 * n == n now nzsimpl'.
Qed.

Theorem mul_1_r : forall n, n * 1 == n.forall n : t, n * 1 == n
Proof.forall n : t, n * 1 == n
intro n.n:t
n * 1 == n now nzsimpl'.
Qed.

Hint Rewrite mul_1_l mul_1_r : nz.

Theorem mul_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 now rewrite <- 2 mul_assoc, (mul_comm m).
Qed.

Theorem mul_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) now rewrite 2 mul_assoc, (mul_shuffle0 n).
Qed.

Theorem mul_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 (mul_comm p).n, m, p, q:t
n * m * (q * p) == n * q * (m * p) apply mul_shuffle1.
Qed.

Theorem mul_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 mul_assoc, (mul_comm n), mul_assoc.
Qed.

End NZMulProp.