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.
Open Local Scope Z_scope.
Definition NZ := w.
Definition NZ_to_Z : NZ -> Z := znz_to_Z w_op.
Definition Z_to_NZ : Z -> NZ := znz_of_Z w_op.
Notation Local wB := (base w_op.(znz_digits)).
Notation Local "[| x |]" := (w_op.(znz_to_Z) x) (at level 0, x at level 99).
Definition NZeq (n m : NZ) := [| n |] = [| m |].
Definition NZ0 := w_op.(znz_0).
Definition NZsucc := w_op.(znz_succ).
Definition NZpred := w_op.(znz_pred).
Definition NZadd := w_op.(znz_add).
Definition NZsub := w_op.(znz_sub).
Definition NZmul := w_op.(znz_mul).
Theorem NZeq_equiv : equiv NZ NZeq.
Add Relation NZ NZeq
reflexivity proved by (proj1 NZeq_equiv)
symmetry proved by (proj2 (proj2 NZeq_equiv))
transitivity proved by (proj1 (proj2 NZeq_equiv))
as NZeq_rel.
Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd.
Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd.
Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd.
Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd.
Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd.
Delimit Scope IntScope with Int.
Open Local Scope IntScope.
Notation "x == y" := (NZeq x y) (at level 70) : IntScope.
Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope.
Notation "0" := NZ0 : IntScope.
Notation S x := (NZsucc x).
Notation P x := (NZpred x).
Notation "x + y" := (NZadd x y) : IntScope.
Notation "x - y" := (NZsub x y) : IntScope.
Notation "x * y" := (NZmul x y) : IntScope.
Theorem gt_wB_1 : 1 < wB.
Theorem gt_wB_0 : 0 < wB.
Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |].
Theorem NZpred_succ : forall n : NZ, P (S n) == n.
Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int.
Section Induction.
Variable A : NZ -> Prop.
Hypothesis A_wd : predicate_wd NZeq A.
Hypothesis A0 : A 0.
Hypothesis AS : forall n : NZ, A n <-> A (S n).
Add Morphism A with signature NZeq ==> iff as A_morph.
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 NZinduction : forall n : NZ, A n.
End Induction.
Theorem NZadd_0_l : forall n : NZ, 0 + n == n.
Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m).
Theorem NZsub_0_r : forall n : NZ, n - 0 == n.
Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m).
Theorem NZmul_0_l : forall n : NZ, 0 * n == 0.
Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m.
End NZCyclicAxiomsMod.