Library Coq.Numbers.Cyclic.Abstract.NZCyclic
Require Export NZAxioms.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import CyclicAxioms.
A Z/nZ representation given by a module type CyclicType
implements NZAxiomsSig, e.g. the common properties between
N and Z with no ordering. Notice that the n in Z/nZ is
a power of 2.
Module NZCyclicAxiomsMod (Import Cyclic : CyclicType) <: NZAxiomsSig.
Local Open Scope Z_scope.
Definition t := w.
Definition NZ_to_Z : t -> Z := znz_to_Z w_op.
Definition Z_to_NZ : Z -> t := znz_of_Z w_op.
Local Notation wB := (base w_op.(znz_digits)).
Local Notation "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
Definition eq (n m : t) := [| n |] = [| m |].
Definition zero := w_op.(znz_0).
Definition succ := w_op.(znz_succ).
Definition pred := w_op.(znz_pred).
Definition add := w_op.(znz_add).
Definition sub := w_op.(znz_sub).
Definition mul := w_op.(znz_mul).
Local Infix "==" := eq (at level 70).
Local Notation "0" := zero.
Local Notation S := succ.
Local Notation P := pred.
Local Infix "+" := add.
Local Infix "-" := sub.
Local Infix "*" := mul.
Hint Rewrite w_spec.(spec_0) w_spec.(spec_succ) w_spec.(spec_pred)
w_spec.(spec_add) w_spec.(spec_mul) w_spec.(spec_sub) : w.
Ltac wsimpl :=
unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
Ltac wcongruence := repeat red; intros; wsimpl; congruence.
Instance eq_equiv : Equivalence eq.
Instance succ_wd : Proper (eq ==> eq) succ.
Instance pred_wd : Proper (eq ==> eq) pred.
Instance add_wd : Proper (eq ==> eq ==> eq) add.
Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Theorem gt_wB_1 : 1 < wB.
Theorem gt_wB_0 : 0 < wB.
Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
Theorem pred_succ : forall n, P (S n) == n.
Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0.
Section Induction.
Variable A : t -> Prop.
Hypothesis A_wd : Proper (eq ==> iff) A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n, A n <-> A (S n).
Let B (n : Z) := A (Z_to_NZ n).
Lemma B0 : B 0.
Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
Lemma B_holds : forall n : Z, 0 <= n < wB -> B n.
Theorem bi_induction : forall n, A n.
End Induction.
Theorem add_0_l : forall n, 0 + n == n.
Theorem add_succ_l : forall n m, (S n) + m == S (n + m).
Theorem sub_0_r : forall n, n - 0 == n.
Theorem sub_succ_r : forall n m, n - (S m) == P (n - m).
Theorem mul_0_l : forall n, 0 * n == 0.
Theorem mul_succ_l : forall n m, (S n) * m == n * m + m.
End NZCyclicAxiomsMod.