diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 375 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 236 |
2 files changed, 611 insertions, 0 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v new file mode 100644 index 00000000..528d78c3 --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -0,0 +1,375 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(* $Id: CyclicAxioms.v 11012 2008-05-28 16:34:43Z letouzey $ *) + +(** * Signature and specification of a bounded integer structure *) + +(** This file specifies how to represent [Z/nZ] when [n=2^d], + [d] being the number of digits of these bounded integers. *) + +Set Implicit Arguments. + +Require Import ZArith. +Require Import Znumtheory. +Require Import BigNumPrelude. +Require Import DoubleType. + +Open Local Scope Z_scope. + +(** First, a description via an operator record and a spec record. *) + +Section Z_nZ_Op. + + Variable znz : Type. + + Record znz_op := mk_znz_op { + + (* Conversion functions with Z *) + znz_digits : positive; + znz_zdigits: znz; + znz_to_Z : znz -> Z; + znz_of_pos : positive -> N * znz; (* Euclidean division by [2^digits] *) + znz_head0 : znz -> znz; (* number of digits 0 in front of the number *) + znz_tail0 : znz -> znz; (* number of digits 0 at the bottom of the number *) + + (* Basic numbers *) + znz_0 : znz; + znz_1 : znz; + znz_Bm1 : znz; (* [2^digits-1], which is equivalent to [-1] *) + + (* Comparison *) + znz_compare : znz -> znz -> comparison; + znz_eq0 : znz -> bool; + + (* Basic arithmetic operations *) + znz_opp_c : znz -> carry znz; + znz_opp : znz -> znz; + znz_opp_carry : znz -> znz; (* the carry is known to be -1 *) + + znz_succ_c : znz -> carry znz; + znz_add_c : znz -> znz -> carry znz; + znz_add_carry_c : znz -> znz -> carry znz; + znz_succ : znz -> znz; + znz_add : znz -> znz -> znz; + znz_add_carry : znz -> znz -> znz; + + znz_pred_c : znz -> carry znz; + znz_sub_c : znz -> znz -> carry znz; + znz_sub_carry_c : znz -> znz -> carry znz; + znz_pred : znz -> znz; + znz_sub : znz -> znz -> znz; + znz_sub_carry : znz -> znz -> znz; + + znz_mul_c : znz -> znz -> zn2z znz; + znz_mul : znz -> znz -> znz; + znz_square_c : znz -> zn2z znz; + + (* Special divisions operations *) + znz_div21 : znz -> znz -> znz -> znz*znz; + znz_div_gt : znz -> znz -> znz * znz; (* specialized version of [znz_div] *) + znz_div : znz -> znz -> znz * znz; + + znz_mod_gt : znz -> znz -> znz; (* specialized version of [znz_mod] *) + znz_mod : znz -> znz -> znz; + + znz_gcd_gt : znz -> znz -> znz; (* specialized version of [znz_gcd] *) + znz_gcd : znz -> znz -> znz; + (* [znz_add_mul_div p i j] is a combination of the [(digits-p)] + low bits of [i] above the [p] high bits of [j]: + [znz_add_mul_div p i j = i*2^p+j/2^(digits-p)] *) + znz_add_mul_div : znz -> znz -> znz -> znz; + (* [znz_pos_mod p i] is [i mod 2^p] *) + znz_pos_mod : znz -> znz -> znz; + + znz_is_even : znz -> bool; + (* square root *) + znz_sqrt2 : znz -> znz -> znz * carry znz; + znz_sqrt : znz -> znz }. + +End Z_nZ_Op. + +Section Z_nZ_Spec. + Variable w : Type. + Variable w_op : znz_op w. + + Let w_digits := w_op.(znz_digits). + Let w_zdigits := w_op.(znz_zdigits). + Let w_to_Z := w_op.(znz_to_Z). + Let w_of_pos := w_op.(znz_of_pos). + Let w_head0 := w_op.(znz_head0). + Let w_tail0 := w_op.(znz_tail0). + + Let w0 := w_op.(znz_0). + Let w1 := w_op.(znz_1). + Let wBm1 := w_op.(znz_Bm1). + + Let w_compare := w_op.(znz_compare). + Let w_eq0 := w_op.(znz_eq0). + + Let w_opp_c := w_op.(znz_opp_c). + Let w_opp := w_op.(znz_opp). + Let w_opp_carry := w_op.(znz_opp_carry). + + Let w_succ_c := w_op.(znz_succ_c). + Let w_add_c := w_op.(znz_add_c). + Let w_add_carry_c := w_op.(znz_add_carry_c). + Let w_succ := w_op.(znz_succ). + Let w_add := w_op.(znz_add). + Let w_add_carry := w_op.(znz_add_carry). + + Let w_pred_c := w_op.(znz_pred_c). + Let w_sub_c := w_op.(znz_sub_c). + Let w_sub_carry_c := w_op.(znz_sub_carry_c). + Let w_pred := w_op.(znz_pred). + Let w_sub := w_op.(znz_sub). + Let w_sub_carry := w_op.(znz_sub_carry). + + Let w_mul_c := w_op.(znz_mul_c). + Let w_mul := w_op.(znz_mul). + Let w_square_c := w_op.(znz_square_c). + + Let w_div21 := w_op.(znz_div21). + Let w_div_gt := w_op.(znz_div_gt). + Let w_div := w_op.(znz_div). + + Let w_mod_gt := w_op.(znz_mod_gt). + Let w_mod := w_op.(znz_mod). + + Let w_gcd_gt := w_op.(znz_gcd_gt). + Let w_gcd := w_op.(znz_gcd). + + Let w_add_mul_div := w_op.(znz_add_mul_div). + + Let w_pos_mod := w_op.(znz_pos_mod). + + Let w_is_even := w_op.(znz_is_even). + Let w_sqrt2 := w_op.(znz_sqrt2). + Let w_sqrt := w_op.(znz_sqrt). + + Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99). + + Let wB := base w_digits. + + Notation "[+| c |]" := + (interp_carry 1 wB w_to_Z c) (at level 0, x at level 99). + + Notation "[-| c |]" := + (interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99). + + Notation "[|| x ||]" := + (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99). + + Record znz_spec := mk_znz_spec { + + (* Conversion functions with Z *) + spec_to_Z : forall x, 0 <= [| x |] < wB; + spec_of_pos : forall p, + Zpos p = (Z_of_N (fst (w_of_pos p)))*wB + [|(snd (w_of_pos p))|]; + spec_zdigits : [| w_zdigits |] = Zpos w_digits; + spec_more_than_1_digit: 1 < Zpos w_digits; + + (* Basic numbers *) + spec_0 : [|w0|] = 0; + spec_1 : [|w1|] = 1; + spec_Bm1 : [|wBm1|] = wB - 1; + + (* Comparison *) + spec_compare : + forall x y, + match w_compare x y with + | Eq => [|x|] = [|y|] + | Lt => [|x|] < [|y|] + | Gt => [|x|] > [|y|] + end; + spec_eq0 : forall x, w_eq0 x = true -> [|x|] = 0; + (* Basic arithmetic operations *) + spec_opp_c : forall x, [-|w_opp_c x|] = -[|x|]; + spec_opp : forall x, [|w_opp x|] = (-[|x|]) mod wB; + spec_opp_carry : forall x, [|w_opp_carry x|] = wB - [|x|] - 1; + + spec_succ_c : forall x, [+|w_succ_c x|] = [|x|] + 1; + spec_add_c : forall x y, [+|w_add_c x y|] = [|x|] + [|y|]; + spec_add_carry_c : forall x y, [+|w_add_carry_c x y|] = [|x|] + [|y|] + 1; + spec_succ : forall x, [|w_succ x|] = ([|x|] + 1) mod wB; + spec_add : forall x y, [|w_add x y|] = ([|x|] + [|y|]) mod wB; + spec_add_carry : + forall x y, [|w_add_carry x y|] = ([|x|] + [|y|] + 1) mod wB; + + spec_pred_c : forall x, [-|w_pred_c x|] = [|x|] - 1; + spec_sub_c : forall x y, [-|w_sub_c x y|] = [|x|] - [|y|]; + spec_sub_carry_c : forall x y, [-|w_sub_carry_c x y|] = [|x|] - [|y|] - 1; + spec_pred : forall x, [|w_pred x|] = ([|x|] - 1) mod wB; + spec_sub : forall x y, [|w_sub x y|] = ([|x|] - [|y|]) mod wB; + spec_sub_carry : + forall x y, [|w_sub_carry x y|] = ([|x|] - [|y|] - 1) mod wB; + + spec_mul_c : forall x y, [|| w_mul_c x y ||] = [|x|] * [|y|]; + spec_mul : forall x y, [|w_mul x y|] = ([|x|] * [|y|]) mod wB; + spec_square_c : forall x, [|| w_square_c x||] = [|x|] * [|x|]; + + (* Special divisions operations *) + spec_div21 : forall a1 a2 b, + wB/2 <= [|b|] -> + [|a1|] < [|b|] -> + let (q,r) := w_div21 a1 a2 b in + [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + spec_div_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + let (q,r) := w_div_gt a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + spec_div : forall a b, 0 < [|b|] -> + let (q,r) := w_div a b in + [|a|] = [|q|] * [|b|] + [|r|] /\ + 0 <= [|r|] < [|b|]; + + spec_mod_gt : forall a b, [|a|] > [|b|] -> 0 < [|b|] -> + [|w_mod_gt a b|] = [|a|] mod [|b|]; + spec_mod : forall a b, 0 < [|b|] -> + [|w_mod a b|] = [|a|] mod [|b|]; + + spec_gcd_gt : forall a b, [|a|] > [|b|] -> + Zis_gcd [|a|] [|b|] [|w_gcd_gt a b|]; + spec_gcd : forall a b, Zis_gcd [|a|] [|b|] [|w_gcd a b|]; + + + (* shift operations *) + spec_head00: forall x, [|x|] = 0 -> [|w_head0 x|] = Zpos w_digits; + spec_head0 : forall x, 0 < [|x|] -> + wB/ 2 <= 2 ^ ([|w_head0 x|]) * [|x|] < wB; + spec_tail00: forall x, [|x|] = 0 -> [|w_tail0 x|] = Zpos w_digits; + spec_tail0 : forall x, 0 < [|x|] -> + exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|w_tail0 x|]) ; + spec_add_mul_div : forall x y p, + [|p|] <= Zpos w_digits -> + [| w_add_mul_div p x y |] = + ([|x|] * (2 ^ [|p|]) + + [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB; + spec_pos_mod : forall w p, + [|w_pos_mod p w|] = [|w|] mod (2 ^ [|p|]); + (* sqrt *) + spec_is_even : forall x, + if w_is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1; + spec_sqrt2 : forall x y, + wB/ 4 <= [|x|] -> + let (s,r) := w_sqrt2 x y in + [||WW x y||] = [|s|] ^ 2 + [+|r|] /\ + [+|r|] <= 2 * [|s|]; + spec_sqrt : forall x, + [|w_sqrt x|] ^ 2 <= [|x|] < ([|w_sqrt x|] + 1) ^ 2 + }. + +End Z_nZ_Spec. + +(** Generic construction of double words *) + +Section WW. + + Variable w : Type. + Variable w_op : znz_op w. + Variable op_spec : znz_spec w_op. + + Let wB := base w_op.(znz_digits). + Let w_to_Z := w_op.(znz_to_Z). + Let w_eq0 := w_op.(znz_eq0). + Let w_0 := w_op.(znz_0). + + Definition znz_W0 h := + if w_eq0 h then W0 else WW h w_0. + + Definition znz_0W l := + if w_eq0 l then W0 else WW w_0 l. + + Definition znz_WW h l := + if w_eq0 h then znz_0W l else WW h l. + + Lemma spec_W0 : forall h, + zn2z_to_Z wB w_to_Z (znz_W0 h) = (w_to_Z h)*wB. + Proof. + unfold zn2z_to_Z, znz_W0, w_to_Z; simpl; intros. + case_eq (w_eq0 h); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + unfold w_0; rewrite op_spec.(spec_0); auto with zarith. + Qed. + + Lemma spec_0W : forall l, + zn2z_to_Z wB w_to_Z (znz_0W l) = w_to_Z l. + Proof. + unfold zn2z_to_Z, znz_0W, w_to_Z; simpl; intros. + case_eq (w_eq0 l); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + unfold w_0; rewrite op_spec.(spec_0); auto with zarith. + Qed. + + Lemma spec_WW : forall h l, + zn2z_to_Z wB w_to_Z (znz_WW h l) = (w_to_Z h)*wB + w_to_Z l. + Proof. + unfold znz_WW, w_to_Z; simpl; intros. + case_eq (w_eq0 h); intros. + rewrite (op_spec.(spec_eq0) _ H); auto. + rewrite spec_0W; auto. + simpl; auto. + Qed. + +End WW. + +(** Injecting [Z] numbers into a cyclic structure *) + +Section znz_of_pos. + + Variable w : Type. + Variable w_op : znz_op w. + Variable op_spec : znz_spec w_op. + + Notation "[| x |]" := (znz_to_Z w_op x) (at level 0, x at level 99). + + Definition znz_of_Z (w:Type) (op:znz_op w) z := + match z with + | Zpos p => snd (op.(znz_of_pos) p) + | _ => op.(znz_0) + end. + + Theorem znz_of_pos_correct: + forall p, Zpos p < base (znz_digits w_op) -> [|(snd (znz_of_pos w_op p))|] = Zpos p. + intros p Hp. + generalize (spec_of_pos op_spec p). + case (znz_of_pos w_op p); intros n w1; simpl. + case n; simpl Npos; auto with zarith. + intros p1 Hp1; contradict Hp; apply Zle_not_lt. + rewrite Hp1; auto with zarith. + match goal with |- _ <= ?X + ?Y => + apply Zle_trans with X; auto with zarith + end. + match goal with |- ?X <= _ => + pattern X at 1; rewrite <- (Zmult_1_l); + apply Zmult_le_compat_r; auto with zarith + end. + case p1; simpl; intros; red; simpl; intros; discriminate. + unfold base; auto with zarith. + case (spec_to_Z op_spec w1); auto with zarith. + Qed. + + Theorem znz_of_Z_correct: + forall p, 0 <= p < base (znz_digits w_op) -> [|znz_of_Z w_op p|] = p. + intros p; case p; simpl; try rewrite spec_0; auto. + intros; rewrite znz_of_pos_correct; auto with zarith. + intros p1 (H1, _); contradict H1; apply Zlt_not_le; red; simpl; auto. + Qed. +End znz_of_pos. + + +(** A modular specification grouping the earlier records. *) + +Module Type CyclicType. + Parameter w : Type. + Parameter w_op : znz_op w. + Parameter w_spec : znz_spec w_op. +End CyclicType. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v new file mode 100644 index 00000000..22f6d95b --- /dev/null +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -0,0 +1,236 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: NZCyclic.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NZAxioms. +Require Import BigNumPrelude. +Require Import DoubleType. +Require Import CyclicAxioms. + +(** * From [CyclicType] to [NZAxiomsSig] *) + +(** 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. +Proof. +unfold equiv, reflexive, symmetric, transitive, NZeq; repeat split; intros; auto. +now transitivity [| y |]. +Qed. + +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. +Proof. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. +Qed. + +Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. +Proof. +unfold NZeq; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. +Qed. + +Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. +Proof. +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). +now rewrite H1, H2. +Qed. + +Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. +Proof. +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). +now rewrite H1, H2. +Qed. + +Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. +Proof. +unfold NZeq; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_mul). +now rewrite H1, H2. +Qed. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with NZ. +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'" := NZsucc : IntScope. +Notation "'P'" := NZpred : IntScope. +(*Notation "1" := (S 0) : IntScope.*) +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. +Proof. +unfold base. +apply Zpower_gt_1; unfold Zlt; auto with zarith. +Qed. + +Theorem gt_wB_0 : 0 < wB. +Proof. +pose proof gt_wB_1; auto with zarith. +Qed. + +Lemma NZsucc_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB. +Proof. +intro n. +pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod. +reflexivity. +now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. +Qed. + +Lemma NZpred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB. +Proof. +intro n. +pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod. +reflexivity. +now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]]. +Qed. + +Lemma NZ_to_Z_mod : forall n : NZ, [| n |] mod wB = [| n |]. +Proof. +intro n; rewrite Zmod_small. reflexivity. apply w_spec.(spec_to_Z). +Qed. + +Theorem NZpred_succ : forall n : NZ, P (S n) == n. +Proof. +intro n; unfold NZsucc, NZpred, NZeq. rewrite w_spec.(spec_pred), w_spec.(spec_succ). +rewrite <- NZpred_mod_wB. +replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. +Qed. + +Lemma Z_to_NZ_0 : Z_to_NZ 0%Z == 0%Int. +Proof. +unfold NZeq, NZ_to_Z, Z_to_NZ. rewrite znz_of_Z_correct. +symmetry; apply w_spec.(spec_0). +exact w_spec. split; [auto with zarith |apply gt_wB_0]. +Qed. + +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). (* Below, we use only -> direction *) + +Add Morphism A with signature NZeq ==> iff as A_morph. +Proof. apply A_wd. Qed. + +Let B (n : Z) := A (Z_to_NZ n). + +Lemma B0 : B 0. +Proof. +unfold B. now rewrite Z_to_NZ_0. +Qed. + +Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1). +Proof. +intros n H1 H2 H3. +unfold B in *. apply -> AS in H3. +setoid_replace (Z_to_NZ (n + 1)) with (S (Z_to_NZ n)) using relation NZeq. assumption. +unfold NZeq. rewrite w_spec.(spec_succ). +unfold NZ_to_Z, Z_to_NZ. +do 2 (rewrite znz_of_Z_correct; [ | exact w_spec | auto with zarith]). +symmetry; apply Zmod_small; auto with zarith. +Qed. + +Lemma B_holds : forall n : Z, 0 <= n < wB -> B n. +Proof. +intros n [H1 H2]. +apply Zbounded_induction with wB. +apply B0. apply BS. assumption. assumption. +Qed. + +Theorem NZinduction : forall n : NZ, A n. +Proof. +intro n. setoid_replace n with (Z_to_NZ (NZ_to_Z n)) using relation NZeq. +apply B_holds. apply w_spec.(spec_to_Z). +unfold NZeq, NZ_to_Z, Z_to_NZ; rewrite znz_of_Z_correct. +reflexivity. +exact w_spec. +apply w_spec.(spec_to_Z). +Qed. + +End Induction. + +Theorem NZadd_0_l : forall n : NZ, 0 + n == n. +Proof. +intro n; unfold NZadd, NZ0, NZeq. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). +rewrite Zplus_0_l. rewrite Zmod_small; [reflexivity | apply w_spec.(spec_to_Z)]. +Qed. + +Theorem NZadd_succ_l : forall n m : NZ, (S n) + m == S (n + m). +Proof. +intros n m; unfold NZadd, NZsucc, NZeq. rewrite w_spec.(spec_add). +do 2 rewrite w_spec.(spec_succ). rewrite w_spec.(spec_add). +rewrite NZsucc_mod_wB. repeat rewrite Zplus_mod_idemp_l; try apply gt_wB_0. +rewrite <- (Zplus_assoc ([| n |] mod wB) 1 [| m |]). rewrite Zplus_mod_idemp_l. +rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. +Qed. + +Theorem NZsub_0_r : forall n : NZ, n - 0 == n. +Proof. +intro n; unfold NZsub, NZ0, NZeq. rewrite w_spec.(spec_sub). +rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. +Qed. + +Theorem NZsub_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Proof. +intros n m; unfold NZsub, NZsucc, NZpred, NZeq. +rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). +rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r. +rewrite Zminus_mod_idemp_l. +now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith. +Qed. + +Theorem NZmul_0_l : forall n : NZ, 0 * n == 0. +Proof. +intro n; unfold NZmul, NZ0, NZ, NZeq. rewrite w_spec.(spec_mul). +rewrite w_spec.(spec_0). now rewrite Zmult_0_l. +Qed. + +Theorem NZmul_succ_l : forall n m : NZ, (S n) * m == n * m + m. +Proof. +intros n m; unfold NZmul, NZsucc, NZadd, NZeq. rewrite w_spec.(spec_mul). +rewrite w_spec.(spec_add), w_spec.(spec_mul), w_spec.(spec_succ). +rewrite Zplus_mod_idemp_l, Zmult_mod_idemp_l. +now rewrite Zmult_plus_distr_l, Zmult_1_l. +Qed. + +End NZCyclicAxiomsMod. |