diff options
Diffstat (limited to 'theories/Numbers/Integer/BigInts')
| -rw-r--r-- | theories/Numbers/Integer/BigInts/EZBase.v | 167 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigInts/Zeqmod.v | 48 |
2 files changed, 215 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v new file mode 100644 index 000000000..f5c19c611 --- /dev/null +++ b/theories/Numbers/Integer/BigInts/EZBase.v @@ -0,0 +1,167 @@ +Require Export ZBase. +(*Require Import BigN.*) +Require Import NMake. +Require Import ZnZ. +Require Import Basic_type. +Require Import ZAux. +Require Import Zeqmod. +Require Import ZArith. + +Module EZBaseMod (Import EffIntsMod : W0Type) <: ZBaseSig. +Open Local Scope Z_scope. + +Definition Z := EffIntsMod.w. + +Definition w_op := EffIntsMod.w_op. +Definition w_spec := EffIntsMod.w_spec. +Definition to_Z := w_op.(znz_to_Z). +Definition of_Z := znz_of_Z w_op. +Definition wB := base w_op.(znz_digits). + +Theorem Zpow_gt_1 : forall n m : BinInt.Z, 0 < n -> 1 < m -> 1 < m ^ n. +Proof. +intros n m H1 H2. +replace 1 with (m ^ 0) by apply Zpower_exp_0. +apply Zpower_lt_monotone; auto with zarith. +Qed. + +Theorem wB_gt_1 : 1 < wB. +Proof. +unfold wB, base. apply Zpow_gt_1; unfold Zlt; auto with zarith. +Qed. + +Theorem wB_gt_0 : 0 < wB. +Proof. +pose proof wB_gt_1; auto with zarith. +Qed. + +Notation "[| x |]" := (to_Z x) (at level 0, x at level 99). + +Theorem to_Z_spec : forall x : Z, 0 <= [|x|] < wB. +Proof w_spec.(spec_to_Z). + +Definition ZE (n m : Z) := [|n|] = [|m|]. + +Notation "x == y" := (ZE x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope. +Open Local Scope IntScope. + +Theorem ZE_equiv : equiv Z ZE. +Proof. +unfold equiv, reflexive, symmetric, transitive, ZE; repeat split; intros; auto. +now transitivity [|y|]. +Qed. + +Add Relation Z ZE + reflexivity proved by (proj1 ZE_equiv) + symmetry proved by (proj2 (proj2 ZE_equiv)) + transitivity proved by (proj1 (proj2 ZE_equiv)) +as ZE_rel. + +Definition Z0 := w_op.(znz_0). +Definition Zsucc := w_op.(znz_succ). + +Notation "0" := Z0 : IntScope. +Notation "'S'" := Zsucc : IntScope. +Notation "1" := (S 0) : IntScope. + +Theorem Zsucc_spec : forall n : Z, [|S n|] = ([|n|] + 1) mod wB. +Proof w_spec.(spec_succ). + +Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd. +Proof. +unfold ZE; intros n m H. do 2 rewrite Zsucc_spec. now rewrite H. +Qed. + +Theorem Zsucc_inj : forall x y : Z, S x == S y -> x == y. +Proof. +intros x y H; unfold ZE in *; do 2 rewrite Zsucc_spec in H. +apply <- Zplus_eqmod_compat_r in H. +do 2 rewrite Zmod_def_small in H; now try apply to_Z_spec. +apply wB_gt_0. +Qed. + +Lemma of_Z_0 : of_Z 0 == Z0. +Proof. +unfold ZE, to_Z, of_Z. rewrite znz_of_Z_correct. +symmetry; apply w_spec.(spec_0). +exact w_spec. split; [auto with zarith |apply wB_gt_0]. +Qed. + +Section Induction. + +Variable A : Z -> Prop. +Hypothesis A_wd : predicate_wd ZE A. +Hypothesis A0 : A 0. +Hypothesis AS : forall n : Z, A n <-> A (S n). (* In fact, it's enought to have only -> *) + +Add Morphism A with signature ZE ==> iff as A_morph. +Proof A_wd. + +Let B (n : BinInt.Z) := A (of_Z n). + +Lemma B0 : B 0. +Proof. +unfold B. now rewrite of_Z_0. +Qed. + +Lemma BS : forall n : BinInt.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 (of_Z (n + 1)) with (S (of_Z n)) using relation ZE. assumption. +unfold ZE. rewrite Zsucc_spec. +unfold to_Z, of_Z. rewrite znz_of_Z_correct. rewrite znz_of_Z_correct. +symmetry; apply Zmod_def_small; auto with zarith. +exact w_spec. +unfold wB in *; auto with zarith. +exact w_spec. +unfold wB in *; auto with zarith. +Qed. + +Lemma Zbounded_induction : + (forall Q : BinInt.Z -> Prop, forall b : BinInt.Z, + Q 0 -> + (forall n, 0 <= n -> n < b - 1 -> Q n -> Q (n + 1)) -> + forall n, 0 <= n -> n < b -> Q n)%Z. +Proof. +intros Q b Q0 QS. +set (Q' := fun n => (n < b /\ Q n) \/ (b <= n)). +assert (H : forall n, 0 <= n -> Q' n). +apply natlike_rec2; unfold Q'. +destruct (Zle_or_lt b 0) as [H | H]. now right. left; now split. +intros n H IH. destruct IH as [[IH1 IH2] | IH]. +destruct (Zle_or_lt (b - 1) n) as [H1 | H1]. +right; auto with zarith. +left. split; [auto with zarith | now apply (QS n)]. +right; auto with zarith. +unfold Q' in *; intros n H1 H2. destruct (H n H1) as [[H3 H4] | H3]. +assumption. apply Zle_not_lt in H3. false_hyp H2 H3. +Qed. + +Lemma B_holds : forall n : BinInt.Z, 0 <= n < wB -> B n. +Proof. +intros n [H1 H2]. +apply Zbounded_induction with wB. +apply B0. apply BS. assumption. assumption. +Qed. + +Theorem Zinduction : forall n : Z, A n. +Proof. +intro n. setoid_replace n with (of_Z (to_Z n)) using relation ZE. +apply B_holds. apply to_Z_spec. +unfold ZE, to_Z, of_Z; rewrite znz_of_Z_correct. +reflexivity. +exact w_spec. +apply to_Z_spec. +Qed. + +End Induction. + +End EZBaseMod. + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v new file mode 100644 index 000000000..ca3286211 --- /dev/null +++ b/theories/Numbers/Integer/BigInts/Zeqmod.v @@ -0,0 +1,48 @@ +Require Import ZArith. +Require Import ZAux. + +Open Local Scope Z_scope. +Notation "x == y '[' 'mod' z ']'" := ((x mod z) = (y mod z)) + (at level 70, no associativity) : Z_scope. + +Theorem Zeqmod_refl : forall p n : Z, n == n [mod p]. +Proof. +reflexivity. +Qed. + +Theorem Zeqmod_symm : forall p n m : Z, n == m [mod p] -> m == n [mod p]. +Proof. +now symmetry. +Qed. + +Theorem Zeqmod_trans : + forall p n m k : Z, n == m [mod p] -> m == k [mod p] -> n == k [mod p]. +Proof. +intros p n m k H1 H2; now transitivity (m mod p). +Qed. + +Theorem Zplus_eqmod_compat_l : + forall p n m k : Z, 0 < p -> (n == m [mod p] <-> k + n == k + m [mod p]). +intros p n m k H1. +assert (LR : forall n' m' k' : Z, n' == m' [mod p] -> k' + n' == k' + m' [mod p]). +intros n' m' k' H2. +pattern ((k' + n') mod p); rewrite Zmod_plus; [| assumption]. +pattern ((k' + m') mod p); rewrite Zmod_plus; [| assumption]. +rewrite H2. apply Zeqmod_refl. +split; [apply LR |]. +intro H2. apply (LR (k + n) (k + m) (-k)) in H2. +do 2 rewrite Zplus_assoc in H2. rewrite Zplus_opp_l in H2. +now do 2 rewrite Zplus_0_l in H2. +Qed. + +Theorem Zplus_eqmod_compat_r : + forall p n m k : Z, 0 < p -> (n == m [mod p] <-> n + k == m + k [mod p]). +intros p n m k; rewrite (Zplus_comm n k); rewrite (Zplus_comm m k); +apply Zplus_eqmod_compat_l. +Qed. + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |