diff options
| -rw-r--r-- | Makefile.common | 5 | ||||
| -rw-r--r-- | theories/Ints/Z/ZAux.v | 121 | ||||
| -rw-r--r-- | theories/Ints/Z/Zmod.v | 94 | ||||
| -rw-r--r-- | theories/Ints/num/GenDiv.v | 1 | ||||
| -rw-r--r-- | theories/Ints/num/GenLift.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigInts/EZBase.v | 161 | ||||
| -rw-r--r-- | theories/Numbers/Integer/BigInts/Zeqmod.v | 42 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsOrder.v | 112 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsPlus.v | 83 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsTimes.v | 56 | ||||
| -rw-r--r-- | theories/Numbers/Integer/TreeMod/ZTreeMod.v | 216 |
12 files changed, 324 insertions, 569 deletions
diff --git a/Makefile.common b/Makefile.common index ba790f62b6..08feab44b5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -531,7 +531,6 @@ INTSVO:=\ theories/Ints/Z/IntsZmisc.vo theories/Ints/Z/Pmod.vo \ theories/Ints/Tactic.vo theories/Ints/Z/ZAux.vo \ theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo \ - theories/Ints/Z/Zmod.vo \ theories/Ints/Basic_type.vo theories/Ints/Int31.vo \ theories/Ints/num/GenBase.vo theories/Ints/num/ZnZ.vo \ theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo \ @@ -710,7 +709,9 @@ INTEGERBINARYVO:=$(INTEGERDIR)/Binary/ZBinary.vo INTEGERNATPAIRSVO:=$(INTEGERDIR)/NatPairs/ZNatPairs.vo -INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) +INTEGERTREEMODVO:=$(INTEGERDIR)/TreeMod/ZTreeMod.vo + +INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) $(INTEGERTREEMODVO) NUMBERSVO:=$(NATURALVO) $(INTEGERVO) diff --git a/theories/Ints/Z/ZAux.v b/theories/Ints/Z/ZAux.v index 73fdbd1281..3f0c7a5c65 100644 --- a/theories/Ints/Z/ZAux.v +++ b/theories/Ints/Z/ZAux.v @@ -7,9 +7,9 @@ (*************************************************************) (********************************************************************** - Aux.v - - Auxillary functions & Theorems + Aux.v + + Auxillary functions & Theorems **********************************************************************) Require Import ArithRing. @@ -368,6 +368,12 @@ intros p2 _; apply Zpower_pos_nat. intros p2 H1; case H1; auto. Qed. +Theorem Zgt_pow_1 : forall n m : 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. (************************************** Properties Zmod @@ -397,7 +403,7 @@ replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n)) apply Z_mod_plus; auto with zarith. ring. Qed. - + Theorem Zmod_mod: forall a n, 0 < n -> (a mod n) mod n = a mod n. intros a n H. pattern a at 2; rewrite (Z_div_mod_eq a n); auto with zarith. @@ -450,6 +456,60 @@ case (Z_mod_lt a n); auto with zarith. rewrite Zmod_def_small; auto with zarith. Qed. +Lemma Zplus_mod_idemp_l: forall a b n, 0 < n -> (a mod n + b) mod n = (a + b) mod n. +Proof. +intros. rewrite Zmod_plus; auto. +rewrite Zmod_mod; auto. +symmetry; apply Zmod_plus; auto. +Qed. + +Lemma Zplus_mod_idemp_r: forall a b n, 0 < n -> (b + a mod n) mod n = (b + a) mod n. +Proof. +intros a b n H; repeat rewrite (Zplus_comm b). +apply Zplus_mod_idemp_l; auto. +Qed. + +Lemma Zminus_mod_idemp_l: forall a b n, 0 < n -> (a mod n - b) mod n = (a - b) mod n. +Proof. +intros. rewrite Zmod_minus; auto. +rewrite Zmod_mod; auto. +symmetry; apply Zmod_minus; auto. +Qed. + +Lemma Zminus_mod_idemp_r: forall a b n, 0 < n -> (a - b mod n) mod n = (a - b) mod n. +Proof. +intros. rewrite Zmod_minus; auto. +rewrite Zmod_mod; auto. +symmetry; apply Zmod_minus; auto. +Qed. + +Lemma Zmult_mod_idemp_l: forall a b n, 0 < n -> (a mod n * b) mod n = (a * b) mod n. +Proof. +intros; rewrite Zmod_mult; auto. +rewrite Zmod_mod; auto. +symmetry; apply Zmod_mult; auto. +Qed. + +Lemma Zmult_mod_idemp_r: forall a b n, 0 < n -> (b * (a mod n)) mod n = (b * a) mod n. +Proof. +intros a b n H; repeat rewrite (Zmult_comm b). +apply Zmult_mod_idemp_l; auto. +Qed. + +Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m -> + (n | m) -> a mod n = (a mod m) mod n. +Proof. +intros n m a H1 H2 H3. +pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith. +case H3; intros q Hq; pattern m at 1; rewrite Hq. +rewrite (Zmult_comm q). +rewrite Zmod_plus; auto. +rewrite <- Zmult_assoc; rewrite Zmod_mult; auto. +rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith. +rewrite (Zmod_def_small 0); auto with zarith. +rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. +Qed. + (** A better way to compute Zpower mod **) Fixpoint Zpow_mod_pos (a: Z) (m: positive) (n : Z) {struct m} : Z := @@ -701,18 +761,6 @@ intros H2; absurd (0 <= Zgcd a b); auto with zarith. generalize (Zgcd_is_pos a b); auto with zarith. Qed. - -Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q. -intros p q H H0. -assert (H1: Bezout p q 1). -apply rel_prime_bezout; auto. -inversion_clear H1 as [q1 r1 H2]. -apply bezout_rel_prime. -apply Bezout_intro with q1 (r1 + q1 * (p / q)). -rewrite <- H2. -pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. -Qed. - Theorem rel_prime_mod_rev: forall p q, 0 < q -> rel_prime (p mod q) q -> rel_prime p q. intros p q H H0. rewrite (Z_div_mod_eq p q); auto with zarith. @@ -744,6 +792,24 @@ exists 1; auto with zarith. apply Zis_gcd_sym; auto. Qed. +Theorem rel_prime_mod: forall p q, 0 < q -> rel_prime p q -> rel_prime (p mod q) q. +intros p q H H0. +assert (H1: Bezout p q 1). +apply rel_prime_bezout; auto. +inversion_clear H1 as [q1 r1 H2]. +apply bezout_rel_prime. +apply Bezout_intro with q1 (r1 + q1 * (p / q)). +rewrite <- H2. +pattern p at 3; rewrite (Z_div_mod_eq p q); try ring; auto with zarith. +Qed. + +Theorem Zrel_prime_neq_mod_0: forall a b, 1 < b -> rel_prime a b -> a mod b <> 0. +Proof. +intros a b H H1 H2. +case (not_rel_prime_0 _ H). +rewrite <- H2. +apply rel_prime_mod; auto with zarith. +Qed. Theorem rel_prime_Zpower_r: forall i p q, 0 < i -> rel_prime p q -> rel_prime p (q^i). intros i p q Hi Hpq; generalize Hi; pattern i; apply natlike_ind; auto with zarith; clear i Hi. @@ -1369,4 +1435,27 @@ Ltac pos_tac := [idtac; repeat rewrite Zpos_eq_Z_of_nat_o_nat_of_P; eq_tac | injection tmp; auto] end; autorewrite with pos_morph. +(************************************** + Bounded induction +**************************************) + +Theorem Zbounded_induction : + (forall Q : Z -> Prop, forall b : 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. diff --git a/theories/Ints/Z/Zmod.v b/theories/Ints/Z/Zmod.v deleted file mode 100644 index dffa795322..0000000000 --- a/theories/Ints/Z/Zmod.v +++ /dev/null @@ -1,94 +0,0 @@ -Require Import ZArith. -Require Import ZAux. - -Set Implicit Arguments. - -Open Scope Z_scope. - -Lemma rel_prime_mod: forall a b, 1 < b -> - rel_prime a b -> a mod b <> 0. -Proof. -intros a b H H1 H2. -case (not_rel_prime_0 _ H). -rewrite <- H2. -apply rel_prime_mod; auto with zarith. -Qed. - -Lemma Zmodpl: forall a b n, 0 < n -> - (a mod n + b) mod n = (a + b) mod n. -Proof. -intros a b n H. -rewrite Zmod_plus; auto. -rewrite Zmod_mod; auto. -apply sym_equal; apply Zmod_plus; auto. -Qed. - -Lemma Zmodpr: forall a b n, 0 < n -> - (b + a mod n) mod n = (b + a) mod n. -Proof. -intros a b n H; repeat rewrite (Zplus_comm b). -apply Zmodpl; auto. -Qed. - -Lemma Zmodml: forall a b n, 0 < n -> - (a mod n * b) mod n = (a * b) mod n. -Proof. -intros a b n H. -rewrite Zmod_mult; auto. -rewrite Zmod_mod; auto. -apply sym_equal; apply Zmod_mult; auto. -Qed. - -Lemma Zmodmr: forall a b n, 0 < n -> - (b * (a mod n)) mod n = (b * a) mod n. -Proof. -intros a b n H; repeat rewrite (Zmult_comm b). -apply Zmodml; auto. -Qed. - - -Ltac is_ok t := - match t with - | (?x mod _ + ?y mod _) mod _ => constr:false - | (?x mod _ * (?y mod _)) mod _ => constr:false - | ?x mod _ => x - end. - -Ltac rmod t := - match t with - (?x + ?y) mod _ => - match (is_ok x) with - | false => rmod x - | ?x1 => match (is_ok y) with - |false => rmod y - | ?y1 => - rewrite <- (Zmod_plus x1 y1) - |false => rmod y - end - end - | (?x * ?y) mod _ => - match (is_ok x) with - | false => rmod x - | ?x1 => match (is_ok y) with - |false => rmod y - | ?y1 => rewrite <- (Zmod_mult x1 y1) - end - | false => rmod x - end - end. - - -Lemma Zmod_div_mod: forall n m a, 0 < n -> 0 < m -> - (n | m) -> a mod n = (a mod m) mod n. -Proof. -intros n m a H1 H2 H3. -pattern a at 1; rewrite (Z_div_mod_eq a m); auto with zarith. -case H3; intros q Hq; pattern m at 1; rewrite Hq. -rewrite (Zmult_comm q). -rewrite Zmod_plus; auto. -rewrite <- Zmult_assoc; rewrite Zmod_mult; auto. -rewrite Z_mod_same; try rewrite Zmult_0_l; auto with zarith. -rewrite (Zmod_def_small 0); auto with zarith. -rewrite Zplus_0_l; rewrite Zmod_mod; auto with zarith. -Qed. - diff --git a/theories/Ints/num/GenDiv.v b/theories/Ints/num/GenDiv.v index 4a30fa2c32..3bf0615c2b 100644 --- a/theories/Ints/num/GenDiv.v +++ b/theories/Ints/num/GenDiv.v @@ -12,7 +12,6 @@ Require Import ZArith. Require Import ZAux. Require Import ZDivModAux. Require Import ZPowerAux. -Require Import Zmod. Require Import Basic_type. Require Import GenBase. Require Import GenDivn1. diff --git a/theories/Ints/num/GenLift.v b/theories/Ints/num/GenLift.v index 11455b8044..68d03fd82f 100644 --- a/theories/Ints/num/GenLift.v +++ b/theories/Ints/num/GenLift.v @@ -12,7 +12,6 @@ Require Import ZArith. Require Import ZAux. Require Import ZPowerAux. Require Import ZDivModAux. -Require Import Zmod. Require Import Basic_type. Require Import GenBase. diff --git a/theories/Numbers/Integer/BigInts/EZBase.v b/theories/Numbers/Integer/BigInts/EZBase.v deleted file mode 100644 index a1e52a2024..0000000000 --- a/theories/Numbers/Integer/BigInts/EZBase.v +++ /dev/null @@ -1,161 +0,0 @@ -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. diff --git a/theories/Numbers/Integer/BigInts/Zeqmod.v b/theories/Numbers/Integer/BigInts/Zeqmod.v deleted file mode 100644 index b31dcdf9df..0000000000 --- a/theories/Numbers/Integer/BigInts/Zeqmod.v +++ /dev/null @@ -1,42 +0,0 @@ -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. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 41fc7e75ee..5c8b5890d5 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -25,7 +25,6 @@ In that case, we could get rid of setoids as well as arrive at integers as signed natural numbers. *) Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)). Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)). -Definition NZuminus (n : Z) := (snd n, fst n). (* Unfortunately, the elements of the pair keep increasing, even during subtraction *) Definition NZtimes (n m : Z) := diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v deleted file mode 100644 index dc258f873f..0000000000 --- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v +++ /dev/null @@ -1,112 +0,0 @@ -Require Import NPlusOrder. -Require Export ZPlusOrder. -Require Export ZPairsPlus. - -Module NatPairsOrder (Import NPlusMod : NPlusSig) - (Import NOrderModule : NOrderSig - with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature. -Module Import NPlusOrderPropertiesModule := - NPlusOrderProperties NPlusMod NOrderModule. -Module Export ZBaseMod := NatPairsInt NPlusMod. -Open Local Scope NatScope. - -Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1). -Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1). - -Notation "x < y" := (lt x y) : IntScope. -Notation "x <= y" := (le x y) : IntScope. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl. -rewrite eq_true_iff; split; intro H. -stepr (snd y1 + fst y2) by apply plus_comm. -apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption]. -stepl (snd y2 + fst x1) by apply plus_comm. -stepr (fst y2 + snd x1) by apply plus_comm. -apply (plus_lt_repl_pair (snd x2) (fst x2)). -now stepl (fst x1 + snd x2) by apply plus_comm. -stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm. -stepr (snd x1 + fst x2) by apply plus_comm. -apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry]. -stepl (snd x2 + fst y1) by apply plus_comm. -stepr (fst x2 + snd y1) by apply plus_comm. -apply (plus_lt_repl_pair (snd y2) (fst y2)). -now stepl (fst y1 + snd y2) by apply plus_comm. -stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm. -Qed. - -(* Below is a very long explanation why it would be useful to be -able to use the fold tactic in hypotheses. -We will prove the following statement not from scratch, like lt_wd, -but expanding <= to < and == and then using lt_wd. The theorem we need -to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z. -To be able to express <= through < and ==, we need to expand <=%Int to -<=%Nat, since we have not proved yet the properties of <=%Int. But -then it would be convenient to fold back equalities from -(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int. -The reason is that we will need to show that (x1 == x2)%Int <-> -(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold -equalities back to Int, then we could do simple rewriting, since we have -already showed that ==%Int is an equivalence relation. On the other hand, -if we leave equalities expanded to Nat, we will have to apply the -transitivity of ==%Int by hand. *) - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl. -rewrite eq_true_iff. do 2 rewrite le_lt. -pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H. -(* This is a remark about an extra level of definitions created by -"with Module NBaseMod := NPlusMod.NBaseMod" constraint in the beginning -of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out -that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since -NPlusMod was imported first. On the other hand, the goal uses -NOrderModule.NBaseMod.NDomainModule.E, or just NDomainModule.E, since le_lt -theorem was proved in NOrderDomain module. (E without qualifiers refers to -ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer, -though, if the constraint "with Module NBaseMod := NPlusMod.NBaseMod" in the -declaration of this functor would not create an extra level of definitions -and there would be only one NDomainModule.E. *) -replace NDomainModule.E with NPlusMod.NBaseMod.NDomainModule.E by reflexivity. -fold (x1 == x2)%Int. fold (y1 == y2)%Int. -assert (H1' : (x1 == y1)%Int); [exact H1 |]. -(* We do this instead of "fold (x1 == y1)%Int in H1" *) -assert (H2' : (x2 == y2)%Int); [exact H2 |]. -rewrite H1'; rewrite H2'. reflexivity. -Qed. - -Open Local Scope IntScope. - -Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m. -Proof. -intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *) -Qed. - -Theorem lt_irr : forall n : Z, ~ (n < n). -Proof. -intros n; unfold lt, E; simpl. apply lt_irr. -(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *) -Qed. - -Theorem lt_succ : forall n m, n < (S m) <-> n <= m. -Proof. -intros n m; unfold lt, le, E; simpl. rewrite plus_succ_l; apply lt_succ. -Qed. - -End NatPairsOrder. - -(* Since to define the order on integers we need both plus and order -on natural numbers, we can export the properties of plus and order together *) -(*Module NatPairsPlusOrderProperties (NPlusMod : NPlusSig) - (NOrderModule : NOrderSig - with Module NBaseMod := NPlusMod.NBaseMod). -Module Export NatPairsPlusModule := NatPairsPlus NPlusMod. -Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule. -Module Export NatPairsPlusOrderPropertiesModule := - ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule. -End NatPairsPlusOrderProperties.*) -(* We cannot prove to Coq that NatPairsPlusModule.ZBaseMod and -NatPairsOrderModule.ZBaseMod are the same *) - - diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v deleted file mode 100644 index 2e658c181f..0000000000 --- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v +++ /dev/null @@ -1,83 +0,0 @@ -Require Import NPlus. -Require Export ZPlus. -Require Export ZPairsAxioms. - -Module NatPairsPlus (Import NPlusMod : NPlusSig) <: ZPlusSignature. -Module Export ZBaseMod := NatPairsInt NPlusMod. -Open Local Scope NatScope. - -Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)). -Definition minus (x y : Z) := ((fst x) + (snd y), (snd x) + (fst y)). -Definition uminus (x : Z) := (snd x, fst x). -(* Unfortunately, the elements of pair keep increasing, even during subtraction *) - -Notation "x + y" := (plus x y) : IntScope. -Notation "x - y" := (minus x y) : IntScope. -Notation "- x" := (uminus x) : IntScope. - -(* Below, we need to rewrite subtems that have several occurrences. -Since with the currect setoid_rewrite we cannot point an accurrence -using pattern, we use symmetry tactic to make a particular occurrence -the leftmost, since that is what rewrite will use. *) -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Proof. -unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl. -pose proof (plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 - (fst x2 + snd y2) (fst y2 + snd x2) H2) as H. -rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1. -Qed. - -Add Morphism minus with signature E ==> E ==> E as minus_wd. -Proof. -unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl. -rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2. -pose proof (NPlusMod.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 - (snd x2 + fst y2) (snd y2 + fst x2) H2) as H. -rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1. -Qed. - -Add Morphism uminus with signature E ==> E as uminus_wd. -Proof. -unfold E, plus; intros x y H; simpl. -rewrite plus_comm. symmetry. now rewrite plus_comm. -Qed. - -Open Local Scope IntScope. - -Theorem plus_0 : forall n, 0 + n == n. -Proof. -intro n; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_0_l. -Qed. - -Theorem plus_succ : forall n m, (S n) + m == S (n + m). -Proof. -intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_succ_l. -Qed. - -Theorem minus_0 : forall n, n - 0 == n. -Proof. -intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r. -Qed. - -Theorem minus_succ : forall n m, n - (S m) == P (n - m). -Proof. -intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_succ_r. -Qed. - -Theorem uminus_0 : - 0 == 0. -Proof. -unfold uminus, E; simpl. now rewrite plus_0_l. -Qed. - -Theorem uminus_succ : forall n, - (S n) == P (- n). -Proof. -reflexivity. -Qed. - -End NatPairsPlus. - -Module NatPairsPlusProperties (NPlusMod : NPlusSig). -Module Export NatPairsPlusModule := NatPairsPlus NPlusMod. -Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule. -End NatPairsPlusProperties. - diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v deleted file mode 100644 index 553c6df22f..0000000000 --- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v +++ /dev/null @@ -1,56 +0,0 @@ -Require Import Ring. -Require Import NTimes. -Require Export ZTimes. -Require Export ZPairsPlus. - -Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature. -Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *) -Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod. -Open Local Scope NatScope. - -Definition times (n m : Z) := - ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). - -Notation "x * y" := (times x y) : IntScope. - -Add Morphism times with signature E ==> E ==> E as times_wd. -Proof. -unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl. -stepl_ring (fst x1 * fst x2 + (snd x1 * snd x2 + fst y1 * snd y2 + snd y1 * fst y2)). -stepr_ring (fst x1 * snd x2 + (fst y1 * fst y2 + snd y1 * snd y2 + snd x1 * fst x2)). -apply plus_times_repl_pair with (n := fst y2) (m := snd y2); [| now idtac]. -stepl_ring (snd x1 * snd x2 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)). -stepr_ring (snd x1 * fst x2 + (fst x1 * snd y2 + fst y1 * fst y2 + snd y1 * snd y2)). -apply plus_times_repl_pair with (n := snd y2) (m := fst y2); - [| rewrite plus_comm; symmetry; now rewrite plus_comm]. -stepl_ring (snd y2 * snd x1 + (fst x1 * fst y2 + fst y1 * snd y2 + snd y1 * fst y2)). -stepr_ring (snd y2 * fst x1 + (snd x1 * fst y2 + fst y1 * fst y2 + snd y1 * snd y2)). -apply plus_times_repl_pair with (n := snd y1) (m := fst y1); - [| rewrite plus_comm; symmetry; now rewrite plus_comm]. -stepl_ring (fst y2 * fst x1 + (snd y2 * snd y1 + fst y1 * snd y2 + snd y1 * fst y2)). -stepr_ring (fst y2 * snd x1 + (snd y2 * fst y1 + fst y1 * fst y2 + snd y1 * snd y2)). -apply plus_times_repl_pair with (n := fst y1) (m := snd y1); [| now idtac]. -ring. -Qed. - -Open Local Scope IntScope. - -Theorem times_0 : forall n, n * 0 == 0. -Proof. -intro n; unfold times, E; simpl. -repeat rewrite times_0_r. now rewrite plus_assoc. -Qed. - -Theorem times_succ : forall n m, n * (S m) == n * m + n. -Proof. -intros n m; unfold times, S, E; simpl. -do 2 rewrite times_succ_r. ring. -Qed. - -End NatPairsTimes. - -Module NatPairsTimesProperties (NTimesMod : NTimesSig). -Module Export NatPairsTimesModule := NatPairsTimes NTimesMod. -Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule. -End NatPairsTimesProperties. - diff --git a/theories/Numbers/Integer/TreeMod/ZTreeMod.v b/theories/Numbers/Integer/TreeMod/ZTreeMod.v new file mode 100644 index 0000000000..7479868e9d --- /dev/null +++ b/theories/Numbers/Integer/TreeMod/ZTreeMod.v @@ -0,0 +1,216 @@ +Require Export NZAxioms. +Require Import NMake. (* contains W0Type *) +Require Import ZnZ. +Require Import Basic_type. (* contais base *) +Require Import ZAux. + +Module NZBigIntsAxiomsMod (Import BoundedIntsMod : W0Type) <: 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 NZE (n m : NZ) := [| n |] = [| m |]. +Definition NZ0 := w_op.(znz_0). +Definition NZsucc := w_op.(znz_succ). +Definition NZpred := w_op.(znz_pred). +Definition NZplus := w_op.(znz_add). +Definition NZminus := w_op.(znz_sub). +Definition NZtimes := w_op.(znz_mul). + +Theorem NZE_equiv : equiv NZ NZE. +Proof. +unfold equiv, reflexive, symmetric, transitive, NZE; repeat split; intros; auto. +now transitivity [| y |]. +Qed. + +Add Relation NZ NZE + reflexivity proved by (proj1 NZE_equiv) + symmetry proved by (proj2 (proj2 NZE_equiv)) + transitivity proved by (proj1 (proj2 NZE_equiv)) +as NZE_rel. + +Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. +Proof. +unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_succ). now rewrite H. +Qed. + +Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. +Proof. +unfold NZE; intros n m H. do 2 rewrite w_spec.(spec_pred). now rewrite H. +Qed. + +Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Proof. +unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_add). +now rewrite H1, H2. +Qed. + +Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. +Proof. +unfold NZE; intros n1 n2 H1 m1 m2 H2. do 2 rewrite w_spec.(spec_sub). +now rewrite H1, H2. +Qed. + +Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. +Proof. +unfold NZE; 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" := (NZE x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZE 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" := (NZplus x y) : IntScope. +Notation "x - y" := (NZminus x y) : IntScope. +Notation "x * y" := (NZtimes x y) : IntScope. + +Theorem gt_wB_1 : 1 < wB. +Proof. +unfold base. apply Zgt_pow_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 <- Zmod_plus; [ | apply gt_wB_0]. +reflexivity. +now rewrite Zmod_def_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 <- Zmod_minus; [ | apply gt_wB_0]. +reflexivity. +now rewrite Zmod_def_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_def_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, NZE. 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 NZE, 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 NZE 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 NZE ==> iff as A_morph. +Proof A_wd. + +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 NZE. assumption. +unfold NZE. 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_def_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 NZE. +apply B_holds. apply w_spec.(spec_to_Z). +unfold NZE, 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 NZplus_0_l : forall n : NZ, 0 + n == n. +Proof. +intro n; unfold NZplus, NZ0, NZE. rewrite w_spec.(spec_add). rewrite w_spec.(spec_0). +rewrite Zplus_0_l. rewrite Zmod_def_small; [reflexivity | apply w_spec.(spec_to_Z)]. +Qed. + +Theorem NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). +Proof. +intros n m; unfold NZplus, NZsucc, NZE. 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; [ |apply gt_wB_0]. +rewrite (Zplus_comm 1 [| m |]); now rewrite Zplus_assoc. +Qed. + +Theorem NZminus_0_r : forall n : NZ, n - 0 == n. +Proof. +intro n; unfold NZminus, NZ0, NZE. rewrite w_spec.(spec_sub). +rewrite w_spec.(spec_0). rewrite Zminus_0_r. apply NZ_to_Z_mod. +Qed. + +Theorem NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). +Proof. +intros n m; unfold NZminus, NZsucc, NZpred, NZE. +rewrite w_spec.(spec_pred). do 2 rewrite w_spec.(spec_sub). +rewrite w_spec.(spec_succ). rewrite Zminus_mod_idemp_r; [ | apply gt_wB_0]. +rewrite Zminus_mod_idemp_l; [ | apply gt_wB_0]. +now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z by auto with zarith. +Qed. + +Theorem NZtimes_0_r : forall n : NZ, n * 0 == 0. +Proof. +intro n; unfold NZtimes, NZ0, NZ, NZE. rewrite w_spec.(spec_mul). +rewrite w_spec.(spec_0). now rewrite Zmult_0_r. +Qed. + +Theorem NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. +Proof. +intros n m; unfold NZtimes, NZsucc, NZplus, NZE. rewrite w_spec.(spec_mul). +rewrite w_spec.(spec_add). rewrite w_spec.(spec_mul). rewrite w_spec.(spec_succ). +rewrite Zplus_mod_idemp_l; [ | apply gt_wB_0]. rewrite Zmult_mod_idemp_r; [ | apply gt_wB_0]. +rewrite Zmult_plus_distr_r. now rewrite Zmult_1_r. +Qed. + +End NZBigIntsAxiomsMod. |