diff options
| -rw-r--r-- | plugins/micromega/RMicromega.v | 6 | ||||
| -rw-r--r-- | plugins/nsatz/Nsatz.v | 12 | ||||
| -rw-r--r-- | plugins/omega/OmegaLemmas.v | 7 | ||||
| -rw-r--r-- | theories/Arith/Wf_nat.v | 17 | ||||
| -rw-r--r-- | theories/Bool/Bool.v | 10 | ||||
| -rw-r--r-- | theories/NArith/BinNat.v | 161 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 688 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 332 | ||||
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 2 | ||||
| -rw-r--r-- | theories/PArith/BinPos.v | 394 | ||||
| -rw-r--r-- | theories/PArith/Pminmax.v | 8 | ||||
| -rw-r--r-- | theories/PArith/Pnat.v | 511 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 41 | ||||
| -rw-r--r-- | theories/Reals/Rfunctions.v | 249 | ||||
| -rw-r--r-- | theories/ZArith/BinInt.v | 317 | ||||
| -rw-r--r-- | theories/ZArith/Wf_Z.v | 28 | ||||
| -rw-r--r-- | theories/ZArith/Zabs.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zcompare.v | 415 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv_def.v | 2 | ||||
| -rw-r--r-- | theories/ZArith/Zlog_def.v | 50 | ||||
| -rw-r--r-- | theories/ZArith/Zlogarithm.v | 23 | ||||
| -rw-r--r-- | theories/ZArith/Zmisc.v | 56 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 287 | ||||
| -rw-r--r-- | theories/ZArith/Zpow_def.v | 44 | ||||
| -rw-r--r-- | theories/ZArith/Zpower.v | 2 |
25 files changed, 1753 insertions, 1911 deletions
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 2b6ef8c5d..3f29a4fcf 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -67,7 +67,7 @@ Lemma RZSORaddon : SORaddon R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) Zeq_bool Zle_bool - IZR Nnat.nat_of_N pow. + IZR nat_of_N pow. Proof. constructor. constructor ; intros ; try reflexivity. @@ -94,7 +94,7 @@ Definition INZ (n:N) : R := | Npos p => IZR (Zpos p) end. -Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow. +Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR nat_of_N pow. Definition Reval_op2 (o:Op2) : R -> R -> Prop := @@ -112,7 +112,7 @@ Definition Reval_formula (e: PolEnv R) (ff : Formula Z) := let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs). Definition Reval_formula' := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow. + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR nat_of_N pow. Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index aa32b386c..e8e02f2ca 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -142,12 +142,12 @@ Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := Definition PhiR : list R -> PolZ -> R := (Pphi 0 ring_plus ring_mult (gen_phiZ 0 1 ring_plus ring_mult ring_opp)). -Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (Nnat.N_of_nat n). +Definition pow (r : R) (n : nat) := pow_N 1 ring_mult r (N_of_nat n). Definition PEevalR : list R -> PEZ -> R := PEeval 0 ring_plus ring_mult ring_sub ring_opp (gen_phiZ 0 1 ring_plus ring_mult ring_opp) - Nnat.nat_of_N pow. + nat_of_N pow. Lemma P0Z_correct : forall l, PhiR l P0Z = 0. Proof. trivial. Qed. @@ -177,8 +177,8 @@ Proof. Qed. Lemma R_power_theory - : power_theory 1 ring_mult ring_eq Nnat.nat_of_N pow. -apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. + : power_theory 1 ring_mult ring_eq nat_of_N pow. +apply mkpow_th. unfold pow. intros. rewrite Nnat.N_of_nat_of_N. ring. Qed. Lemma norm_correct : forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). @@ -288,7 +288,7 @@ Fixpoint interpret3 t fv {struct t}: R := | (PEopp t1) => let v1 := interpret3 t1 fv in (ring_opp v1) | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in pow v1 (Nnat.nat_of_N t2) + let v1 := interpret3 t1 fv in pow v1 (nat_of_N t2) | (PEc t1) => (IZR1 t1) | (PEX n) => List.nth (pred (nat_of_P n)) fv 0 end. @@ -484,7 +484,7 @@ Ltac nsatz_domain_generic radicalmax info lparam lvar tacsimpl Rd := tacsimpl; repeat (split;[assumption|idtac]); exact I | simpl in Hg2; tacsimpl; - apply Rdomain_pow with (interpret3 _ Rd c fv) (Nnat.nat_of_N r); auto with domain; + apply Rdomain_pow with (interpret3 _ Rd c fv) (nat_of_N r); auto with domain; tacsimpl; apply domain_axiom_one_zero || (simpl) || idtac "could not prove discrimination result" ] diff --git a/plugins/omega/OmegaLemmas.v b/plugins/omega/OmegaLemmas.v index ff433bbd8..5b6f4670f 100644 --- a/plugins/omega/OmegaLemmas.v +++ b/plugins/omega/OmegaLemmas.v @@ -298,3 +298,10 @@ Definition fast_Zred_factor5 (x y : Z) (P : Z -> Prop) Definition fast_Zred_factor6 (x : Z) (P : Z -> Prop) (H : P (x + 0)) := eq_ind_r P H (Zred_factor6 x). + +Theorem intro_Z : + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +Proof. + intros n; exists (Z_of_nat n); split; trivial. + rewrite Zmult_1_r, Zplus_0_r. apply Zle_0_nat. +Qed. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index c16a13dfb..d3d7b5835 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -270,7 +270,18 @@ Theorem iter_nat_plus : forall (n m:nat) (A:Type) (f:A -> A) (x:A), iter_nat (n + m) A f x = iter_nat n A f (iter_nat m A f x). Proof. - simple induction n; - [ simpl in |- *; auto with arith - | intros; simpl in |- *; apply f_equal with (f := f); apply H ]. + induction n; simpl; trivial. + intros. now f_equal. +Qed. + +(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], + then the iterates of [f] also preserve it. *) + +Theorem iter_nat_invariant : + forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop), + (forall x:A, Inv x -> Inv (f x)) -> + forall x:A, Inv x -> Inv (iter_nat n A f x). +Proof. + induction n; simpl; trivial. + intros A f Inv Hf x Hx. apply Hf, IHn; trivial. Qed. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index b13369368..f4649be04 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -257,6 +257,11 @@ Proof. intros. apply orb_false_iff; trivial. Qed. +Lemma orb_diag : forall b, b || b = b. +Proof. + destr_bool. +Qed. + (** [true] is a zero for [orb] *) Lemma orb_true_r : forall b:bool, b || true = true. @@ -362,6 +367,11 @@ Qed. Notation andb_b_false := andb_false_r (only parsing). Notation andb_false_b := andb_false_l (only parsing). +Lemma andb_diag : forall b, b && b = b. +Proof. + destr_bool. +Qed. + (** [true] is neutral for [andb] *) Lemma andb_true_r : forall b:bool, b && true = b. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index eb89fb20d..51c5b462b 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -152,6 +152,20 @@ Definition Nmax (n n' : N) := match Ncompare n n' with | Gt => n end. +(** Translation from [N] to [nat] and back. *) + +Definition nat_of_N (a:N) := + match a with + | N0 => O + | Npos p => nat_of_P p + end. + +Definition N_of_nat (n:nat) := + match n with + | O => N0 + | S n' => Npos (P_of_succ_nat n') + end. + (** Decidability of equality. *) Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }. @@ -229,7 +243,7 @@ Qed. Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n. Proof. -destruct n as [| p]; simpl. reflexivity. +intros [| p]; simpl. reflexivity. case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ). intro H; false_hyp H Psucc_not_one. Qed. @@ -249,7 +263,7 @@ Qed. Theorem Nplus_comm : forall n m:N, n + m = m + n. Proof. intros. -destruct n; destruct m; simpl in |- *; try reflexivity. +destruct n; destruct m; simpl; try reflexivity. rewrite Pplus_comm; reflexivity. Qed. @@ -259,51 +273,49 @@ intros. destruct n; try reflexivity. destruct m; try reflexivity. destruct p; try reflexivity. -simpl in |- *; rewrite Pplus_assoc; reflexivity. +simpl; rewrite Pplus_assoc; reflexivity. Qed. Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m). Proof. -destruct n; destruct m. - simpl in |- *; reflexivity. - unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity. - simpl in |- *; reflexivity. - simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. +destruct n, m. + simpl; reflexivity. + unfold Nsucc, Nplus; rewrite <- Pplus_one_succ_l; reflexivity. + simpl; reflexivity. + simpl; rewrite Pplus_succ_permute_l; reflexivity. Qed. Theorem Nsucc_0 : forall n : N, Nsucc n <> N0. Proof. -intro n; elim n; simpl Nsucc; intros; discriminate. +now destruct n. Qed. Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m. Proof. -destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H; - clear H; intro H. - symmetry in H; contradiction Psucc_not_one with p. - contradiction Psucc_not_one with p. - rewrite Psucc_inj with (1 := H); reflexivity. +intros [|p] [|q] H; simpl in *; trivial; injection H; clear H; intro H. + now elim (Psucc_not_one q). + now elim (Psucc_not_one p). + apply Psucc_inj in H. now f_equal. Qed. Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p. Proof. -intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *. + induction n using Nind. trivial. - intros n IHn m p H0; do 2 rewrite Nplus_succ in H0. - apply IHn; apply Nsucc_inj; assumption. + intros m p H; rewrite 2 Nplus_succ in H. + apply Nsucc_inj in H. now apply IHn. Qed. (** Properties of subtraction. *) Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'. Proof. -destruct n as [| p]; destruct n' as [| q]; unfold Nle; simpl; -split; intro H; try discriminate; try reflexivity. +intros [| p] [| q]; unfold Nle; simpl; +split; intro H; try easy. now elim H. -intro H1; apply Pminus_mask_Gt in H1. destruct H1 as [h [H1 _]]. -rewrite H1 in H; discriminate. -case_eq (Pcompare p q Eq); intro H1; rewrite H1 in H; try now elim H. -assert (H2 : p = q); [now apply Pcompare_Eq_eq |]. now rewrite H2, Pminus_mask_diag. +contradict H. now destruct (Pminus_mask_Gt _ _ H) as (h & -> & _). +destruct (Pcompare_spec p q); try now elim H. +subst. now rewrite Pminus_mask_diag. now rewrite Pminus_mask_Lt. Qed. @@ -314,10 +326,15 @@ Qed. Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m). Proof. -destruct n as [| p]; destruct m as [| q]; try reflexivity. +intros [|p] [|q]; trivial. now destruct p. simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. -now destruct (Pminus_mask p q) as [| r |]; [| destruct r |]. +now destruct (Pminus_mask p q) as [|[r|r|]|]. +Qed. + +Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1). +Proof. + intros [|[p|p|]]; trivial. Qed. (** Properties of multiplication *) @@ -334,21 +351,17 @@ Qed. Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. Proof. -destruct n as [| n]; destruct m as [| m]; simpl; auto. -rewrite Pmult_Sn_m; reflexivity. +intros [|n] [|m]; simpl; trivial. now rewrite Pmult_Sn_m. Qed. Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n. Proof. -destruct n; simpl in |- *; try reflexivity. -rewrite Pmult_1_r; reflexivity. +intros [|n]; simpl; trivial. now rewrite Pmult_1_r. Qed. Theorem Nmult_comm : forall n m:N, n * m = m * n. Proof. -intros. -destruct n; destruct m; simpl in |- *; try reflexivity. -rewrite Pmult_comm; reflexivity. +intros [|n] [|m]; simpl; trivial. now rewrite Pmult_comm. Qed. Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p. @@ -357,7 +370,7 @@ intros. destruct n; try reflexivity. destruct m; try reflexivity. destruct p; try reflexivity. -simpl in |- *; rewrite Pmult_assoc; reflexivity. +simpl; rewrite Pmult_assoc; reflexivity. Qed. Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p. @@ -365,7 +378,7 @@ Proof. intros. destruct n; try reflexivity. destruct m; destruct p; try reflexivity. -simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity. +simpl; rewrite Pmult_plus_distr_r; reflexivity. Qed. Theorem Nmult_plus_distr_l : forall n m p:N, p * (n + m) = p * n + p * m. @@ -400,7 +413,7 @@ Qed. Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m. Proof. -destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H; +destruct n as [| n]; destruct m as [| m]; simpl; intro H; reflexivity || (try discriminate H). rewrite (Pcompare_Eq_eq n m H); reflexivity. Qed. @@ -509,22 +522,6 @@ Proof. now apply (Pplus_lt_mono_l p). Qed. -Lemma Nmult_lt_mono_l : forall n m p, N0<n -> m<p -> n*m<n*p. -Proof. - intros [|n] m p. discriminate. intros _. - destruct m, p; try discriminate. auto. - simpl. - apply Pmult_lt_mono_l. -Qed. - -Lemma Nmult_le_mono_l : forall n m p, m<=p -> n*m<=n*p. -Proof. - intros [|n] m p. intros _ H. discriminate. - intros. apply Nle_lteq. apply Nle_lteq in H. destruct H; [left|right]. - now apply Nmult_lt_mono_l. - congruence. -Qed. - (** 0 is the least natural number *) Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. @@ -567,9 +564,10 @@ Qed. (** Power *) Definition Npow n p := - match p with - | N0 => Npos 1 - | Npos p => Piter_op Nmult p n + match p, n with + | N0, _ => Npos 1 + | _, N0 => N0 + | Npos p, Npos q => Npos (Ppow q p) end. Infix "^" := Npow : N_scope. @@ -579,53 +577,32 @@ Proof. reflexivity. Qed. Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p. Proof. - intros n p; destruct p; simpl. - now rewrite Nmult_1_r. - apply Piter_op_succ. apply Nmult_assoc. + intros [|q] [|p]; simpl; trivial; f_equal. + apply Ppow_succ_r. Qed. (** Base-2 logarithm *) -Fixpoint Plog2_N (p:positive) : N := - match p with - | p~0 => Nsucc (Plog2_N p) - | p~1 => Nsucc (Plog2_N p) - | 1 => N0 - end%positive. - Definition Nlog2 n := match n with - | N0 => N0 - | Npos p => Plog2_N p + | N0 => N0 + | Npos 1 => N0 + | Npos (p~0) => Npos (Psize_pos p) + | Npos (p~1) => Npos (Psize_pos p) end. -Lemma Plog2_N_spec : forall p, - (Npos 2)^(Plog2_N p) <= Npos p < (Npos 2)^(Nsucc (Plog2_N p)). -Proof. - induction p; simpl; try rewrite 2 Npow_succ_r. - (* p~1 *) - change (Npos p~1) with (Nsucc (Npos 2 * Npos p)). - split; destruct IHp as [LE LT]. - apply Nle_trans with (Npos 2 * Npos p). - now apply Nmult_le_mono_l. - apply Nle_lteq. left. - apply Ncompare_n_Sm. now right. - apply Nle_succ_l. apply Nle_succ_l in LT. - change (Nsucc (Nsucc (Npos 2 * Npos p))) with (Npos 2 * (Nsucc (Npos p))). - now apply Nmult_le_mono_l. - (* p~0 *) - change (Npos p~0) with (Npos 2 * Npos p). - split; destruct IHp. - now apply Nmult_le_mono_l. - now apply Nmult_lt_mono_l. - (* 1 *) - now split. -Qed. - Lemma Nlog2_spec : forall n, N0 < n -> (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)). Proof. - intros [|n] Hn. discriminate. apply Plog2_N_spec. + intros [|[p|p|]] H; discriminate H || clear H; simpl; split. + eapply Nle_trans with (Npos (p~0)). + apply Psize_pos_le. + apply Nle_lteq; left. exact (Pcompare_p_Sp (p~0)). + apply Psize_pos_gt. + apply Psize_pos_le. + apply Psize_pos_gt. + discriminate. + reflexivity. Qed. Lemma Nlog2_nonpos : forall n, n<=N0 -> Nlog2 n = N0. @@ -643,8 +620,8 @@ Definition Neven n := end. Definition Nodd n := negb (Neven n). -Local Notation "1" := (Npos xH) : N_scope. -Local Notation "2" := (Npos (xO xH)) : N_scope. +Local Notation "1" := (Npos 1) : N_scope. +Local Notation "2" := (Npos 2) : N_scope. Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m. Proof. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 1992268ab..98e88c6a2 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,308 +6,542 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Bool Setoid Bvector BinPos BinNat. +Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat + Pnat Nnat Ndiv_def. + +Local Open Scope positive_scope. (** Operation over bits of a [N] number. *) -(** [xor] *) +(** Logical [or] *) + +Fixpoint Por (p q : positive) : positive := + match p, q with + | 1, q~0 => q~1 + | 1, _ => q + | p~0, 1 => p~1 + | _, 1 => p + | p~0, q~0 => (Por p q)~0 + | p~0, q~1 => (Por p q)~1 + | p~1, q~0 => (Por p q)~1 + | p~1, q~1 => (Por p q)~1 + end. -Fixpoint Pxor (p1 p2:positive) : N := - match p1, p2 with - | xH, xH => N0 - | xH, xO p2 => Npos (xI p2) - | xH, xI p2 => Npos (xO p2) - | xO p1, xH => Npos (xI p1) - | xO p1, xO p2 => Ndouble (Pxor p1 p2) - | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2) - | xI p1, xH => Npos (xO p1) - | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2) - | xI p1, xI p2 => Ndouble (Pxor p1 p2) +Definition Nor n m := + match n, m with + | N0, _ => m + | _, N0 => n + | Npos p, Npos q => Npos (Por p q) + end. + +(** Logical [and] *) + +Fixpoint Pand (p q : positive) : N := + match p, q with + | 1, q~0 => N0 + | 1, _ => Npos 1 + | p~0, 1 => N0 + | _, 1 => Npos 1 + | p~0, q~0 => Ndouble (Pand p q) + | p~0, q~1 => Ndouble (Pand p q) + | p~1, q~0 => Ndouble (Pand p q) + | p~1, q~1 => Ndouble_plus_one (Pand p q) end. -Definition Nxor (n n':N) := - match n, n' with - | N0, _ => n' +Definition Nand n m := + match n, m with + | N0, _ => N0 + | _, N0 => N0 + | Npos p, Npos q => Pand p q + end. + +(** Logical [diff] *) + +Fixpoint Pdiff (p q:positive) : N := + match p, q with + | 1, q~0 => Npos 1 + | 1, _ => N0 + | _~0, 1 => Npos p + | p~1, 1 => Npos (p~0) + | p~0, q~0 => Ndouble (Pdiff p q) + | p~0, q~1 => Ndouble (Pdiff p q) + | p~1, q~1 => Ndouble (Pdiff p q) + | p~1, q~0 => Ndouble_plus_one (Pdiff p q) + end. + +Fixpoint Ndiff n m := + match n, m with + | N0, _ => N0 | _, N0 => n - | Npos p, Npos p' => Pxor p p' + | Npos p, Npos q => Pdiff p q + end. + +(** [xor] *) + +Fixpoint Pxor (p q:positive) : N := + match p, q with + | 1, 1 => N0 + | 1, q~0 => Npos (q~1) + | 1, q~1 => Npos (q~0) + | p~0, 1 => Npos (p~1) + | p~0, q~0 => Ndouble (Pxor p q) + | p~0, q~1 => Ndouble_plus_one (Pxor p q) + | p~1, 1 => Npos (p~0) + | p~1, q~0 => Ndouble_plus_one (Pxor p q) + | p~1, q~1 => Ndouble (Pxor p q) + end. + +Definition Nxor (n m:N) := + match n, m with + | N0, _ => m + | _, N0 => n + | Npos p, Npos q => Pxor p q + end. + +(** For proving properties of these operations, we will use + an equivalence with functional streams of bit, cf [eqf] below *) + +(** Shift *) + +Definition Nshiftl_nat (a:N)(n:nat) := iter_nat n _ Ndouble a. + +Definition Nshiftr_nat (a:N)(n:nat) := iter_nat n _ Ndiv2 a. + +Definition Nshiftr a n := + match n with + | N0 => a + | Npos p => iter_pos p _ Ndiv2 a + end. + +Definition Nshiftl a n := + match a, n with + | _, N0 => a + | N0, _ => a + | Npos p, Npos q => Npos (iter_pos q _ xO p) end. -Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n. +(** Checking whether a particular bit is set on not *) + +Fixpoint Pbit (p:positive) : nat -> bool := + match p with + | 1 => fun n => match n with + | O => true + | S _ => false + end + | p~0 => fun n => match n with + | O => false + | S n' => Pbit p n' + end + | p~1 => fun n => match n with + | O => true + | S n' => Pbit p n' + end + end. + +Definition Nbit (a:N) := + match a with + | N0 => fun _ => false + | Npos p => Pbit p + end. + +(** Same, but with index in N *) + +Fixpoint Ptestbit p n := + match p, n with + | p~0, N0 => false + | _, N0 => true + | 1, _ => false + | p~0, _ => Ptestbit p (Npred n) + | p~1, _ => Ptestbit p (Npred n) + end. + +Definition Ntestbit a n := + match a with + | N0 => false + | Npos p => Ptestbit p n + end. + +Local Close Scope positive_scope. +Local Open Scope N_scope. + +(** Equivalence of Pbit and Ptestbit *) + +Lemma Ptestbit_Pbit : + forall p n, Ptestbit p (N_of_nat n) = Pbit p n. Proof. - trivial. + induction p as [p IH|p IH| ]; intros n; simpl. + rewrite <- N_of_pred, IH; destruct n; trivial. + rewrite <- N_of_pred, IH; destruct n; trivial. + destruct n; trivial. Qed. -Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n. +Lemma Ntestbit_Nbit : forall a n, Ntestbit a (N_of_nat n) = Nbit a n. Proof. - destruct n; trivial. + destruct a. trivial. apply Ptestbit_Pbit. Qed. -Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n. +Lemma Pbit_Ptestbit : + forall p n, Pbit p (nat_of_N n) = Ptestbit p n. Proof. - destruct n; destruct n'; simpl; auto. - generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl; - auto. - destruct p0; trivial; rewrite Hrecp; trivial. - destruct p0; trivial; rewrite Hrecp; trivial. - destruct p0 as [p| p| ]; simpl; auto. + intros; now rewrite <- Ptestbit_Pbit, N_of_nat_of_N. Qed. -Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0. +Lemma Nbit_Ntestbit : + forall a n, Nbit a (nat_of_N n) = Ntestbit a n. Proof. - destruct n; trivial. - simpl. induction p as [p IHp| p IHp| ]; trivial. - simpl. rewrite IHp; reflexivity. - simpl. rewrite IHp; reflexivity. + destruct a. trivial. apply Pbit_Ptestbit. Qed. -(** Checking whether a particular bit is set on not *) +(** Equivalence of shifts, N and nat versions *) -Fixpoint Pbit (p:positive) : nat -> bool := - match p with - | xH => fun n:nat => match n with - | O => true - | S _ => false - end - | xO p => - fun n:nat => match n with - | O => false - | S n' => Pbit p n' - end - | xI p => fun n:nat => match n with - | O => true - | S n' => Pbit p n' - end - end. +Lemma Nshiftr_nat_equiv : + forall a n, Nshiftr_nat a (nat_of_N n) = Nshiftr a n. +Proof. + intros a [|n]; simpl; unfold Nshiftr_nat. + trivial. + symmetry. apply iter_nat_of_P. +Qed. -Definition Nbit (a:N) := - match a with - | N0 => fun _ => false - | Npos p => Pbit p - end. +Lemma Nshiftr_equiv_nat : + forall a n, Nshiftr a (N_of_nat n) = Nshiftr_nat a n. +Proof. + intros. now rewrite <- Nshiftr_nat_equiv, nat_of_N_of_nat. +Qed. + +Lemma Nshiftl_nat_equiv : + forall a n, Nshiftl_nat a (nat_of_N n) = Nshiftl a n. +Proof. + intros [|a] [|n]; simpl; unfold Nshiftl_nat; trivial. + apply iter_nat_invariant; intros; now subst. + rewrite <- iter_nat_of_P. symmetry. now apply iter_pos_swap_gen. +Qed. + +Lemma Nshiftl_equiv_nat : + forall a n, Nshiftl a (N_of_nat n) = Nshiftl_nat a n. +Proof. + intros. now rewrite <- Nshiftl_nat_equiv, nat_of_N_of_nat. +Qed. + +(** Correctness proofs for shifts *) -(** Auxiliary results about streams of bits *) +Lemma Nshiftl_mult_pow : forall a n, Nshiftl a n = a * 2^n. +Proof. + intros [|a] [|n]; simpl; trivial. + now rewrite Pmult_1_r. + f_equal. + set (f x := Pmult x a). + rewrite Pmult_comm. fold (f (2^n))%positive. + change a with (f xH). + unfold Ppow. symmetry. now apply iter_pos_swap_gen. +Qed. + +(* +Lemma Nshiftr_div_pow : forall a n, Nshiftr a n = a / 2^n. +*) + +(** Equality over functional streams of bits *) Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. -Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. +Instance eqf_equiv : Equivalence eqf. +Proof. + split; congruence. +Qed. + +Local Infix "==" := eqf (at level 70, no associativity). + +(** If two numbers produce the same stream of bits, they are equal. *) + +Local Notation Step H := (fun n => H (S n)). + +Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)). Proof. - unfold eqf. intros. rewrite H. reflexivity. + induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). + apply (IHp (Step H)). Qed. -Lemma eqf_refl : forall f:nat -> bool, eqf f f. +Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'. Proof. - unfold eqf. trivial. + induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial; + try discriminate (H O). + f_equal. apply (IHp _ (Step H)). + destruct (Pbit_faithful_0 _ (Step H)). + f_equal. apply (IHp _ (Step H)). + symmetry in H. destruct (Pbit_faithful_0 _ (Step H)). Qed. -Lemma eqf_trans : - forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''. +Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'. Proof. - unfold eqf. intros. rewrite H. exact (H0 n). + intros [|p] [|p'] H; trivial. + symmetry in H. destruct (Pbit_faithful_0 _ H). + destruct (Pbit_faithful_0 _ H). + f_equal. apply Pbit_faithful, H. Qed. +Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'. +Proof. + split. apply Nbit_faithful. intros; now subst. +Qed. + + +(** Bit operations for functional streams of bits *) + +Definition orf (f g:nat -> bool) (n:nat) := (f n) || (g n). +Definition andf (f g:nat -> bool) (n:nat) := (f n) && (g n). +Definition difff (f g:nat -> bool) (n:nat) := (f n) && negb (g n). Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n). -Lemma xorf_eq : - forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'. +Instance eqf_orf : Proper (eqf==>eqf==>eqf) orf. Proof. - unfold eqf, xorf. intros. apply xorb_eq, H. + unfold orf. congruence. Qed. -Lemma xorf_assoc : - forall f f' f'', - eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')). +Instance eqf_andf : Proper (eqf==>eqf==>eqf) andf. Proof. - unfold eqf, xorf. intros. apply xorb_assoc. + unfold andf. congruence. Qed. -Lemma eqf_xorf : - forall f f' f'' f''', - eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f'''). +Instance eqf_difff : Proper (eqf==>eqf==>eqf) difff. Proof. - unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity. + unfold difff. congruence. Qed. -(** End of auxilliary results *) +Instance eqf_xorf : Proper (eqf==>eqf==>eqf) xorf. +Proof. + unfold xorf. congruence. +Qed. -(** This part is aimed at proving that if two numbers produce - the same stream of bits, then they are equal. *) +(** We now describe the semantics of [Nxor] and other bitwise + operations in terms of bit streams. *) -Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a. +Lemma Pxor_semantics : forall p p', + Nbit (Pxor p p') == xorf (Pbit p) (Pbit p'). Proof. - destruct a. trivial. - induction p as [p IHp| p IHp| ]; intro H. - absurd (N0 = Npos p). discriminate. - exact (IHp (fun n => H (S n))). - absurd (N0 = Npos p). discriminate. - exact (IHp (fun n => H (S n))). - absurd (false = true). discriminate. - exact (H 0). + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) || + (unfold xorf; now rewrite ?xorb_false_l, ?xorb_false_r). Qed. -Lemma Nbit_faithful_2 : - forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a. +Lemma Nxor_semantics : forall a a', + Nbit (Nxor a a') == xorf (Nbit a) (Nbit a'). Proof. - destruct a. intros. absurd (true = false). discriminate. - exact (H 0). - destruct p. intro H. absurd (N0 = Npos p). discriminate. - exact (Nbit_faithful_1 (Npos p) (fun n:nat => H (S n))). - intros. absurd (true = false). discriminate. - exact (H 0). - trivial. + intros [|p] [|p'] n; simpl; unfold xorf; trivial. + now rewrite xorb_false_l. + now rewrite xorb_false_r. + apply Pxor_semantics. Qed. -Lemma Nbit_faithful_3 : - forall (a:N) (p:positive), - (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> - eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a. +Lemma Por_semantics : forall p p', + Pbit (Por p p') == orf (Pbit p) (Pbit p'). Proof. - destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))). - intro. rewrite (Nbit_faithful_1 (Npos (xO p)) H1). reflexivity. - unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity. - destruct p. discriminate (H0 O). - rewrite (H p (fun n => H0 (S n))). reflexivity. - discriminate (H0 0). + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; + unfold orf; apply (IHp p' n) || now rewrite orb_false_r. Qed. -Lemma Nbit_faithful_4 : - forall (a:N) (p:positive), - (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> - eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a. +Lemma Nor_semantics : forall a a', + Nbit (Nor a a') == orf (Nbit a) (Nbit a'). Proof. - destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))). - intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity. - intro. rewrite H0. reflexivity. - destruct p. rewrite (H p (fun n:nat => H0 (S n))). reflexivity. - discriminate (H0 0). - cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))). - intro. discriminate (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))). - intro. rewrite H0. reflexivity. + intros [|p] [|p'] n; simpl; unfold orf; trivial. + now rewrite orb_false_r. + apply Por_semantics. Qed. -Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'. +Lemma Pand_semantics : forall p p', + Nbit (Pand p p') == andf (Pbit p) (Pbit p'). Proof. - destruct a. exact Nbit_faithful_1. - induction p. intros a' H. apply Nbit_faithful_4. intros. - assert (Npos p = Npos p') by exact (IHp (Npos p') H0). - inversion H1. reflexivity. - assumption. - intros. apply Nbit_faithful_3. intros. - assert (Npos p = Npos p') by exact (IHp (Npos p') H0). - inversion H1. reflexivity. - assumption. - exact Nbit_faithful_2. + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) || + (unfold andf; now rewrite andb_false_r). Qed. -(** We now describe the semantics of [Nxor] in terms of bit streams. *) +Lemma Nand_semantics : forall a a', + Nbit (Nand a a') == andf (Nbit a) (Nbit a'). +Proof. + intros [|p] [|p'] n; simpl; unfold andf; trivial. + now rewrite andb_false_r. + apply Pand_semantics. +Qed. -Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0. +Lemma Pdiff_semantics : forall p p', + Nbit (Pdiff p p') == difff (Pbit p) (Pbit p'). Proof. - trivial. + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) || + (unfold difff; simpl; now rewrite andb_true_r). Qed. -Lemma Nxor_sem_2 : - forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0). +Lemma Ndiff_semantics : forall a a', + Nbit (Ndiff a a') == difff (Nbit a) (Nbit a'). Proof. - intro. destruct a'. trivial. - destruct p; trivial. + intros [|p] [|p'] n; simpl; unfold difff; trivial. + simpl. now rewrite andb_true_r. + apply Pdiff_semantics. Qed. -Lemma Nxor_sem_3 : - forall (p:positive) (a':N), - Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0. +Hint Rewrite Nxor_semantics Nor_semantics + Nand_semantics Ndiff_semantics : bitwise_semantics. + +Ltac bitwise_semantics := + apply Nbit_faithful; autorewrite with bitwise_semantics; + intro n; unfold xorf, orf, andf, difff. + +(** Now, we can easily deduce properties of [Nxor] and others + from properties of [xorb] and others. *) + +Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'. Proof. - intros. destruct a'. trivial. - simpl. destruct p0; trivial. - destruct (Pxor p p0); trivial. - destruct (Pxor p p0); trivial. + intros a a' H. bitwise_semantics. apply xorb_eq. + rewrite <- Nbit_faithful_iff, Nxor_semantics in H. apply H. Qed. -Lemma Nxor_sem_4 : - forall (p:positive) (a':N), - Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0). +Lemma Nxor_nilpotent : forall a, Nxor a a = 0. Proof. - intros. destruct a'. trivial. - simpl. destruct p0; trivial. - destruct (Pxor p p0); trivial. - destruct (Pxor p p0); trivial. + intros. bitwise_semantics. apply xorb_nilpotent. Qed. -Lemma Nxor_sem_5 : - forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0. +Lemma Nxor_0_l : forall n, Nxor 0 n = n. Proof. - destruct a; intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial. - destruct p. apply Nxor_sem_4. - change (Nbit (Nxor (Npos (xO p)) a') 0 = xorb false (Nbit a' 0)). - rewrite false_xorb. apply Nxor_sem_3. apply Nxor_sem_2. + trivial. Qed. +Notation Nxor_neutral_left := Nxor_0_l (only parsing). -Lemma Nxor_sem_6 : - forall n:nat, - (forall a a':N, Nbit (Nxor a a') n = xorf (Nbit a) (Nbit a') n) -> - forall a a':N, - Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n). +Lemma Nxor_0_r : forall n, Nxor n 0 = n. Proof. - intros. -(* pose proof (fun p1 p2 => H (Npos p1) (Npos p2)) as H'. clear H. rename H' into H.*) - generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H. - unfold xorf in *. - destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity. - destruct a' as [|p0]. - simpl Nbit; rewrite xorb_false. reflexivity. - destruct p. destruct p0; simpl Nbit in *. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite xorb_false. reflexivity. - destruct p0; simpl Nbit in *. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite xorb_false. reflexivity. - simpl Nbit. rewrite false_xorb. destruct p0; trivial. -Qed. - -Lemma Nxor_semantics : - forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')). -Proof. - unfold eqf. intros; generalize a, a'. induction n. - apply Nxor_sem_5. apply Nxor_sem_6; assumption. -Qed. - -(** Consequences: - - only equal numbers lead to a null xor - - xor is associative -*) + destruct n; trivial. +Qed. +Notation Nxor_neutral_right := Nxor_0_r (only parsing). -Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'. +Lemma Nxor_comm : forall a a', Nxor a a' = Nxor a' a. Proof. - intros. apply Nbit_faithful, xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')). - apply eqf_sym, Nxor_semantics. - rewrite H. unfold eqf. trivial. + intros. bitwise_semantics. apply xorb_comm. Qed. Lemma Nxor_assoc : - forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a''). -Proof. - intros. apply Nbit_faithful. - apply eqf_trans with (xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')). - apply eqf_trans with (xorf (Nbit (Nxor a a')) (Nbit a'')). - apply Nxor_semantics. - apply eqf_xorf. apply Nxor_semantics. - apply eqf_refl. - apply eqf_trans with (xorf (Nbit a) (xorf (Nbit a') (Nbit a''))). - apply xorf_assoc. - apply eqf_trans with (xorf (Nbit a) (Nbit (Nxor a' a''))). - apply eqf_xorf. apply eqf_refl. - apply eqf_sym, Nxor_semantics. - apply eqf_sym, Nxor_semantics. + forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a''). +Proof. + intros. bitwise_semantics. apply xorb_assoc. +Qed. + +Lemma Nor_0_l : forall n, Nor 0 n = n. +Proof. + trivial. +Qed. + +Lemma Nor_0_r : forall n, Nor n 0 = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Nor_comm : forall a a', Nor a a' = Nor a' a. +Proof. + intros. bitwise_semantics. apply orb_comm. +Qed. + +Lemma Nor_assoc : + forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''. +Proof. + intros. bitwise_semantics. apply orb_assoc. +Qed. + +Lemma Nor_diag : forall a, Nor a a = a. +Proof. + intros. bitwise_semantics. apply orb_diag. +Qed. + +Lemma Nand_0_l : forall n, Nand 0 n = 0. +Proof. + trivial. +Qed. + +Lemma Nand_0_r : forall n, Nand n 0 = 0. +Proof. + destruct n; trivial. +Qed. + +Lemma Nand_comm : forall a a', Nand a a' = Nand a' a. +Proof. + intros. bitwise_semantics. apply andb_comm. +Qed. + +Lemma Nand_assoc : + forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''. +Proof. + intros. bitwise_semantics. apply andb_assoc. +Qed. + +Lemma Nand_diag : forall a, Nand a a = a. +Proof. + intros. bitwise_semantics. apply andb_diag. +Qed. + +Lemma Ndiff_0_l : forall n, Ndiff 0 n = 0. +Proof. + trivial. Qed. +Lemma Ndiff_0_r : forall n, Ndiff n 0 = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndiff_diag : forall a, Ndiff a a = 0. +Proof. + intros. bitwise_semantics. apply andb_negb_r. +Qed. + +Lemma Nor_and_distr_l : forall a b c, + Nor (Nand a b) c = Nand (Nor a c) (Nor b c). +Proof. + intros. bitwise_semantics. apply orb_andb_distrib_l. +Qed. + +Lemma Nor_and_distr_r : forall a b c, + Nor a (Nand b c) = Nand (Nor a b) (Nor a c). +Proof. + intros. bitwise_semantics. apply orb_andb_distrib_r. +Qed. + +Lemma Nand_or_distr_l : forall a b c, + Nand (Nor a b) c = Nor (Nand a c) (Nand b c). +Proof. + intros. bitwise_semantics. apply andb_orb_distrib_l. +Qed. + +Lemma Nand_or_distr_r : forall a b c, + Nand a (Nor b c) = Nor (Nand a b) (Nand a c). +Proof. + intros. bitwise_semantics. apply andb_orb_distrib_r. +Qed. + +Lemma Ndiff_diff_l : forall a b c, + Ndiff (Ndiff a b) c = Ndiff a (Nor b c). +Proof. + intros. bitwise_semantics. now rewrite negb_orb, andb_assoc. +Qed. + +Lemma Nor_diff_and : forall a b, + Nor (Ndiff a b) (Nand a b) = a. +Proof. + intros. bitwise_semantics. + now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r. +Qed. + +Lemma Nand_diff : forall a b, + Nand (Ndiff a b) b = 0. +Proof. + intros. bitwise_semantics. + now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r. +Qed. + +Local Close Scope N_scope. + (** Checking whether a number is odd, i.e. if its lower bit is set. *) Definition Nbit0 (n:N) := match n with | N0 => false - | Npos (xO _) => false + | Npos (_~0) => false | _ => true end. @@ -358,7 +592,7 @@ Qed. Lemma Nxor_bit0 : forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a'). Proof. - intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' 0). + intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O). unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity. Qed. @@ -554,7 +788,7 @@ Qed. (** Number of digits in a number *) Definition Nsize (n:N) : nat := match n with - | N0 => 0%nat + | N0 => O | Npos p => Psize p end. @@ -719,18 +953,40 @@ induction n; simpl in *; intros; destruct p; auto with arith. inversion H; inversion H1. Qed. -(** Xor is the same in the two worlds. *) +(** Binary bitwise operations are the same in the two worlds. *) Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). Proof. -induction n. -intros. +induction n; intros bv bv'. +rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. +rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. +rewrite IHn. +destruct (Vhead bool n bv), (Vhead bool n bv'), + (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); + simpl; auto. +Qed. + +Lemma Nor_BVor : forall n (bv bv' : Bvector n), + Bv2N _ (BVor _ bv bv') = Nor (Bv2N _ bv) (Bv2N _ bv'). +Proof. +induction n; intros bv bv'. rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. -intros. rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. rewrite IHn. -destruct (Vhead bool n bv); destruct (Vhead bool n bv'); - destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto. +destruct (Vhead bool n bv), (Vhead bool n bv'), + (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); + simpl; auto. Qed. +Lemma Nand_BVand : forall n (bv bv' : Bvector n), + Bv2N _ (BVand _ bv bv') = Nand (Bv2N _ bv) (Bv2N _ bv'). +Proof. +induction n; intros bv bv'. +rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. +rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. +rewrite IHn. +destruct (Vhead bool n bv), (Vhead bool n bv'), + (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv')); + simpl; auto. +Qed. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 93fdfff7a..05ca4a550 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,149 +6,86 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Arith_base. -Require Import Compare_dec. -Require Import Sumbool. -Require Import Div2. -Require Import Min. -Require Import Max. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. -Require Import Pnat. -Require Import Znat. - -(** Translation from [N] to [nat] and back. *) - -Definition nat_of_N (a:N) := - match a with - | N0 => 0%nat - | Npos p => nat_of_P p - end. - -Definition N_of_nat (n:nat) := - match n with - | O => N0 - | S n' => Npos (P_of_succ_nat n') - end. +Require Import Arith_base Compare_dec Sumbool Div2 Min Max. +Require Import BinPos BinNat Pnat. Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a. Proof. destruct a as [| p]. reflexivity. - simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. - rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. + simpl. elim (nat_of_P_is_S p). intros n H. rewrite H. simpl. + rewrite <- nat_of_P_of_succ_nat in H. rewrite nat_of_P_inj with (1 := H). reflexivity. Qed. Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n. Proof. induction n. trivial. - intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ. + intros. simpl. apply nat_of_P_of_succ_nat. Qed. -(** Interaction of this translation and usual operations. *) - -Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a). +Lemma nat_of_N_inj : forall n n', nat_of_N n = nat_of_N n' -> n = n'. Proof. - destruct a; simpl nat_of_N; auto. - apply nat_of_P_xO. + intros n n' H. + rewrite <- (N_of_nat_of_N n), <- (N_of_nat_of_N n'). now f_equal. Qed. -Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n). +Lemma N_of_nat_inj : forall n n', N_of_nat n = N_of_nat n' -> n = n'. Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndouble. - apply N_of_nat_of_N. + intros n n' H. + rewrite <- (nat_of_N_of_nat n), <- (nat_of_N_of_nat n'). now f_equal. Qed. -Lemma nat_of_Ndouble_plus_one : - forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). +Hint Rewrite nat_of_N_of_nat N_of_nat_of_N : Nnat. + +(** Interaction of this translation and usual operations. *) + +Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a). Proof. - destruct a; simpl nat_of_N; auto. - apply nat_of_P_xI. + destruct a; simpl nat_of_N; trivial. apply nat_of_P_xO. Qed. -Lemma N_of_double_plus_one : - forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). +Lemma nat_of_Ndouble_plus_one : + forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndouble_plus_one. - apply N_of_nat_of_N. + destruct a; simpl nat_of_N; trivial. apply nat_of_P_xI. Qed. Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a). Proof. destruct a; simpl. apply nat_of_P_xH. - apply nat_of_P_succ_morphism. -Qed. - -Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Nsucc. - apply N_of_nat_of_N. + apply Psucc_S. Qed. Lemma nat_of_Nplus : forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a'). Proof. destruct a; destruct a'; simpl; auto. - apply nat_of_P_plus_morphism. + apply Pplus_plus. Qed. -Lemma N_of_plus : - forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). +Lemma nat_of_Nmult : + forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nplus. - apply N_of_nat_of_N. + destruct a; destruct a'; simpl; auto. + apply Pmult_mult. Qed. Lemma nat_of_Nminus : forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. Proof. - destruct a; destruct a'; simpl; auto with arith. - case_eq (Pcompare p p0 Eq); simpl; intros. - rewrite (Pcompare_Eq_eq _ _ H); auto with arith. - rewrite Pminus_mask_diag. simpl. apply minus_n_n. - rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl. - symmetry; apply not_le_minus_0. auto with arith. assumption. - pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl. - replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1). - apply nat_of_P_minus_morphism; auto. -Qed. - -Lemma N_of_minus : - forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nminus. - apply N_of_nat_of_N. -Qed. - -Lemma nat_of_Nmult : - forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). -Proof. - destruct a; destruct a'; simpl; auto. - apply nat_of_P_mult_morphism. + intros [|a] [|a']; simpl; auto with arith. + destruct (Pcompare_spec a a'). + subst. now rewrite Pminus_mask_diag, <- minus_n_n. + rewrite Pminus_mask_Lt by trivial. apply Plt_lt in H. + simpl; symmetry; apply not_le_minus_0; auto with arith. + destruct (Pminus_mask_Gt a a' (ZC2 _ _ H)) as (q & -> & Hq & _). + simpl. apply plus_minus. now rewrite <- Hq, Pplus_plus. Qed. -Lemma N_of_mult : - forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). +Lemma nat_of_Npred : forall a, nat_of_N (Npred a) = pred (nat_of_N a). Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmult. - apply N_of_nat_of_N. + intros. rewrite pred_of_minus, Npred_minus. apply nat_of_Nminus. Qed. Lemma nat_of_Ndiv2 : @@ -162,205 +99,92 @@ Proof. rewrite div2_double; auto. Qed. -Lemma N_of_div2 : - forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - rewrite <- nat_of_Ndiv2. - apply N_of_nat_of_N. -Qed. - Lemma nat_of_Ncompare : forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). Proof. - destruct a; destruct a'; simpl. - reflexivity. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - apply nat_of_P_compare_morphism. -Qed. - -Lemma N_of_nat_compare : - forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - symmetry; apply nat_of_Ncompare. -Qed. - -Lemma nat_of_Nmin : - forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). -Proof. - intros; unfold Nmin; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply min_l; rewrite e; auto with arith. -Qed. - -Lemma N_of_min : - forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmin. - apply N_of_nat_of_N. + destruct a; destruct a'; simpl; trivial. + now destruct (nat_of_P_is_S p) as (n,->). + now destruct (nat_of_P_is_S p) as (n,->). + apply Pcompare_nat_compare. Qed. Lemma nat_of_Nmax : forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). Proof. - intros; unfold Nmax; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply max_r; rewrite e; auto with arith. -Qed. - -Lemma N_of_max : - forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). -Proof. - intros. - pattern n at 1; rewrite <- (nat_of_N_of_nat n). - pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). - rewrite <- nat_of_Nmax. - apply N_of_nat_of_N. + intros; unfold Nmax; rewrite nat_of_Ncompare. symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -(** Properties concerning [Z_of_N] *) - -Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n. -Proof. - destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. -Qed. - -Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m. -Proof. - intros; f_equal; assumption. -Qed. - -Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m. -Proof. - intros [|n] [|m]; simpl; intros; try discriminate; congruence. -Qed. - -Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m. -Proof. - split; [apply Z_of_N_eq | apply Z_of_N_eq_rev]. -Qed. - -Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z. -Proof. - split; [apply Z_of_N_le | apply Z_of_N_le_rev]. -Qed. - -Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z. -Proof. - split; [apply Z_of_N_lt | apply Z_of_N_lt_rev]. -Qed. - -Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. - -Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z. -Proof. - split; [apply Z_of_N_ge | apply Z_of_N_ge_rev]. -Qed. - -Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z. +Lemma nat_of_Nmin : + forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). Proof. - intros [|n] [|m]; simpl; auto. + intros; unfold Nmin; rewrite nat_of_Ncompare. symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. +Hint Rewrite nat_of_Ndouble nat_of_Ndouble_plus_one + nat_of_Nsucc nat_of_Nplus nat_of_Nmult nat_of_Nminus + nat_of_Npred nat_of_Ndiv2 nat_of_Nmax nat_of_Nmin : Nnat. -Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z. +Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n). Proof. - split; [apply Z_of_N_gt | apply Z_of_N_gt_rev]. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n. +Lemma N_of_double_plus_one : + forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). Proof. - destruct n; simpl; auto. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. +Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n). Proof. - destruct p; simpl; auto. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. +Lemma N_of_pred : forall n, N_of_nat (pred n) = Npred (N_of_nat n). Proof. - destruct z; simpl; auto. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z. +Lemma N_of_plus : + forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). Proof. - destruct n; intro; discriminate. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z. +Lemma N_of_minus : + forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n'). Proof. - destruct n; destruct m; auto. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z. +Lemma N_of_mult : + forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). Proof. - destruct n; destruct m; auto. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). +Lemma N_of_div2 : + forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Lemma N_of_nat_compare : + forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). Proof. - intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S. + intros. rewrite nat_of_Ncompare. now autorewrite with Nnat. Qed. -Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Lemma N_of_min : + forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. -Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). +Lemma N_of_max : + forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max. + intros. apply nat_of_N_inj. now autorewrite with Nnat. Qed. - diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 6bb9c2ac4..e944750d8 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -1274,7 +1274,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. apply Qred_complete; apply spec_power_pos; auto. induction p using Pind. simpl; ring. - rewrite nat_of_P_succ_morphism; simpl Qcpower. + rewrite Psucc_S; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. apply Qc_decomp; intros _ _; unfold this. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index c42f9cceb..cb6030e26 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -11,8 +11,7 @@ Unset Boxed Definitions. Declare ML Module "z_syntax_plugin". -(**********************************************************************) -(** Binary positive numbers *) +(** * Binary positive numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) @@ -42,13 +41,16 @@ Notation "p ~ 1" := (xI p) Notation "p ~ 0" := (xO p) (at level 7, left associativity, format "p '~' '0'") : positive_scope. -Open Local Scope positive_scope. +Local Open Scope positive_scope. (* In the current file, [xH] cannot yet be written as [1], since the interpretation of positive numerical constants is not available yet. We fix this here with an ad-hoc temporary notation. *) -Notation Local "1" := xH (at level 7). +Local Notation "1" := xH (at level 7). + + +(** * Operations over positive numbers *) (** Successor *) @@ -224,6 +226,24 @@ Fixpoint Pmult (x y:positive) : positive := Infix "*" := Pmult : positive_scope. +(** Iteration over a positive number *) + +Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := + match n with + | xH => f x + | xO n' => iter_pos n' A f (iter_pos n' A f x) + | xI n' => f (iter_pos n' A f (iter_pos n' A f x)) + end. + +(** Power *) + +Definition Ppow (x y:positive) := iter_pos y _ (Pmult x) 1. + +(** Another possible definition is : Piter_op Pmult y x + but for some reason, this is quite slower on powers of two. *) + +Infix "^" := Ppow : positive_scope. + (** Division by 2 rounded below but for 1 *) Definition Pdiv2 (z:positive) := @@ -235,6 +255,24 @@ Definition Pdiv2 (z:positive) := Infix "/" := Pdiv2 : positive_scope. +(** Number of digits in a positive number *) + +Fixpoint Psize (p:positive) : nat := + match p with + | 1 => S O + | p~1 => S (Psize p) + | p~0 => S (Psize p) + end. + +(** Same, with positive output *) + +Fixpoint Psize_pos (p:positive) : positive := + match p with + | 1 => 1 + | p~1 => Psucc (Psize_pos p) + | p~0 => Psucc (Psize_pos p) + end. + (** Comparison on binary positive numbers *) Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := @@ -278,7 +316,6 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with | Gt => p end. -(********************************************************************) (** Boolean equality *) Fixpoint Peqb (x y : positive) {struct y} : bool := @@ -289,7 +326,9 @@ Fixpoint Peqb (x y : positive) {struct y} : bool := | _, _ => false end. -(**********************************************************************) + +(** * Properties of operations over positive numbers *) + (** Decidability of equality on binary positive numbers *) Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. @@ -759,6 +798,61 @@ Proof. rewrite Pplus_assoc, Pplus_diag. simpl. now rewrite Pplus_comm. Qed. +(** Properties of [iter_pos] *) + +Lemma iter_pos_swap_gen : forall A B (f:A->B)(g:A->A)(h:B->B), + (forall a, f (g a) = h (f a)) -> forall p a, + f (iter_pos p A g a) = iter_pos p B h (f a). +Proof. + induction p; simpl; intros; now rewrite ?H, ?IHp. +Qed. + +Theorem iter_pos_swap : + forall p (A:Type) (f:A -> A) (x:A), + iter_pos p A f (f x) = f (iter_pos p A f x). +Proof. + intros. symmetry. now apply iter_pos_swap_gen. +Qed. + +Theorem iter_pos_succ : + forall p (A:Type) (f:A -> A) (x:A), + iter_pos (Psucc p) A f x = f (iter_pos p A f x). +Proof. + induction p as [p IHp|p IHp|]; intros; simpl; trivial. + now rewrite !IHp, iter_pos_swap. +Qed. + +Theorem iter_pos_plus : + forall p q (A:Type) (f:A -> A) (x:A), + iter_pos (p+q) A f x = iter_pos p A f (iter_pos q A f x). +Proof. + induction p using Pind; intros. + now rewrite <- Pplus_one_succ_l, iter_pos_succ. + now rewrite Pplus_succ_permute_l, !iter_pos_succ, IHp. +Qed. + +Theorem iter_pos_invariant : + forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop), + (forall x:A, Inv x -> Inv (f x)) -> + forall x:A, Inv x -> Inv (iter_pos p A f x). +Proof. + induction p as [p IHp|p IHp|]; simpl; trivial. + intros A f Inv H x H0. apply H, IHp, IHp; trivial. + intros A f Inv H x H0. apply IHp, IHp; trivial. +Qed. + +(** Properties of power *) + +Lemma Ppow_1_r : forall p, p^1 = p. +Proof. + intros p. unfold Ppow. simpl. now rewrite Pmult_comm. +Qed. + +Lemma Ppow_succ_r : forall p q, p^(Psucc q) = p * p^q. +Proof. + intros. unfold Ppow. now rewrite iter_pos_succ. +Qed. + (*********************************************************************) (** Properties of boolean equality *) @@ -924,7 +1018,6 @@ Proof. apply ZC1; auto. Qed. - (** Comparison and the successor *) Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt. @@ -958,6 +1051,29 @@ Proof. destruct (Pcompare_Lt_eq_Lt p q); auto. Qed. +Lemma Pcompare_succ_succ : + forall n m, (Psucc n ?= Psucc m) Eq = (n ?= m) Eq. +Proof. + assert (AUX : forall n m, (Psucc n ?= Psucc m) Eq = (n ?= m) Eq -> + (Psucc n ?= m) Lt = (n ?= m) Gt). + intros n m IH. + case_eq ((n ?= m) Gt); intros H. + elim (proj1 (Pcompare_not_Eq n m) H). + apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq. rewrite IH. + now apply Pcompare_Gt_Lt. + apply Pcompare_eq_Gt, ZC2, Pcompare_p_Sq. apply Pcompare_Gt_Gt in H. + destruct H; [left; now apply ZC1|now right]. + (* main *) + induction n; destruct m; simpl; trivial. + now apply AUX. + generalize (Psucc_not_one n); destruct (Psucc n); intuition. + change Gt with (CompOpp Lt); rewrite <- Pcompare_antisym. + rewrite AUX, Pcompare_antisym; trivial. now rewrite ZC4, IHn, <- ZC4. + now destruct n. + apply Pcompare_p_Sq; destruct m; auto. + now destruct m. +Qed. + (** 1 is the least positive number *) Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt. @@ -965,7 +1081,7 @@ Proof. destruct p; discriminate. Qed. -(** Properties of the strict order on positive numbers *) +(** Properties of the order on positive numbers *) Lemma Plt_1 : forall p, ~ p < 1. Proof. @@ -984,15 +1100,12 @@ Qed. Lemma Psucc_lt_compat : forall n m, n < m <-> Psucc n < Psucc m. Proof. - unfold Plt. induction n; destruct m; simpl; auto; split; try easy; intros. - now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, IHn, Pcompare_Gt_Lt. - now apply Pcompare_eq_Lt, IHn, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. - destruct (Psucc n); discriminate. - now apply Pcompare_eq_Lt, Pcompare_p_Sq, Pcompare_Lt_eq_Lt. - now apply Pcompare_Lt_eq_Lt, Pcompare_p_Sq, Pcompare_Gt_Lt. - destruct n; discriminate. - apply Plt_1_succ. - destruct m; auto. + unfold Plt. intros. rewrite Pcompare_succ_succ. apply iff_refl. +Qed. + +Lemma Psucc_le_compat : forall n m, n <= m <-> Psucc n <= Psucc m. +Proof. + unfold Ple. intros. rewrite Pcompare_succ_succ. apply iff_refl. Qed. Lemma Plt_irrefl : forall p : positive, ~ p < p. @@ -1025,52 +1138,149 @@ Proof. destruct ((p ?= q) Eq); intuition; discriminate. Qed. -Lemma Ple_refl : forall p, Ple p p. +Lemma Ple_refl : forall p, p <= p. Proof. intros. unfold Ple. rewrite Pcompare_refl_id. discriminate. Qed. -(** Strict order and operations *) +Lemma Ple_lt_trans : forall n m p, n <= m -> m < p -> n < p. +Proof. + intros n m p H H'. + apply Ple_lteq in H. destruct H. + now apply Plt_trans with m. now subst. +Qed. + +Lemma Plt_le_trans : forall n m p, n < m -> m <= p -> n < p. +Proof. + intros n m p H H'. + apply Ple_lteq in H'. destruct H'. + now apply Plt_trans with m. now subst. +Qed. + +Lemma Ple_trans : forall n m p, n <= m -> m <= p -> n <= p. +Proof. + intros n m p H H'. + apply Ple_lteq in H. destruct H. + apply Ple_lteq; left. now apply Plt_le_trans with m. + now subst. +Qed. + +Lemma Plt_succ_r : forall p q, p < Psucc q <-> p <= q. +Proof. + intros. eapply iff_trans; [eapply Pcompare_p_Sq|eapply iff_sym, Ple_lteq]. +Qed. + +Lemma Ple_succ_l : forall n m, Psucc n <= m <-> n < m. +Proof. + intros. apply iff_sym. + eapply iff_trans; [eapply Psucc_lt_compat|eapply Plt_succ_r]. +Qed. + +(** Comparison and addition *) + +Lemma Pplus_compare_mono_l : forall p q r, (p+q ?= p+r) Eq = (q ?= r) Eq. +Proof. + induction p using Pind; intros q r. + rewrite <- 2 Pplus_one_succ_l. apply Pcompare_succ_succ. + now rewrite 2 Pplus_succ_permute_l, Pcompare_succ_succ. +Qed. + +Lemma Pplus_compare_mono_r : forall p q r, (q+p ?= r+p) Eq = (q ?= r) Eq. +Proof. + intros. rewrite 2 (Pplus_comm _ p). apply Pplus_compare_mono_l. +Qed. + +(** Order and addition *) Lemma Pplus_lt_mono_l : forall p q r, q<r <-> p+q < p+r. Proof. - induction p using Prect. - intros q r. rewrite <- 2 Pplus_one_succ_l. apply Psucc_lt_compat. - intros q r. rewrite 2 Pplus_succ_permute_l. - eapply iff_trans; [ eapply IHp | eapply Psucc_lt_compat ]. + intros. unfold Plt. rewrite Pplus_compare_mono_l. apply iff_refl. +Qed. + +Lemma Pplus_lt_mono_r : forall p q r, q<r <-> q+p < r+p. +Proof. + intros. unfold Plt. rewrite Pplus_compare_mono_r. apply iff_refl. Qed. Lemma Pplus_lt_mono : forall p q r s, p<q -> r<s -> p+r<q+s. Proof. intros. apply Plt_trans with (p+s). now apply Pplus_lt_mono_l. - rewrite (Pplus_comm p), (Pplus_comm q). now apply Pplus_lt_mono_l. + now apply Pplus_lt_mono_r. +Qed. + +Lemma Pplus_le_mono_l : forall p q r, q<=r <-> p+q<=p+r. +Proof. + intros. unfold Ple. rewrite Pplus_compare_mono_l. apply iff_refl. +Qed. + +Lemma Pplus_le_mono_r : forall p q r, q<=r <-> q+p<=r+p. +Proof. + intros. unfold Ple. rewrite Pplus_compare_mono_r. apply iff_refl. +Qed. + +Lemma Pplus_le_mono : forall p q r s, p<=q -> r<=s -> p+r <= q+s. +Proof. + intros. apply Ple_trans with (p+s). + now apply Pplus_le_mono_l. + now apply Pplus_le_mono_r. +Qed. + +(** Comparison and multiplication *) + +Lemma Pmult_compare_mono_l : forall p q r, (p*q ?= p*r) Eq = (q ?= r) Eq. +Proof. + induction p; simpl; trivial. intros q r. specialize (IHp q r). + case_eq ((q ?= r) Eq); intros H; rewrite H in IHp. + apply Pcompare_Eq_eq in H. subst. apply Pcompare_refl. + now apply Pplus_lt_mono. + apply ZC2, Pplus_lt_mono; now apply ZC1. +Qed. + +Lemma Pmult_compare_mono_r : forall p q r, (q*p ?= r*p) Eq = (q ?= r) Eq. +Proof. + intros. rewrite 2 (Pmult_comm _ p). apply Pmult_compare_mono_l. Qed. +(** Order and multiplication *) + Lemma Pmult_lt_mono_l : forall p q r, q<r <-> p*q < p*r. Proof. - assert (IMPL : forall p q r, q<r -> p*q < p*r). - induction p using Prect; auto. - intros q r H. rewrite 2 Pmult_Sn_m. - apply Pplus_lt_mono; auto. - split; auto. - intros H. - destruct (Pcompare_spec q r) as [EQ|LT|GT]; trivial. - rewrite EQ in H. elim (Plt_irrefl _ H). - apply (IMPL p) in GT. - elim (Plt_irrefl (p*q)). eapply Plt_trans; eauto. + intros. unfold Plt. rewrite Pmult_compare_mono_l. apply iff_refl. +Qed. + +Lemma Pmult_lt_mono_r : forall p q r, q<r <-> q*p < r*p. +Proof. + intros. unfold Plt. rewrite Pmult_compare_mono_r. apply iff_refl. Qed. Lemma Pmult_lt_mono : forall p q r s, p<q -> r<s -> p*r < q*s. Proof. intros. apply Plt_trans with (p*s). now apply Pmult_lt_mono_l. - rewrite (Pmult_comm p), (Pmult_comm q). now apply Pmult_lt_mono_l. + now apply Pmult_lt_mono_r. +Qed. + +Lemma Pmult_le_mono_l : forall p q r, q<=r <-> p*q<=p*r. +Proof. + intros. unfold Ple. rewrite Pmult_compare_mono_l. apply iff_refl. +Qed. + +Lemma Pmult_le_mono_r : forall p q r, q<=r <-> q*p<=r*p. +Proof. + intros. unfold Ple. rewrite Pmult_compare_mono_r. apply iff_refl. +Qed. + +Lemma Pmult_le_mono : forall p q r s, p<=q -> r<=s -> p*r <= q*s. +Proof. + intros. apply Ple_trans with (p*s). + now apply Pmult_le_mono_l. + now apply Pmult_le_mono_r. Qed. Lemma Plt_plus_r : forall p q, p < p+q. Proof. - induction q using Prect. + induction q using Pind. rewrite <- Pplus_one_succ_r. apply Pcompare_p_Sp. apply Plt_trans with (p+q); auto. apply Pplus_lt_mono_l, Pcompare_p_Sp. @@ -1217,18 +1427,23 @@ Proof. Qed. Theorem Pplus_minus : - forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. + forall p q:positive, (p ?= q) Eq = Gt -> q+(p-q) = p. Proof. intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _). unfold Pminus; rewrite U; simpl; auto. Qed. +Theorem Pplus_minus_lt : forall p q, q<p -> q+(p-q) = p. +Proof. + intros p q H. apply Pplus_minus. apply ZC2, H. +Qed. + Lemma Pplus_minus_eq : forall p q, p+q-q = p. Proof. intros. apply Pplus_reg_l with q. - rewrite Pplus_minus. + rewrite Pplus_minus_lt. apply Pplus_comm. - now rewrite ZC4, Pplus_comm, Plt_plus_r. + rewrite Pplus_comm. apply Plt_plus_r. Qed. Lemma Pmult_minus_distr_l : forall p q r, r<q -> p*(q-r) = p*q-p*r. @@ -1236,21 +1451,52 @@ Proof. intros p q r H. apply Pplus_reg_l with (p*r). rewrite <- Pmult_plus_distr_l. - rewrite Pplus_minus. - symmetry. apply Pplus_minus. - apply (Pmult_lt_mono_l p) in H. - now rewrite ZC4, H. - now rewrite ZC4, H. + rewrite Pplus_minus_lt; trivial. + symmetry. apply Pplus_minus_lt; trivial. + now apply Pmult_lt_mono_l. +Qed. + +Lemma Pminus_lt_mono_l : + forall p q r, q<p -> p<r -> r-p < r-q. +Proof. + intros p q r Hqp Hpr. + apply (Pplus_lt_mono_l p). + rewrite Pplus_minus_lt by trivial. + apply Ple_lt_trans with (q+(r-q)). + rewrite Pplus_minus_lt by (now apply Plt_trans with p). + apply Ple_refl. + now apply Pplus_lt_mono_r. +Qed. + +Lemma Pminus_compare_mono_l : + forall p q r, q<p -> r<p -> (p-q ?= p-r) Eq = (r ?= q) Eq. +Proof. + intros p q r Hqp Hrp. + case (Pcompare_spec r q); intros H. subst. apply Pcompare_refl. + apply Pminus_lt_mono_l; trivial. + apply ZC2, Pminus_lt_mono_l; trivial. +Qed. + +Lemma Pminus_compare_mono_r : + forall p q r, p<q -> p<r -> (q-p ?= r-p) Eq = (q ?= r) Eq. +Proof. + intros. + rewrite <- (Pplus_compare_mono_l p), 2 Pplus_minus_lt; trivial. +Qed. + +Lemma Pminus_lt_mono_r : + forall p q r, q<p -> r<q -> q-r < p-r. +Proof. + intros. unfold Plt. rewrite Pminus_compare_mono_r; trivial. + now apply Plt_trans with q. Qed. Lemma Pminus_decr : forall n m, m<n -> n-m < n. Proof. intros n m LT. apply Pplus_lt_mono_l with m. - rewrite Pplus_minus. - rewrite Pplus_comm. - apply Plt_plus_r. - now rewrite ZC4, LT. + rewrite Pplus_minus_lt; trivial. + rewrite Pplus_comm. apply Plt_plus_r. Qed. Lemma Pminus_xI_xI : forall n m, m<n -> n~1 - m~1 = (n-m)~0. @@ -1260,6 +1506,34 @@ Proof. now rewrite ZC4, H. Qed. +Lemma Pplus_minus_assoc : forall p q r, r<q -> p+(q-r) = p+q-r. +Proof. + intros p q r H. + apply Pplus_reg_l with r. + rewrite Pplus_assoc, (Pplus_comm r), <- Pplus_assoc. + rewrite !Pplus_minus_lt; trivial. + rewrite Pplus_comm. apply Plt_trans with q; trivial using Plt_plus_r. +Qed. + +Lemma Pminus_plus_distr : forall p q r, q+r < p -> p-(q+r) = p-q-r. +Proof. + intros p q r H. + assert (q < p) + by (apply Plt_trans with (q+r); trivial using Plt_plus_r). + apply Pplus_reg_l with (q+r). + rewrite Pplus_minus_lt, <- Pplus_assoc, !Pplus_minus_lt; trivial. + apply (Pplus_lt_mono_l q). rewrite Pplus_minus_lt; trivial. +Qed. + +Lemma Pminus_minus_distr : forall p q r, r<q -> q-r < p -> p-(q-r) = p+r-q. +Proof. + intros p q r H H'. + apply Pplus_reg_l with (r+(q-r)). + rewrite <- Pplus_assoc, !Pplus_minus_lt; trivial using Pplus_comm. + rewrite Pplus_comm, <- (Pplus_minus_lt q r); trivial. + now apply Pplus_lt_mono_l. +Qed. + (** When x<y, the substraction of x by y returns 1 *) Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg. @@ -1284,14 +1558,7 @@ Proof. intros; unfold Pminus; rewrite Pminus_mask_diag; auto. Qed. -(** Number of digits in a number *) - -Fixpoint Psize (p:positive) : nat := - match p with - | 1 => S O - | p~1 => S (Psize p) - | p~0 => S (Psize p) - end. +(** Results concerning [Psize] and [Psize_pos] *) Lemma Psize_monotone : forall p q, p<q -> (Psize p <= Psize q)%nat. Proof. @@ -1301,3 +1568,18 @@ Proof. intros; generalize (Pcompare_Gt_Lt _ _ H); auto. intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto. Qed. + +Local Notation "2" := (1~0) : positive_scope. + +Lemma Psize_pos_gt : forall p, p < 2^(Psize_pos p). +Proof. + induction p; simpl; try rewrite Ppow_succ_r; try easy. + apply Ple_succ_l in IHp. now apply Ple_succ_l. +Qed. + +Lemma Psize_pos_le : forall p, 2^(Psize_pos p) <= p~0. +Proof. + induction p; simpl; try rewrite Ppow_succ_r; try easy. + apply Pmult_le_mono_l. + apply Ple_lteq; left. rewrite xI_succ_xO. apply Plt_succ_r, IHp. +Qed. diff --git a/theories/PArith/Pminmax.v b/theories/PArith/Pminmax.v index 2f753a4c9..6fe6435a0 100644 --- a/theories/PArith/Pminmax.v +++ b/theories/PArith/Pminmax.v @@ -83,7 +83,7 @@ Lemma succ_max_distr : Proof. intros. symmetry. apply max_monotone. intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + rewrite 2 Pcompare_nat_compare, 2 Psucc_S. simpl; auto. Qed. @@ -91,7 +91,7 @@ Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). Proof. intros. symmetry. apply min_monotone. intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. + rewrite 2 Pcompare_nat_compare, 2 Psucc_S. simpl; auto. Qed. @@ -99,7 +99,7 @@ Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. Proof. intros. apply max_monotone. intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite 2 Pcompare_nat_compare, 2 Pplus_plus. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. @@ -113,7 +113,7 @@ Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. Proof. intros. apply min_monotone. intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. + rewrite 2 Pcompare_nat_compare, 2 Pplus_plus. rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. Qed. diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index b3f2493b2..590217d5d 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -7,332 +7,199 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos. +Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec Wf_nat. -(**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano - natural numbers *) +(** Properties of the injection from binary positive numbers + to Peano natural numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) -Require Import Le. -Require Import Lt. -Require Import Gt. -Require Import Plus. -Require Import Mult. -Require Import Minus. -Require Import Compare_dec. - Local Open Scope positive_scope. Local Open Scope nat_scope. -(** [nat_of_P] is a morphism for addition *) - -Lemma Pmult_nat_succ_morphism : - forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n. -Proof. -intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m; - rewrite IHp; rewrite plus_assoc; trivial. -Qed. +(** [Pmult_nat] in term of [nat_of_P] *) -Lemma nat_of_P_succ_morphism : - forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p). +Lemma Pmult_nat_mult : forall p n, + Pmult_nat p n = nat_of_P p * n. Proof. - intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *; - unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism. + induction p; intros n. + unfold nat_of_P. simpl. f_equal. rewrite 2 IHp. + rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O. + unfold nat_of_P. simpl. rewrite 2 IHp. + rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O. + simpl. now rewrite <- plus_n_O. Qed. -Theorem Pmult_nat_plus_carry_morphism : - forall (p q:positive) (n:nat), - Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n. -Proof. -intro x; induction x as [p IHp| p IHp| ]; intro y; - [ destruct y as [p0| p0| ] - | destruct y as [p0| p0| ] - | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; - intro m; - [ rewrite IHp; rewrite plus_assoc; trivial with arith - | rewrite IHp; rewrite plus_assoc; trivial with arith - | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith - | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. -Qed. +(** [nat_of_P] is a morphism for successor, addition, multiplication *) -Theorem nat_of_P_plus_carry_morphism : - forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)). +Lemma Psucc_S : forall p, nat_of_P (Psucc p) = S (nat_of_P p). Proof. -intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism; - simpl in |- *; trivial with arith. + induction p; unfold nat_of_P; simpl; trivial. + now rewrite !Pmult_nat_mult, IHp. Qed. -Theorem Pmult_nat_l_plus_morphism : - forall (p q:positive) (n:nat), - Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n. +Theorem Pplus_plus : + forall p q, nat_of_P (p + q) = nat_of_P p + nat_of_P q. Proof. -intro x; induction x as [p IHp| p IHp| ]; intro y; - [ destruct y as [p0| p0| ] - | destruct y as [p0| p0| ] - | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; - [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp; - rewrite plus_assoc_reverse; rewrite plus_assoc_reverse; - rewrite (plus_permute m (Pmult_nat p (m + m))); - trivial with arith - | intros m; rewrite IHp; apply plus_assoc - | intros m; rewrite Pmult_nat_succ_morphism; - rewrite (plus_comm (m + Pmult_nat p (m + m))); - apply plus_assoc_reverse - | intros m; rewrite IHp; apply plus_permute - | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. + induction p using Pind; intros q. + now rewrite <- Pplus_one_succ_l, Psucc_S. + now rewrite Pplus_succ_permute_l, !Psucc_S, IHp. Qed. -Theorem nat_of_P_plus_morphism : - forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q. +Theorem Pmult_mult : + forall p q, nat_of_P (p * q) = nat_of_P p * nat_of_P q. Proof. -intros x y; exact (Pmult_nat_l_plus_morphism x y 1). + induction p using Pind; simpl; intros; trivial. + now rewrite Pmult_Sn_m, Pplus_plus, IHp, Psucc_S. Qed. -(** [Pmult_nat] is a morphism for addition *) +(** Mapping of xH, xO and xI through [nat_of_P] *) -Lemma Pmult_nat_r_plus_morphism : - forall (p:positive) (n:nat), - Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. +Lemma nat_of_P_xH : nat_of_P 1 = 1. Proof. -intro y; induction y as [p H| p H| ]; intro m; - [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse; - rewrite (plus_permute m (Pmult_nat p (m + m))); - rewrite plus_assoc_reverse; auto with arith - | simpl in |- *; rewrite H; auto with arith - | simpl in |- *; trivial with arith ]. + reflexivity. Qed. -Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p. +Lemma nat_of_P_xO : forall p, nat_of_P (xO p) = 2 * nat_of_P p. Proof. -intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism; - trivial. + intros. exact (Pmult_mult 2 p). Qed. -(** [nat_of_P] is a morphism for multiplication *) - -Theorem nat_of_P_mult_morphism : - forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q. +Lemma nat_of_P_xI : forall p, nat_of_P (xI p) = S (2 * nat_of_P p). Proof. -intros x y; induction x as [x' H| x' H| ]; - [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *; - rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *; - simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r; - reflexivity - | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H; - rewrite mult_plus_distr_r; reflexivity - | simpl in |- *; rewrite <- plus_n_O; reflexivity ]. + intros. now rewrite xI_succ_xO, Psucc_S, nat_of_P_xO. Qed. (** [nat_of_P] maps to the strictly positive subset of [nat] *) -Lemma ZL4 : forall p:positive, exists h : nat, nat_of_P p = S h. +Lemma nat_of_P_is_S : forall p, exists n, nat_of_P p = S n. Proof. -intro y; induction y as [p H| p H| ]; - [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; - simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; - rewrite H1; auto with arith - | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *; - simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; - rewrite H2; auto with arith - | exists 0; auto with arith ]. +induction p as [p (h,IH)| p (h,IH)| ]; unfold nat_of_P; simpl. + exists (S h * 2). now rewrite Pmult_nat_mult, IH. + exists (S (h*2)). now rewrite Pmult_nat_mult,IH. + now exists 0. Qed. -(** Extra lemmas on [lt] on Peano natural numbers *) - -Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m. -Proof. -intros m n H; apply lt_trans with (m := m + n); - [ apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. -Qed. +(** [nat_of_P] is strictly positive *) -Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. +Lemma nat_of_P_pos : forall p, 0 < nat_of_P p. Proof. -intros m n H; apply le_lt_trans with (m := m + n); - [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. + intros p. destruct (nat_of_P_is_S p) as (n,->). auto with arith. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) +(** [nat_of_P] is a morphism for comparison *) - Part 1: [lt] on [positive] is finer than [lt] on [nat] -*) - -Lemma nat_of_P_lt_Lt_compare_morphism : - forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q. +Lemma Pcompare_nat_compare : forall p q, + (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q). Proof. -intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; - intro H2; - [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6; - apply ZL7; apply H; simpl in H2; assumption - | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8; - apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption - | simpl in |- *; discriminate H2 - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - elim (Pcompare_Lt_Lt p q H2); - [ intros H3; apply lt_S; apply ZL7; apply H; apply H3 - | intros E; rewrite E; apply lt_n_Sn ] - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - apply ZL7; apply H; assumption - | simpl in |- *; discriminate H2 - | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6; - elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; - apply lt_O_Sn - | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q); - intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; - apply lt_n_S; apply lt_O_Sn - | simpl in |- *; discriminate H2 ]. + induction p as [ |p IH] using Pind; intros q. + destruct (Psucc_pred q) as [Hq|Hq]; [now subst|]. + rewrite <- Hq, Plt_1_succ, Psucc_S, nat_of_P_xH, nat_compare_S. + symmetry. apply nat_compare_lt, nat_of_P_pos. + destruct (Psucc_pred q) as [Hq|Hq]; [subst|]. + rewrite ZC4, Plt_1_succ, Psucc_S. simpl. + symmetry. apply nat_compare_gt, nat_of_P_pos. + now rewrite <- Hq, 2 Psucc_S, Pcompare_succ_succ, IH. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) +(** [nat_of_P] is hence injective *) - Part 1: [gt] on [positive] is finer than [gt] on [nat] -*) - -Lemma nat_of_P_gt_Gt_compare_morphism : - forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q. +Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q. Proof. -intros p q GT. unfold gt. -apply nat_of_P_lt_Lt_compare_morphism. -change ((q ?= p) (CompOpp Eq) = CompOpp Gt). -rewrite <- Pcompare_antisym, GT; auto. + intros. + eapply iff_trans; [eapply iff_sym|eapply Pcompare_eq_iff]. + rewrite Pcompare_nat_compare. + apply nat_compare_eq_iff. Qed. -(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *) - -Lemma nat_of_P_compare_morphism : forall p q, - (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q). +Lemma nat_of_P_inj : forall p q, nat_of_P p = nat_of_P q -> p = q. Proof. - intros p q; symmetry. - destruct ((p ?= q) Eq) as [ | | ]_eqn. - rewrite (Pcompare_Eq_eq p q); auto. - apply <- nat_compare_eq_iff; auto. - apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto. - apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto. + intros. now apply nat_of_P_inj_iff. Qed. -(** [nat_of_P] is hence injective. *) +(** [nat_of_P] is a morphism for [lt], [le], etc *) -Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. +Lemma Plt_lt : forall p q, Plt p q <-> nat_of_P p < nat_of_P q. Proof. -intros. -apply Pcompare_Eq_eq. -rewrite nat_of_P_compare_morphism. -apply <- nat_compare_eq_iff; auto. + intros. unfold Plt. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_lt. Qed. -(** Stating this bidirectionally lets us reason equationally with it: *) - -Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q. +Lemma Ple_le : forall p q, Ple p q <-> nat_of_P p <= nat_of_P q. Proof. - split; intro. now apply nat_of_P_inj. now subst. + intros. unfold Ple. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_le. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 2: [lt] on [nat] is finer than [lt] on [positive] -*) - -Lemma nat_of_P_lt_Lt_compare_complement_morphism : - forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt. +Lemma Pgt_gt : forall p q, Pgt p q <-> nat_of_P p > nat_of_P q. Proof. - intros. rewrite nat_of_P_compare_morphism. - apply -> nat_compare_lt; auto. + intros. unfold Pgt. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_gt. Qed. -(** Again, stating this bidirectionally lets us reason equationally with it: *) - -Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q). +Lemma Pge_ge : forall p q, Pge p q <-> nat_of_P p >= nat_of_P q. Proof. - intros. unfold Plt. rewrite nat_of_P_compare_morphism. - apply iff_sym, nat_compare_lt. + intros. unfold Pge. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_ge. Qed. -(** And the same for Ple *) +(** [nat_of_P] is a morphism for subtraction *) -Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q). +Theorem Pminus_minus : + forall p q, Plt q p -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. Proof. - intros. unfold Ple. rewrite nat_of_P_compare_morphism. - apply iff_sym, nat_compare_le. + intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r. + rewrite <- Pplus_plus, Pplus_minus. trivial. now apply ZC2. + now apply lt_le_weak, Plt_lt. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 2: [gt] on [nat] is finer than [gt] on [positive] -*) +(** Results about [Pmult_nat], many are old intermediate results *) -Lemma nat_of_P_gt_Gt_compare_complement_morphism : - forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt. +Lemma Pmult_nat_succ_morphism : + forall p n, Pmult_nat (Psucc p) n = n + Pmult_nat p n. Proof. - intros. rewrite nat_of_P_compare_morphism. - apply -> nat_compare_gt; auto. -Qed. - - -(** [nat_of_P] is strictly positive *) - -Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n. -induction p; simpl in |- *; auto with arith. -intro m; apply le_trans with (m + m); auto with arith. -Qed. - -Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p. -intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith. -apply le_Pmult_nat. + intros. now rewrite !Pmult_nat_mult, Psucc_S. Qed. -(** Pmult_nat permutes with multiplication *) - -Lemma Pmult_nat_mult_permute : - forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n. +Theorem Pmult_nat_l_plus_morphism : + forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n. Proof. - simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n). - rewrite (H (n + n) m). reflexivity. - intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H. - trivial. + intros. rewrite !Pmult_nat_mult, Pplus_plus. apply mult_plus_distr_r. Qed. -Lemma Pmult_nat_2_mult_2_permute : - forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. +Theorem Pmult_nat_plus_carry_morphism : + forall p q n, Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n. Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. + intros. now rewrite Pplus_carry_spec, Pmult_nat_succ_morphism. Qed. -Lemma Pmult_nat_4_mult_2_permute : - forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. +Lemma Pmult_nat_r_plus_morphism : + forall p n, Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. + intros. rewrite !Pmult_nat_mult. apply mult_plus_distr_l. Qed. -(** Mapping of xH, xO and xI through [nat_of_P] *) - -Lemma nat_of_P_xH : nat_of_P 1 = 1. +Lemma ZL6 : forall p, Pmult_nat p 2 = nat_of_P p + nat_of_P p. Proof. - reflexivity. + intros. rewrite Pmult_nat_mult, mult_comm. simpl. now rewrite <- plus_n_O. Qed. -Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. +Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n. Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism. - f_equal. + intros. rewrite Pmult_nat_mult. + apply le_trans with (1*n). now rewrite mult_1_l. + apply mult_le_compat_r. apply nat_of_P_pos. Qed. -Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p). +(** [nat_of_P] is a morphism for [iter_pos] and [iter_nat] *) + +Theorem iter_nat_of_P : + forall p (A:Type) (f:A->A) (x:A), + iter_pos p A f x = iter_nat (nat_of_P p) A f x. Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism. - f_equal. + induction p as [p IH|p IH| ]; intros A f x; simpl; trivial. + f_equal. now rewrite 2 IH, <- iter_nat_plus, <- ZL6. + now rewrite 2 IH, <- iter_nat_plus, <- ZL6. Qed. (**********************************************************************) @@ -341,143 +208,63 @@ Qed. (** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) -Theorem nat_of_P_o_P_of_succ_nat_eq_succ : - forall n:nat, nat_of_P (P_of_succ_nat n) = S n. -Proof. -induction n as [|n H]. -reflexivity. -simpl; rewrite nat_of_P_succ_morphism, H; auto. -Qed. - -(** Miscellaneous lemmas on [P_of_succ_nat] *) - -Lemma ZL3 : - forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). +Theorem nat_of_P_of_succ_nat : + forall n, nat_of_P (P_of_succ_nat n) = S n. Proof. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite plus_comm; simpl; rewrite H; - rewrite xO_succ_permute; auto with arith ]. -Qed. - -Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n). -Proof. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; - auto with arith ]. +induction n as [|n H]; trivial; simpl; now rewrite Psucc_S, H. Qed. (** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) -Theorem P_of_succ_nat_o_nat_of_P_eq_succ : - forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p. +Theorem P_of_succ_nat_of_P : + forall p, P_of_succ_nat (nat_of_P p) = Psucc p. Proof. intros. -apply nat_of_P_inj. -rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto. +apply nat_of_P_inj. now rewrite nat_of_P_of_succ_nat, Psucc_S. Qed. (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity on [positive] *) -Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id : - forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p. +Theorem Ppred_of_succ_nat_of_P : + forall p, Ppred (P_of_succ_nat (nat_of_P p)) = p. Proof. -intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto. +intros; rewrite P_of_succ_nat_of_P, Ppred_succ; auto. Qed. (**********************************************************************) -(** Extra properties of the injection from binary positive numbers to Peano - natural numbers *) - -(** [nat_of_P] is a morphism for subtraction on positive numbers *) - -Theorem nat_of_P_minus_morphism : - forall p q:positive, - (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. -Proof. -intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r; - [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith - | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ]. -Qed. - - -Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p. -Proof. -intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1; - rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; - apply le_minus. -Qed. - -Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q). -Proof. -intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q); - intros k H; rewrite H; rewrite plus_comm; simpl in |- *; - apply le_n_S; apply le_plus_r. -Qed. - -(** Comparison and subtraction *) - -Lemma Pcompare_minus_r : - forall p q r:positive, - (q ?= p) Eq = Lt -> - (r ?= p) Eq = Gt -> - (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt. -Proof. -intros; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r; - [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); - rewrite plus_assoc; rewrite le_plus_minus_r; - [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; - assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -Lemma Pcompare_minus_l : - forall p q r:positive, - (q ?= p) Eq = Lt -> - (p ?= r) Eq = Gt -> - (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt. -Proof. -intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); - rewrite le_plus_minus_r; - [ rewrite le_plus_minus_r; - [ apply nat_of_P_lt_Lt_compare_morphism; assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -(** Distributivity of multiplication over subtraction *) - -Theorem Pmult_minus_distr_l : - forall p q r:positive, - (q ?= r) Eq = Gt -> - (p * (q - r) = p * q - p * r)%positive. -Proof. -intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ do 2 rewrite nat_of_P_mult_morphism; - do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r - | apply nat_of_P_gt_Gt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; - elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_gt_Gt_compare_morphism y z H) ] - | assumption ]. -Qed. +(** Extra properties of the injection from binary positive numbers + to Peano natural numbers *) + +(** Old names and old-style lemmas *) + +Notation nat_of_P_succ_morphism := Psucc_S (only parsing). +Notation nat_of_P_plus_morphism := Pplus_plus (only parsing). +Notation nat_of_P_mult_morphism := Pmult_mult (only parsing). +Notation nat_of_P_compare_morphism := Pcompare_nat_compare (only parsing). +Notation lt_O_nat_of_P := nat_of_P_pos (only parsing). +Notation ZL4 := nat_of_P_is_S (only parsing). +Notation nat_of_P_o_P_of_succ_nat_eq_succ := nat_of_P_of_succ_nat (only parsing). +Notation P_of_succ_nat_o_nat_of_P_eq_succ := P_of_succ_nat_of_P (only parsing). +Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Ppred_of_succ_nat_of_P + (only parsing). + +Definition nat_of_P_minus_morphism p q : + (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q + := fun H => Pminus_minus p q (ZC1 _ _ H). + +Definition nat_of_P_lt_Lt_compare_morphism p q : + (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q + := proj1 (Plt_lt p q). + +Definition nat_of_P_gt_Gt_compare_morphism p q : + (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q + := proj1 (Pgt_gt p q). + +Definition nat_of_P_lt_Lt_compare_complement_morphism p q : + nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt + := proj2 (Plt_lt p q). + +Definition nat_of_P_gt_Gt_compare_complement_morphism p q : + nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt + := proj2 (Pgt_gt p q). diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 154541164..de41fd3f6 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1601,7 +1601,7 @@ Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p). Proof. intro; apply lt_0_INR. simpl in |- *; auto with real. - apply lt_O_nat_of_P. + apply nat_of_P_pos. Qed. Hint Resolve pos_INR_nat_of_P: real. @@ -1710,38 +1710,31 @@ Qed. Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z_of_nat n). Proof. simple induction n; auto with real. - intros; simpl in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; + intros; simpl in |- *; rewrite nat_of_P_of_succ_nat; auto with real. Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. - intros. - case (lt_eq_lt_dec (nat_of_P p) (nat_of_P q)). - intros [H| H]; simpl in |- *. - rewrite nat_of_P_lt_Lt_compare_complement_morphism; simpl in |- *; trivial. - rewrite (nat_of_P_minus_morphism q p). - rewrite minus_INR; auto with arith; ring. - apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial. - rewrite (nat_of_P_inj p q); trivial. - rewrite Pcompare_refl; simpl in |- *; auto with real. - intro H; simpl in |- *. - rewrite nat_of_P_gt_Gt_compare_complement_morphism; simpl in |- *; - auto with arith. - rewrite (nat_of_P_minus_morphism p q). - rewrite minus_INR; auto with arith; ring. - apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial. + intros p q; simpl. case Pcompare_spec; intros H; simpl. + subst. ring. + rewrite Pminus_minus by trivial. + rewrite minus_INR by (now apply lt_le_weak, Plt_lt). + ring. + rewrite Pminus_minus by trivial. + rewrite minus_INR by (now apply lt_le_weak, Plt_lt). + ring. Qed. (**********) Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m. Proof. intro z; destruct z; intro t; destruct t; intros; auto with real. - simpl in |- *; intros; rewrite nat_of_P_plus_morphism; auto with real. + simpl; intros; rewrite Pplus_plus; auto with real. apply plus_IZR_NEG_POS. rewrite Zplus_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. - simpl in |- *; intros; rewrite nat_of_P_plus_morphism; rewrite plus_INR; + simpl; intros; rewrite Pplus_plus; rewrite plus_INR; auto with real. Qed. @@ -1749,14 +1742,14 @@ Qed. Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m. Proof. intros z t; case z; case t; simpl in |- *; auto with real. - intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real. - intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real. + intros t1 z1; rewrite Pmult_mult; auto with real. + intros t1 z1; rewrite Pmult_mult; auto with real. rewrite Rmult_comm. rewrite Ropp_mult_distr_l_reverse; auto with real. apply Ropp_eq_compat; rewrite mult_comm; auto with real. - intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real. + intros t1 z1; rewrite Pmult_mult; auto with real. rewrite Ropp_mult_distr_l_reverse; auto with real. - intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real. + intros t1 z1; rewrite Pmult_mult; auto with real. rewrite Rmult_opp_opp; auto with real. Qed. @@ -1764,7 +1757,7 @@ Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)). Proof. intros z [|n];simpl;trivial. rewrite Zpower_pos_nat. - rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl. + rewrite nat_of_P_of_succ_nat. unfold Zpower_nat;simpl. rewrite mult_IZR. induction n;simpl;trivial. rewrite mult_IZR;ring[IHn]. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index a2fe4f80f..525eff688 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -34,7 +34,7 @@ Open Local Scope R_scope. (*********) Lemma INR_fact_neq_0 : forall n:nat, INR (fact n) <> 0. Proof. - intro; red in |- *; intro; apply (not_O_INR (fact n) (fact_neq_0 n)); + intro; red; intro; apply (not_O_INR (fact n) (fact_neq_0 n)); assumption. Qed. @@ -49,7 +49,7 @@ Lemma simpl_fact : forall n:nat, / INR (fact (S n)) * / / INR (fact n) = / INR (S n). Proof. intro; rewrite (Rinv_involutive (INR (fact n)) (INR_fact_neq_0 n)); - unfold fact at 1 in |- *; cbv beta iota in |- *; fold fact in |- *; + unfold fact at 1; cbv beta iota; fold fact; rewrite (mult_INR (S n) (fact n)); rewrite (Rinv_mult_distr (INR (S n)) (INR (fact n))). rewrite (Rmult_assoc (/ INR (S n)) (/ INR (fact n)) (INR (fact n))); @@ -73,20 +73,20 @@ Qed. Lemma pow_1 : forall x:R, x ^ 1 = x. Proof. - simpl in |- *; auto with real. + simpl; auto with real. Qed. Lemma pow_add : forall (x:R) (n m:nat), x ^ (n + m) = x ^ n * x ^ m. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros n0 H' m; rewrite H'; auto with real. Qed. Lemma pow_nonzero : forall (x:R) (n:nat), x <> 0 -> x ^ n <> 0. Proof. - intro; simple induction n; simpl in |- *. - intro; red in |- *; intro; apply R1_neq_R0; assumption. - intros; red in |- *; intro; elim (Rmult_integral x (x ^ n0) H1). + intro; simple induction n; simpl. + intro; red; intro; apply R1_neq_R0; assumption. + intros; red; intro; elim (Rmult_integral x (x ^ n0) H1). intro; auto. apply H; assumption. Qed. @@ -96,24 +96,24 @@ Hint Resolve pow_O pow_1 pow_add pow_nonzero: real. Lemma pow_RN_plus : forall (x:R) (n m:nat), x <> 0 -> x ^ n = x ^ (n + m) * / x ^ m. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros n0 H' m H'0. rewrite Rmult_assoc; rewrite <- H'; auto. Qed. Lemma pow_lt : forall (x:R) (n:nat), 0 < x -> 0 < x ^ n. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros n0 H' H'0; replace 0 with (x * 0); auto with real. Qed. Hint Resolve pow_lt: real. Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n. Proof. - intros x n; elim n; simpl in |- *; auto with real. + intros x n; elim n; simpl; auto with real. intros H' H'0; exfalso; omega. intros n0; case n0. - simpl in |- *; rewrite Rmult_1_r; auto. + simpl; rewrite Rmult_1_r; auto. intros n1 H' H'0 H'1. replace 1 with (1 * 1); auto with real. apply Rlt_trans with (r2 := x * 1); auto with real. @@ -127,7 +127,7 @@ Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m. Proof. intros x n m H' H'0; replace m with (m - n + n)%nat. rewrite pow_add. - pattern (x ^ n) at 1 in |- *; replace (x ^ n) with (1 * x ^ n); + pattern (x ^ n) at 1; replace (x ^ n) with (1 * x ^ n); auto with real. apply Rminus_lt. repeat rewrite (fun y:R => Rmult_comm y (x ^ n)); @@ -147,14 +147,14 @@ Hint Resolve Rlt_pow: real. (*********) Lemma tech_pow_Rmult : forall (x:R) (n:nat), x * x ^ n = x ^ S n. Proof. - simple induction n; simpl in |- *; trivial. + simple induction n; simpl; trivial. Qed. (*********) Lemma tech_pow_Rplus : forall (x:R) (a n:nat), x ^ a + INR n * x ^ a = INR (S n) * x ^ a. Proof. - intros; pattern (x ^ a) at 1 in |- *; + intros; pattern (x ^ a) at 1; rewrite <- (let (H1, H2) := Rmult_ne (x ^ a) in H1); rewrite (Rmult_comm (INR n) (x ^ a)); rewrite <- (Rmult_plus_distr_l (x ^ a) 1 (INR n)); @@ -165,29 +165,29 @@ Qed. Lemma poly : forall (n:nat) (x:R), 0 < x -> 1 + INR n * x <= (1 + x) ^ n. Proof. intros; elim n. - simpl in |- *; cut (1 + 0 * x = 1). - intro; rewrite H0; unfold Rle in |- *; right; reflexivity. + simpl; cut (1 + 0 * x = 1). + intro; rewrite H0; unfold Rle; right; reflexivity. ring. - intros; unfold pow in |- *; fold pow in |- *; + intros; unfold pow; fold pow; apply (Rle_trans (1 + INR (S n0) * x) ((1 + x) * (1 + INR n0 * x)) ((1 + x) * (1 + x) ^ n0)). cut ((1 + x) * (1 + INR n0 * x) = 1 + INR (S n0) * x + INR n0 * (x * x)). - intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1 in |- *; + intro; rewrite H1; pattern (1 + INR (S n0) * x) at 1; rewrite <- (let (H1, H2) := Rplus_ne (1 + INR (S n0) * x) in H1); apply Rplus_le_compat_l; elim n0; intros. - simpl in |- *; rewrite Rmult_0_l; unfold Rle in |- *; right; auto. - unfold Rle in |- *; left; generalize Rmult_gt_0_compat; unfold Rgt in |- *; - intro; fold (Rsqr x) in |- *; + simpl; rewrite Rmult_0_l; unfold Rle; right; auto. + unfold Rle; left; generalize Rmult_gt_0_compat; unfold Rgt; + intro; fold (Rsqr x); apply (H3 (INR (S n1)) (Rsqr x) (lt_INR_0 (S n1) (lt_O_Sn n1))); fold (x > 0) in H; apply (Rlt_0_sqr x (Rlt_dichotomy_converse x 0 (or_intror (x < 0) H))). rewrite (S_INR n0); ring. unfold Rle in H0; elim H0; intro. - unfold Rle in |- *; left; apply Rmult_lt_compat_l. + unfold Rle; left; apply Rmult_lt_compat_l. rewrite Rplus_comm; apply (Rle_lt_0_plus_1 x (Rlt_le 0 x H)). assumption. - rewrite H1; unfold Rle in |- *; right; trivial. + rewrite H1; unfold Rle; right; trivial. Qed. Lemma Power_monotonic : @@ -195,12 +195,12 @@ Lemma Power_monotonic : Rabs x > 1 -> (m <= n)%nat -> Rabs (x ^ m) <= Rabs (x ^ n). Proof. intros x m n H; induction n as [| n Hrecn]; intros; inversion H0. - unfold Rle in |- *; right; reflexivity. - unfold Rle in |- *; right; reflexivity. + unfold Rle; right; reflexivity. + unfold Rle; right; reflexivity. apply (Rle_trans (Rabs (x ^ m)) (Rabs (x ^ n)) (Rabs (x ^ S n))). apply Hrecn; assumption. - simpl in |- *; rewrite Rabs_mult. - pattern (Rabs (x ^ n)) at 1 in |- *. + simpl; rewrite Rabs_mult. + pattern (Rabs (x ^ n)) at 1. rewrite <- Rmult_1_r. rewrite (Rmult_comm (Rabs x) (Rabs (x ^ n))). apply Rmult_le_compat_l. @@ -211,7 +211,7 @@ Qed. Lemma RPow_abs : forall (x:R) (n:nat), Rabs x ^ n = Rabs (x ^ n). Proof. - intro; simple induction n; simpl in |- *. + intro; simple induction n; simpl. apply sym_eq; apply Rabs_pos_eq; apply Rlt_le; apply Rlt_0_1. intros; rewrite H; apply sym_eq; apply Rabs_mult. Qed. @@ -231,16 +231,16 @@ Proof. rewrite <- RPow_abs; cut (Rabs x = 1 + (Rabs x - 1)). intro; rewrite H3; apply (Rge_trans ((1 + (Rabs x - 1)) ^ x0) (1 + INR x0 * (Rabs x - 1)) b). - apply Rle_ge; apply poly; fold (Rabs x - 1 > 0) in |- *; apply Rgt_minus; + apply Rle_ge; apply poly; fold (Rabs x - 1 > 0); apply Rgt_minus; assumption. apply (Rge_trans (1 + INR x0 * (Rabs x - 1)) (INR x0 * (Rabs x - 1)) b). apply Rle_ge; apply Rlt_le; rewrite (Rplus_comm 1 (INR x0 * (Rabs x - 1))); - pattern (INR x0 * (Rabs x - 1)) at 1 in |- *; + pattern (INR x0 * (Rabs x - 1)) at 1; rewrite <- (let (H1, H2) := Rplus_ne (INR x0 * (Rabs x - 1)) in H1); apply Rplus_lt_compat_l; apply Rlt_0_1. cut (b = b * / (Rabs x - 1) * (Rabs x - 1)). intros; rewrite H4; apply Rmult_ge_compat_r. - apply Rge_minus; unfold Rge in |- *; left; assumption. + apply Rge_minus; unfold Rge; left; assumption. assumption. rewrite Rmult_assoc; rewrite Rinv_l. ring. @@ -252,26 +252,26 @@ Proof. apply (Rge_trans (INR x0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). rewrite INR_IZR_INZ; apply IZR_ge; omega. - unfold Rge in |- *; left; assumption. + unfold Rge; left; assumption. exists 0%nat; apply (Rge_trans (INR 0) (IZR (up (b * / (Rabs x - 1)))) (b * / (Rabs x - 1))). - rewrite INR_IZR_INZ; apply IZR_ge; simpl in |- *; omega. - unfold Rge in |- *; left; assumption. + rewrite INR_IZR_INZ; apply IZR_ge; simpl; omega. + unfold Rge; left; assumption. omega. Qed. Lemma pow_ne_zero : forall n:nat, n <> 0%nat -> 0 ^ n = 0. Proof. simple induction n. - simpl in |- *; auto. + simpl; auto. intros; elim H; reflexivity. - intros; simpl in |- *; apply Rmult_0_l. + intros; simpl; apply Rmult_0_l. Qed. Lemma Rinv_pow : forall (x:R) (n:nat), x <> 0 -> / x ^ n = (/ x) ^ n. Proof. - intros; elim n; simpl in |- *. + intros; elim n; simpl. apply Rinv_1. intro m; intro; rewrite Rinv_mult_distr. rewrite H0; reflexivity; assumption. @@ -305,7 +305,7 @@ Proof. rewrite <- Rabs_Rinv. rewrite Rinv_pow. apply (Rlt_le_trans (/ y) (/ y + 1) (Rabs ((/ x) ^ n))). - pattern (/ y) at 1 in |- *. + pattern (/ y) at 1. rewrite <- (let (H1, H2) := Rplus_ne (/ y) in H1). apply Rplus_lt_compat_l. apply Rlt_0_1. @@ -319,17 +319,17 @@ Proof. apply pow_nonzero. assumption. apply Rlt_dichotomy_converse. - right; unfold Rgt in |- *; assumption. + right; unfold Rgt; assumption. rewrite <- (Rinv_involutive 1). rewrite Rabs_Rinv. - unfold Rgt in |- *; apply Rinv_lt_contravar. + unfold Rgt; apply Rinv_lt_contravar. apply Rmult_lt_0_compat. apply Rabs_pos_lt. assumption. rewrite Rinv_1; apply Rlt_0_1. rewrite Rinv_1; assumption. assumption. - red in |- *; intro; apply R1_neq_R0; assumption. + red; intro; apply R1_neq_R0; assumption. Qed. Lemma pow_R1 : forall (r:R) (n:nat), r ^ n = 1 -> Rabs r = 1 \/ n = 0%nat. @@ -343,7 +343,7 @@ Proof. cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto. absurd (Rabs (/ r) ^ 0 < Rabs (/ r) ^ S n0); auto. replace (Rabs (/ r) ^ S n0) with 1. - simpl in |- *; apply Rlt_irrefl; auto. + simpl; apply Rlt_irrefl; auto. rewrite Rabs_Rinv; auto. rewrite <- Rinv_pow; auto. rewrite RPow_abs; auto. @@ -354,16 +354,16 @@ Proof. case (Rabs_pos r); auto. intros H'3; case Eq2; auto. rewrite Rmult_1_r; rewrite Rinv_r; auto with real. - red in |- *; intro; absurd (r ^ S n0 = 1); auto. - simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real. + red; intro; absurd (r ^ S n0 = 1); auto. + simpl; rewrite H; rewrite Rmult_0_l; auto with real. generalize H'; case n; auto. intros n0 H'0. cut (r <> 0); [ intros Eq1 | auto with real ]. cut (Rabs r <> 0); [ intros Eq2 | apply Rabs_no_R0 ]; auto. absurd (Rabs r ^ 0 < Rabs r ^ S n0); auto with real arith. - repeat rewrite RPow_abs; rewrite H'0; simpl in |- *; auto with real. - red in |- *; intro; absurd (r ^ S n0 = 1); auto. - simpl in |- *; rewrite H; rewrite Rmult_0_l; auto with real. + repeat rewrite RPow_abs; rewrite H'0; simpl; auto with real. + red; intro; absurd (r ^ S n0 = 1); auto. + simpl; rewrite H; rewrite Rmult_0_l; auto with real. Qed. Lemma pow_Rsqr : forall (x:R) (n:nat), x ^ (2 * n) = Rsqr x ^ n. @@ -373,15 +373,15 @@ Proof. replace (2 * S n)%nat with (S (S (2 * n))). replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)). rewrite Hrecn; reflexivity. - simpl in |- *; ring. + simpl; ring. ring. Qed. Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n. Proof. intros; induction n as [| n Hrecn]. - simpl in |- *; left; apply Rlt_0_1. - simpl in |- *; apply Rmult_le_pos; assumption. + simpl; left; apply Rlt_0_1. + simpl; apply Rmult_le_pos; assumption. Qed. (**********) @@ -390,36 +390,36 @@ Proof. intro; induction n as [| n Hrecn]. reflexivity. replace (2 * S n)%nat with (2 + 2 * n)%nat by ring. - rewrite pow_add; rewrite Hrecn; simpl in |- *; ring. + rewrite pow_add; rewrite Hrecn; simpl; ring. Qed. (**********) Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1. Proof. intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring. - rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring. + rewrite pow_add; rewrite pow_1_even; simpl; ring. Qed. (**********) Lemma pow_1_abs : forall n:nat, Rabs ((-1) ^ n) = 1. Proof. intro; induction n as [| n Hrecn]. - simpl in |- *; apply Rabs_R1. + simpl; apply Rabs_R1. replace (S n) with (n + 1)%nat; [ rewrite pow_add | ring ]. rewrite Rabs_mult. - rewrite Hrecn; rewrite Rmult_1_l; simpl in |- *; rewrite Rmult_1_r; + rewrite Hrecn; rewrite Rmult_1_l; simpl; rewrite Rmult_1_r; rewrite Rabs_Ropp; apply Rabs_R1. Qed. Lemma pow_mult : forall (x:R) (n1 n2:nat), x ^ (n1 * n2) = (x ^ n1) ^ n2. Proof. intros; induction n2 as [| n2 Hrecn2]. - simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ]. + simpl; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ]. replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat. replace (S n2) with (n2 + 1)%nat by ring. do 2 rewrite pow_add. rewrite Hrecn2. - simpl in |- *. + simpl. ring. ring. Qed. @@ -429,7 +429,7 @@ Proof. intros. induction n as [| n Hrecn]. right; reflexivity. - simpl in |- *. + simpl. elim H; intros. apply Rle_trans with (y * x ^ n). do 2 rewrite <- (Rmult_comm (x ^ n)). @@ -446,7 +446,7 @@ Proof. intros. induction k as [| k Hreck]. right; reflexivity. - simpl in |- *. + simpl. apply Rle_trans with (x * 1). rewrite Rmult_1_r; assumption. apply Rmult_le_compat_l. @@ -461,33 +461,33 @@ Proof. replace n with (n - m + m)%nat. rewrite pow_add. rewrite Rmult_comm. - pattern (x ^ m) at 1 in |- *; rewrite <- Rmult_1_r. + pattern (x ^ m) at 1; rewrite <- Rmult_1_r. apply Rmult_le_compat_l. apply pow_le; left; apply Rlt_le_trans with 1; [ apply Rlt_0_1 | assumption ]. apply pow_R1_Rle; assumption. rewrite plus_comm. - symmetry in |- *; apply le_plus_minus; assumption. + symmetry ; apply le_plus_minus; assumption. Qed. Lemma pow1 : forall n:nat, 1 ^ n = 1. Proof. intro; induction n as [| n Hrecn]. reflexivity. - simpl in |- *; rewrite Hrecn; rewrite Rmult_1_r; reflexivity. + simpl; rewrite Hrecn; rewrite Rmult_1_r; reflexivity. Qed. Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n. Proof. intros; induction n as [| n Hrecn]. right; reflexivity. - simpl in |- *; case (Rcase_abs x); intro. + simpl; case (Rcase_abs x); intro. apply Rle_trans with (Rabs (x * x ^ n)). apply RRle_abs. rewrite Rabs_mult. apply Rmult_le_compat_l. apply Rabs_pos. - right; symmetry in |- *; apply RPow_abs. - pattern (Rabs x) at 1 in |- *; rewrite (Rabs_right x r); + right; symmetry ; apply RPow_abs. + pattern (Rabs x) at 1; rewrite (Rabs_right x r); apply Rmult_le_compat_l. apply Rge_le; exact r. apply Hrecn. @@ -500,7 +500,7 @@ Proof. apply pow_Rabs. induction n as [| n Hrecn]. right; reflexivity. - simpl in |- *; apply Rle_trans with (x * Rabs y ^ n). + simpl; apply Rle_trans with (x * Rabs y ^ n). do 2 rewrite <- (Rmult_comm (Rabs y ^ n)). apply Rmult_le_compat_l. apply pow_le; apply Rabs_pos. @@ -517,7 +517,7 @@ Qed. (*i Due to L.Thery i*) Ltac case_eq name := - generalize (refl_equal name); pattern name at -1 in |- *; case name. + generalize (refl_equal name); pattern name at -1; case name. Definition powerRZ (x:R) (n:Z) := match n with @@ -531,7 +531,7 @@ Infix Local "^Z" := powerRZ (at level 30, right associativity) : R_scope. Lemma Zpower_NR0 : forall (x:Z) (n:nat), (0 <= x)%Z -> (0 <= Zpower_nat x n)%Z. Proof. - induction n; unfold Zpower_nat in |- *; simpl in |- *; auto with zarith. + induction n; unfold Zpower_nat; simpl; auto with zarith. Qed. Lemma powerRZ_O : forall x:R, x ^Z 0 = 1. @@ -541,60 +541,45 @@ Qed. Lemma powerRZ_1 : forall x:R, x ^Z Zsucc 0 = x. Proof. - simpl in |- *; auto with real. + simpl; auto with real. Qed. Lemma powerRZ_NOR : forall (x:R) (z:Z), x <> 0 -> x ^Z z <> 0. Proof. - destruct z; simpl in |- *; auto with real. + destruct z; simpl; auto with real. Qed. Lemma powerRZ_add : forall (x:R) (n m:Z), x <> 0 -> x ^Z (n + m) = x ^Z n * x ^Z m. Proof. - intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl in |- *; + intro x; destruct n as [| n1| n1]; destruct m as [| m1| m1]; simpl; auto with real. (* POS/POS *) - rewrite nat_of_P_plus_morphism; auto with real. + rewrite Pplus_plus; auto with real. (* POS/NEG *) - case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real. - intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real. - intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real. - rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1)); - auto with real. - rewrite plus_comm; rewrite le_plus_minus_r; auto with real. - rewrite Rinv_mult_distr; auto with real. - rewrite Rinv_involutive; auto with real. - apply lt_le_weak. - apply nat_of_P_lt_Lt_compare_morphism; auto. - apply ZC2; auto. - intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real. - rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1)); - auto with real. - rewrite plus_comm; rewrite le_plus_minus_r; auto with real. - apply lt_le_weak. - change (nat_of_P n1 > nat_of_P m1)%nat in |- *. - apply nat_of_P_gt_Gt_compare_morphism; auto. + case Pcompare_spec; intros; simpl. + subst; auto with real. + rewrite Pminus_minus by trivial. + rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real. + rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt). + rewrite Rinv_mult_distr, Rinv_involutive; auto with real. + rewrite Pminus_minus by trivial. + rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real. + rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt). + reflexivity. (* NEG/POS *) - case_eq ((n1 ?= m1)%positive Datatypes.Eq); simpl in |- *; auto with real. - intros H' H'0; rewrite Pcompare_Eq_eq with (1 := H'); auto with real. - intros H' H'0; rewrite (nat_of_P_minus_morphism m1 n1); auto with real. - rewrite (pow_RN_plus x (nat_of_P m1 - nat_of_P n1) (nat_of_P n1)); - auto with real. - rewrite plus_comm; rewrite le_plus_minus_r; auto with real. - apply lt_le_weak. - apply nat_of_P_lt_Lt_compare_morphism; auto. - apply ZC2; auto. - intros H' H'0; rewrite (nat_of_P_minus_morphism n1 m1); auto with real. - rewrite (pow_RN_plus x (nat_of_P n1 - nat_of_P m1) (nat_of_P m1)); - auto with real. - rewrite plus_comm; rewrite le_plus_minus_r; auto with real. - rewrite Rinv_mult_distr; auto with real. - apply lt_le_weak. - change (nat_of_P n1 > nat_of_P m1)%nat in |- *. - apply nat_of_P_gt_Gt_compare_morphism; auto. + case Pcompare_spec; intros; simpl. + subst; auto with real. + rewrite Pminus_minus by trivial. + rewrite (pow_RN_plus x _ (nat_of_P n1)) by auto with real. + rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt). + auto with real. + rewrite Pminus_minus by trivial. + rewrite (pow_RN_plus x _ (nat_of_P m1)) by auto with real. + rewrite plus_comm, le_plus_minus_r by (now apply lt_le_weak, Plt_lt). + rewrite Rinv_mult_distr, Rinv_involutive; auto with real. (* NEG/NEG *) - rewrite nat_of_P_plus_morphism; auto with real. + rewrite Pplus_plus; auto with real. intros H'; rewrite pow_add; auto with real. apply Rinv_mult_distr; auto. apply pow_nonzero; auto. @@ -605,16 +590,16 @@ Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real. Lemma Zpower_nat_powerRZ : forall n m:nat, IZR (Zpower_nat (Z_of_nat n) m) = INR n ^Z Z_of_nat m. Proof. - intros n m; elim m; simpl in |- *; auto with real. - intros m1 H'; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; simpl in |- *. + intros n m; elim m; simpl; auto with real. + intros m1 H'; rewrite nat_of_P_of_succ_nat; simpl. replace (Zpower_nat (Z_of_nat n) (S m1)) with (Z_of_nat n * Zpower_nat (Z_of_nat n) m1)%Z. rewrite mult_IZR; auto with real. - repeat rewrite <- INR_IZR_INZ; simpl in |- *. - rewrite H'; simpl in |- *. - case m1; simpl in |- *; auto with real. - intros m2; rewrite nat_of_P_o_P_of_succ_nat_eq_succ; auto. - unfold Zpower_nat in |- *; auto. + repeat rewrite <- INR_IZR_INZ; simpl. + rewrite H'; simpl. + case m1; simpl; auto with real. + intros m2; rewrite nat_of_P_of_succ_nat; auto. + unfold Zpower_nat; auto. Qed. Lemma Zpower_pos_powerRZ : @@ -631,7 +616,7 @@ Qed. Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z. Proof. - intros x z; case z; simpl in |- *; auto with real. + intros x z; case z; simpl; auto with real. Qed. Hint Resolve powerRZ_lt: real. @@ -644,19 +629,19 @@ Hint Resolve powerRZ_le: real. Lemma Zpower_nat_powerRZ_absolu : forall n m:Z, (0 <= m)%Z -> IZR (Zpower_nat n (Zabs_nat m)) = IZR n ^Z m. Proof. - intros n m; case m; simpl in |- *; auto with zarith. - intros p H'; elim (nat_of_P p); simpl in |- *; auto with zarith. - intros n0 H'0; rewrite <- H'0; simpl in |- *; auto with zarith. + intros n m; case m; simpl; auto with zarith. + intros p H'; elim (nat_of_P p); simpl; auto with zarith. + intros n0 H'0; rewrite <- H'0; simpl; auto with zarith. rewrite <- mult_IZR; auto. intros p H'; absurd (0 <= Zneg p)%Z; auto with zarith. Qed. Lemma powerRZ_R1 : forall n:Z, 1 ^Z n = 1. Proof. - intros n; case n; simpl in |- *; auto. - intros p; elim (nat_of_P p); simpl in |- *; auto; intros n0 H'; rewrite H'; + intros n; case n; simpl; auto. + intros p; elim (nat_of_P p); simpl; auto; intros n0 H'; rewrite H'; ring. - intros p; elim (nat_of_P p); simpl in |- *. + intros p; elim (nat_of_P p); simpl. exact Rinv_1. intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H'; auto with real. @@ -708,10 +693,10 @@ Lemma GP_finite : forall (x:R) (n:nat), sum_f_R0 (fun n:nat => x ^ n) n * (x - 1) = x ^ (n + 1) - 1. Proof. - intros; induction n as [| n Hrecn]; simpl in |- *. + intros; induction n as [| n Hrecn]; simpl. ring. rewrite Rmult_plus_distr_r; rewrite Hrecn; cut ((n + 1)%nat = S n). - intro H; rewrite H; simpl in |- *; ring. + intro H; rewrite H; simpl; ring. omega. Qed. @@ -719,8 +704,8 @@ Lemma sum_f_R0_triangle : forall (x:nat -> R) (n:nat), Rabs (sum_f_R0 x n) <= sum_f_R0 (fun i:nat => Rabs (x i)) n. Proof. - intro; simple induction n; simpl in |- *. - unfold Rle in |- *; right; reflexivity. + intro; simple induction n; simpl. + unfold Rle; right; reflexivity. intro m; intro; apply (Rle_trans (Rabs (sum_f_R0 x m + x (S m))) @@ -742,16 +727,16 @@ Definition R_dist (x y:R) : R := Rabs (x - y). (*********) Lemma R_dist_pos : forall x y:R, R_dist x y >= 0. Proof. - intros; unfold R_dist in |- *; unfold Rabs in |- *; case (Rcase_abs (x - y)); + intros; unfold R_dist; unfold Rabs; case (Rcase_abs (x - y)); intro l. - unfold Rge in |- *; left; apply (Ropp_gt_lt_0_contravar (x - y) l). + unfold Rge; left; apply (Ropp_gt_lt_0_contravar (x - y) l). trivial. Qed. (*********) Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x. Proof. - unfold R_dist in |- *; intros; split_Rabs; try ring. + unfold R_dist; intros; split_Rabs; try ring. generalize (Ropp_gt_lt_0_contravar (y - x) r); intro; rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0); intro; unfold Rgt in H; exfalso; auto. @@ -763,7 +748,7 @@ Qed. (*********) Lemma R_dist_refl : forall x y:R, R_dist x y = 0 <-> x = y. Proof. - unfold R_dist in |- *; intros; split_Rabs; split; intros. + unfold R_dist; intros; split_Rabs; split; intros. rewrite (Ropp_minus_distr x y) in H; apply sym_eq; apply (Rminus_diag_uniq y x H). rewrite (Ropp_minus_distr x y); generalize (sym_eq H); intro; @@ -774,13 +759,13 @@ Qed. Lemma R_dist_eq : forall x:R, R_dist x x = 0. Proof. - unfold R_dist in |- *; intros; split_Rabs; intros; ring. + unfold R_dist; intros; split_Rabs; intros; ring. Qed. (***********) Lemma R_dist_tri : forall x y z:R, R_dist x y <= R_dist x z + R_dist z y. Proof. - intros; unfold R_dist in |- *; replace (x - y) with (x - z + (z - y)); + intros; unfold R_dist; replace (x - y) with (x - z + (z - y)); [ apply (Rabs_triang (x - z) (z - y)) | ring ]. Qed. @@ -788,7 +773,7 @@ Qed. Lemma R_dist_plus : forall a b c d:R, R_dist (a + c) (b + d) <= R_dist a b + R_dist c d. Proof. - intros; unfold R_dist in |- *; + intros; unfold R_dist; replace (a + c - (b + d)) with (a - b + (c - d)). exact (Rabs_triang (a - b) (c - d)). ring. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index c39edf30f..b99a28d5f 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -11,11 +11,8 @@ (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (***********************************************************) -Require Export BinPos. -Require Export Pnat. -Require Import BinNat. -Require Import Plus. -Require Import Mult. +Require Export BinPos Pnat. +Require Import BinNat Plus Mult. Unset Boxed Definitions. @@ -209,10 +206,10 @@ Proof. intros P H0 Hs Hp z; destruct z. assumption. apply Pind with (P := fun p => P (Zpos p)). - change (P (Zsucc' Z0)) in |- *; apply Hs; apply H0. + change (P (Zsucc' Z0)); apply Hs; apply H0. intro n; exact (Hs (Zpos n)). apply Pind with (P := fun p => P (Zneg p)). - change (P (Zpred' Z0)) in |- *; apply Hp; apply H0. + change (P (Zpred' Z0)); apply Hp; apply H0. intro n; exact (Hp (Zneg n)). Qed. @@ -245,7 +242,7 @@ Qed. Theorem Zopp_inj : forall n m:Z, - n = - m -> n = m. Proof. - intros x y; case x; case y; simpl in |- *; intros; + intros x y; case x; case y; simpl; intros; [ trivial | discriminate H | discriminate H @@ -286,11 +283,10 @@ Qed. Theorem Zplus_comm : forall n m:Z, n + m = m + n. Proof. - intro x; induction x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; try reflexivity. + induction n as [|p|p]; intros [|q|q]; simpl; try reflexivity. rewrite Pplus_comm; reflexivity. - rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. - rewrite ZC4; destruct ((q ?= p)%positive Eq); reflexivity. + rewrite ZC4. now case Pcompare_spec. + rewrite ZC4; now case Pcompare_spec. rewrite Pplus_comm; reflexivity. Qed. @@ -299,7 +295,7 @@ Qed. Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. intro x; destruct x as [| p| p]; intro y; destruct y as [| q| q]; - simpl in |- *; reflexivity || destruct ((p ?= q)%positive Eq); + simpl; reflexivity || destruct ((p ?= q)%positive Eq); reflexivity. Qed. @@ -312,7 +308,7 @@ Qed. Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. Proof. - intro x; destruct x as [| p| p]; simpl in |- *; + intro x; destruct x as [| p| p]; simpl; [ reflexivity | rewrite (Pcompare_refl p); reflexivity | rewrite (Pcompare_refl p); reflexivity ]. @@ -330,159 +326,54 @@ Hint Local Resolve Zplus_0_l Zplus_0_r. Lemma weak_assoc : forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n. Proof. - intros x y z'; case z'; - [ auto with arith - | intros z; simpl in |- *; rewrite Pplus_assoc; auto with arith - | intros z; simpl in |- *; ElimPcompare y z; intros E0; rewrite E0; - ElimPcompare (x + y)%positive z; intros E1; rewrite E1; - [ absurd ((x + y ?= z)%positive Eq = Eq); - [ (* Case 1 *) - rewrite nat_of_P_gt_Gt_compare_complement_morphism; - [ discriminate - | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0); - elim (ZL4 x); intros k E2; rewrite E2; - simpl in |- *; unfold gt, lt in |- *; - apply le_n_S; apply le_plus_r ] - | assumption ] - | absurd ((x + y ?= z)%positive Eq = Lt); - [ (* Case 2 *) - rewrite nat_of_P_gt_Gt_compare_complement_morphism; - [ discriminate - | rewrite nat_of_P_plus_morphism; rewrite (Pcompare_Eq_eq y z E0); - elim (ZL4 x); intros k E2; rewrite E2; - simpl in |- *; unfold gt, lt in |- *; - apply le_n_S; apply le_plus_r ] - | assumption ] - | rewrite (Pcompare_Eq_eq y z E0); - (* Case 3 *) - elim (Pminus_mask_Gt (x + z) z); - [ intros t H; elim H; intros H1 H2; elim H2; intros H3 H4; - unfold Pminus in |- *; rewrite H1; cut (x = t); - [ intros E; rewrite E; auto with arith - | apply Pplus_reg_r with (r := z); rewrite <- H3; - rewrite Pplus_comm; trivial with arith ] - | pattern z at 1 in |- *; rewrite <- (Pcompare_Eq_eq y z E0); - assumption ] - | elim (Pminus_mask_Gt z y); - [ (* Case 4 *) - intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; - unfold Pminus at 1 in |- *; rewrite H1; cut (x = k); - [ intros E; rewrite E; rewrite (Pcompare_refl k); - trivial with arith - | apply Pplus_reg_r with (r := y); rewrite (Pplus_comm k y); - rewrite H3; apply Pcompare_Eq_eq; assumption ] - | apply ZC2; assumption ] - | elim (Pminus_mask_Gt z y); - [ (* Case 5 *) - intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; - unfold Pminus at 1 3 5 in |- *; rewrite H1; - cut ((x ?= k)%positive Eq = Lt); - [ intros E2; rewrite E2; elim (Pminus_mask_Gt k x); - [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9; - elim (Pminus_mask_Gt z (x + y)); - [ intros j H10; elim H10; intros H11 H12; elim H12; - intros H13 H14; unfold Pminus in |- *; - rewrite H6; rewrite H11; cut (i = j); - [ intros E; rewrite E; auto with arith - | apply (Pplus_reg_l (x + y)); rewrite H13; - rewrite (Pplus_comm x y); rewrite <- Pplus_assoc; - rewrite H8; assumption ] - | apply ZC2; assumption ] - | apply ZC2; assumption ] - | apply nat_of_P_lt_Lt_compare_complement_morphism; - apply plus_lt_reg_l with (p := nat_of_P y); - do 2 rewrite <- nat_of_P_plus_morphism; - apply nat_of_P_lt_Lt_compare_morphism; - rewrite H3; rewrite Pplus_comm; assumption ] - | apply ZC2; assumption ] - | elim (Pminus_mask_Gt z y); - [ (* Case 6 *) - intros k H; elim H; intros H1 H2; elim H2; intros H3 H4; - elim (Pminus_mask_Gt (x + y) z); - [ intros i H5; elim H5; intros H6 H7; elim H7; intros H8 H9; - unfold Pminus in |- *; rewrite H1; rewrite H6; - cut ((x ?= k)%positive Eq = Gt); - [ intros H10; elim (Pminus_mask_Gt x k H10); intros j H11; - elim H11; intros H12 H13; elim H13; - intros H14 H15; rewrite H10; rewrite H12; - cut (i = j); - [ intros H16; rewrite H16; auto with arith - | apply (Pplus_reg_l (z + k)); rewrite <- (Pplus_assoc z k j); - rewrite H14; rewrite (Pplus_comm z k); - rewrite <- Pplus_assoc; rewrite H8; - rewrite (Pplus_comm x y); rewrite Pplus_assoc; - rewrite (Pplus_comm k y); rewrite H3; - trivial with arith ] - | apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold lt, gt in |- *; - apply plus_lt_reg_l with (p := nat_of_P y); - do 2 rewrite <- nat_of_P_plus_morphism; - apply nat_of_P_lt_Lt_compare_morphism; - rewrite H3; rewrite Pplus_comm; apply ZC1; - assumption ] - | assumption ] - | apply ZC2; assumption ] - | absurd ((x + y ?= z)%positive Eq = Eq); - [ (* Case 7 *) - rewrite nat_of_P_gt_Gt_compare_complement_morphism; - [ discriminate - | rewrite nat_of_P_plus_morphism; unfold gt in |- *; - apply lt_le_trans with (m := nat_of_P y); - [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption - | apply le_plus_r ] ] - | assumption ] - | absurd ((x + y ?= z)%positive Eq = Lt); - [ (* Case 8 *) - rewrite nat_of_P_gt_Gt_compare_complement_morphism; - [ discriminate - | unfold gt in |- *; apply lt_le_trans with (m := nat_of_P y); - [ exact (nat_of_P_gt_Gt_compare_morphism y z E0) - | rewrite nat_of_P_plus_morphism; apply le_plus_r ] ] - | assumption ] - | elim Pminus_mask_Gt with (1 := E0); intros k H1; - (* Case 9 *) - elim Pminus_mask_Gt with (1 := E1); intros i H2; - elim H1; intros H3 H4; elim H4; intros H5 H6; - elim H2; intros H7 H8; elim H8; intros H9 H10; - unfold Pminus in |- *; rewrite H3; rewrite H7; - cut ((x + k)%positive = i); - [ intros E; rewrite E; auto with arith - | apply (Pplus_reg_l z); rewrite (Pplus_comm x k); rewrite Pplus_assoc; - rewrite H5; rewrite H9; rewrite Pplus_comm; - trivial with arith ] ] ]. -Qed. - -Hint Local Resolve weak_assoc. + intros x y [|z|z]; simpl; trivial. + now rewrite Pplus_assoc. + case (Pcompare_spec y z); intros E0. + (* y = z *) + subst. + assert (H := Plt_plus_r z x). rewrite Pplus_comm in H. apply ZC2 in H. + now rewrite H, Pplus_minus_eq. + (* y < z *) + assert (Hz : (z = (z-y)+y)%positive). + rewrite Pplus_comm, Pplus_minus_lt; trivial. + pattern z at 4. rewrite Hz, Pplus_compare_mono_r. + case Pcompare_spec; intros E1; trivial; f_equal. + symmetry. rewrite Pplus_comm. apply Pminus_plus_distr. + rewrite Hz, Pplus_comm. now apply Pplus_lt_mono_r. + apply Pminus_minus_distr; trivial. + (* z < y *) + assert (LT : (z < x + y)%positive). + rewrite Pplus_comm. apply Plt_trans with y; trivial using Plt_plus_r. + apply ZC2 in LT. rewrite LT. f_equal. + now apply Pplus_minus_assoc. +Qed. Theorem Zplus_assoc : forall n m p:Z, n + (m + p) = n + m + p. Proof. - intros x y z; case x; case y; case z; auto with arith; intros; - [ rewrite (Zplus_comm (Zneg p0)); rewrite weak_assoc; - rewrite (Zplus_comm (Zpos p1 + Zneg p0)); rewrite weak_assoc; - rewrite (Zplus_comm (Zpos p1)); trivial with arith - | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; - rewrite Zplus_comm; rewrite <- weak_assoc; - rewrite (Zplus_comm (- Zpos p1)); - rewrite (Zplus_comm (Zpos p0 + - Zpos p1)); rewrite (weak_assoc p); - rewrite weak_assoc; rewrite (Zplus_comm (Zpos p0)); - trivial with arith - | rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0) (Zpos p)); - rewrite <- weak_assoc; rewrite Zplus_comm; rewrite (Zplus_comm (Zpos p0)); - trivial with arith - | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; - rewrite (Zplus_comm (- Zpos p0)); rewrite weak_assoc; - rewrite (Zplus_comm (Zpos p1 + - Zpos p0)); rewrite weak_assoc; - rewrite (Zplus_comm (Zpos p)); trivial with arith - | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; - apply weak_assoc - | apply Zopp_inj; do 4 rewrite Zopp_plus_distr; do 2 rewrite Zopp_neg; - apply weak_assoc ]. + intros [|x|x] [|y|y] [|z|z]; trivial. + apply weak_assoc. + apply weak_assoc. + now rewrite !Zplus_0_r. + rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc. + f_equal; apply Zplus_comm. + apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg. + rewrite 2 (Zplus_comm (-Zpos x)), 2 (Zplus_comm _ (Zpos z)). + now rewrite weak_assoc. + now rewrite !Zplus_0_r. + rewrite 2 (Zplus_comm (Zneg x)), 2 (Zplus_comm _ (Zpos z)). + now rewrite weak_assoc. + apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg. + rewrite 2 (Zplus_comm _ (Zpos z)), 2 weak_assoc. + f_equal; apply Zplus_comm. + apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg. + apply weak_assoc. + apply Zopp_inj. rewrite !Zopp_plus_distr, !Zopp_neg. + apply weak_assoc. Qed. - Lemma Zplus_assoc_reverse : forall n m p:Z, n + m + p = n + (m + p). Proof. - intros; symmetry in |- *; apply Zplus_assoc. + intros; symmetry ; apply Zplus_assoc. Qed. (** ** Associativity mixed with commutativity *) @@ -498,7 +389,7 @@ Qed. Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. intros n m p H; cut (- n + (n + m) = - n + (n + p)); [ do 2 rewrite Zplus_assoc; rewrite (Zplus_comm (- n) n); - rewrite Zplus_opp_r; simpl in |- *; trivial with arith + rewrite Zplus_opp_r; simpl; trivial with arith | rewrite H; trivial with arith ]. Qed. @@ -506,21 +397,21 @@ Qed. Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m). Proof. - intros x y; unfold Zsucc in |- *; rewrite (Zplus_comm (x + y)); + intros x y; unfold Zsucc; rewrite (Zplus_comm (x + y)); rewrite Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); trivial with arith. Qed. Lemma Zplus_succ_r_reverse : forall n m:Z, Zsucc (n + m) = n + Zsucc m. Proof. - intros n m; unfold Zsucc in |- *; rewrite Zplus_assoc; trivial with arith. + intros n m; unfold Zsucc; rewrite Zplus_assoc; trivial with arith. Qed. Notation Zplus_succ_r := Zplus_succ_r_reverse (only parsing). Lemma Zplus_succ_comm : forall n m:Z, Zsucc n + m = n + Zsucc m. Proof. - unfold Zsucc in |- *; intros n m; rewrite <- Zplus_assoc; + unfold Zsucc; intros n m; rewrite <- Zplus_assoc; rewrite (Zplus_comm (Zpos 1)); trivial with arith. Qed. @@ -528,7 +419,7 @@ Qed. Lemma Zplus_0_r_reverse : forall n:Z, n = n + Z0. Proof. - symmetry in |- *; apply Zplus_0_r. + symmetry ; apply Zplus_0_r. Qed. Lemma Zplus_0_simpl_l : forall n m:Z, n + Z0 = m -> n = m. @@ -561,7 +452,7 @@ Qed. Theorem Zsucc_discr : forall n:Z, n <> Zsucc n. Proof. intros n; cut (Z0 <> Zpos 1); - [ unfold not in |- *; intros H1 H2; apply H1; apply (Zplus_reg_l n); + [ unfold not; intros H1 H2; apply H1; apply (Zplus_reg_l n); rewrite Zplus_0_r; exact H2 | discriminate ]. Qed. @@ -569,7 +460,7 @@ Qed. Theorem Zpos_succ_morphism : forall p:positive, Zpos (Psucc p) = Zsucc (Zpos p). Proof. - intro; rewrite Pplus_one_succ_r; unfold Zsucc in |- *; simpl in |- *; + intro; rewrite Pplus_one_succ_r; unfold Zsucc; simpl; trivial with arith. Qed. @@ -577,7 +468,7 @@ Qed. Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). Proof. - intros n; unfold Zsucc, Zpred in |- *; rewrite <- Zplus_assoc; simpl in |- *; + intros n; unfold Zsucc, Zpred; rewrite <- Zplus_assoc; simpl; rewrite Zplus_0_r; trivial with arith. Qed. @@ -585,14 +476,14 @@ Hint Immediate Zsucc_pred: zarith. Theorem Zpred_succ : forall n:Z, n = Zpred (Zsucc n). Proof. - intros m; unfold Zpred, Zsucc in |- *; rewrite <- Zplus_assoc; simpl in |- *; + intros m; unfold Zpred, Zsucc; rewrite <- Zplus_assoc; simpl; rewrite Zplus_comm; auto with arith. Qed. Theorem Zsucc_inj : forall n m:Z, Zsucc n = Zsucc m -> n = m. Proof. intros n m H. - change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m) in |- *; + change (Zneg 1 + Zpos 1 + n = Zneg 1 + Zpos 1 + m); do 2 rewrite <- Zplus_assoc; do 2 rewrite (Zplus_comm (Zpos 1)); unfold Zsucc in H; rewrite H; trivial with arith. Qed. @@ -640,10 +531,10 @@ Qed. Theorem Zsucc'_discr : forall n:Z, n <> Zsucc' n. Proof. - intro x; destruct x; simpl in |- *. + intro x; destruct x; simpl. discriminate. injection; apply Psucc_discr. - destruct p; simpl in |- *. + destruct p; simpl. discriminate. intro H; symmetry in H; injection H; apply double_moins_un_xO_discr. discriminate. @@ -658,7 +549,7 @@ Qed. Lemma Zsucc_inj_contrapositive : forall n m:Z, n <> m -> Zsucc n <> Zsucc m. Proof. - unfold not in |- *; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. + unfold not; intros n m H1 H2; apply H1; apply Zsucc_inj; assumption. Qed. (**********************************************************************) @@ -668,23 +559,23 @@ Qed. Lemma Zminus_0_r : forall n:Z, n - Z0 = n. Proof. - intro; unfold Zminus in |- *; simpl in |- *; rewrite Zplus_0_r; + intro; unfold Zminus; simpl; rewrite Zplus_0_r; trivial with arith. Qed. Lemma Zminus_0_l_reverse : forall n:Z, n = n - Z0. Proof. - intro; symmetry in |- *; apply Zminus_0_r. + intro; symmetry ; apply Zminus_0_r. Qed. Lemma Zminus_diag : forall n:Z, n - n = Z0. Proof. - intro; unfold Zminus in |- *; rewrite Zplus_opp_r; trivial with arith. + intro; unfold Zminus; rewrite Zplus_opp_r; trivial with arith. Qed. Lemma Zminus_diag_reverse : forall n:Z, Z0 = n - n. Proof. - intro; symmetry in |- *; apply Zminus_diag. + intro; symmetry ; apply Zminus_diag. Qed. @@ -697,7 +588,7 @@ Qed. Lemma Zminus_succ_l : forall n m:Z, Zsucc (n - m) = Zsucc n - m. Proof. - intros n m; unfold Zminus, Zsucc in |- *; rewrite (Zplus_comm n (- m)); + intros n m; unfold Zminus, Zsucc; rewrite (Zplus_comm n (- m)); rewrite <- Zplus_assoc; apply Zplus_comm. Qed. @@ -708,7 +599,7 @@ Qed. Lemma Zplus_minus_eq : forall n m p:Z, n = m + p -> p = n - m. Proof. - intros n m p H; unfold Zminus in |- *; apply (Zplus_reg_l m); + intros n m p H; unfold Zminus; apply (Zplus_reg_l m); rewrite (Zplus_comm m (n + - m)); rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; rewrite H; trivial with arith. @@ -716,32 +607,32 @@ Qed. Lemma Zminus_plus : forall n m:Z, n + m - n = m. Proof. - intros n m; unfold Zminus in |- *; rewrite (Zplus_comm n m); + intros n m; unfold Zminus; rewrite (Zplus_comm n m); rewrite <- Zplus_assoc; rewrite Zplus_opp_r; apply Zplus_0_r. Qed. Lemma Zplus_minus : forall n m:Z, n + (m - n) = m. Proof. - unfold Zminus in |- *; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; + unfold Zminus; intros n m; rewrite Zplus_permute; rewrite Zplus_opp_r; apply Zplus_0_r. Qed. Lemma Zminus_plus_simpl_l : forall n m p:Z, p + n - (p + m) = n - m. Proof. - intros n m p; unfold Zminus in |- *; rewrite Zopp_plus_distr; + intros n m p; unfold Zminus; rewrite Zopp_plus_distr; rewrite Zplus_assoc; rewrite (Zplus_comm p); rewrite <- (Zplus_assoc n p); rewrite Zplus_opp_r; rewrite Zplus_0_r; trivial with arith. Qed. Lemma Zminus_plus_simpl_l_reverse : forall n m p:Z, n - m = p + n - (p + m). Proof. - intros; symmetry in |- *; apply Zminus_plus_simpl_l. + intros; symmetry ; apply Zminus_plus_simpl_l. Qed. Lemma Zminus_plus_simpl_r : forall n m p:Z, n + p - (m + p) = n - m. Proof. intros x y n. - unfold Zminus in |- *. + unfold Zminus. rewrite Zopp_plus_distr. rewrite (Zplus_comm (- y) (- n)). rewrite Zplus_assoc. @@ -765,7 +656,7 @@ Qed. Lemma Zeq_minus : forall n m:Z, n = m -> n - m = Z0. Proof. - intros x y H; rewrite H; symmetry in |- *; apply Zminus_diag_reverse. + intros x y H; rewrite H; symmetry ; apply Zminus_diag_reverse. Qed. Lemma Zminus_eq : forall n m:Z, n - m = Z0 -> n = m. @@ -792,7 +683,7 @@ Qed. Theorem Zmult_1_r : forall n:Z, n * Zpos 1 = n. Proof. - intro x; destruct x; simpl in |- *; try rewrite Pmult_1_r; reflexivity. + intro x; destruct x; simpl; try rewrite Pmult_1_r; reflexivity. Qed. (** ** Zero property of multiplication *) @@ -818,7 +709,7 @@ Qed. Theorem Zmult_comm : forall n m:Z, n * m = m * n. Proof. - intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl in |- *; + intros x y; destruct x as [| p| p]; destruct y as [| q| q]; simpl; try rewrite (Pmult_comm p q); reflexivity. Qed. @@ -826,7 +717,7 @@ Qed. Theorem Zmult_assoc : forall n m p:Z, n * (m * p) = n * m * p. Proof. - intros x y z; destruct x; destruct y; destruct z; simpl in |- *; + intros x y z; destruct x; destruct y; destruct z; simpl; try rewrite Pmult_assoc; reflexivity. Qed. @@ -856,7 +747,7 @@ Qed. Theorem Zmult_integral : forall n m:Z, n * m = Z0 -> n = Z0 \/ m = Z0. Proof. - intros x y; destruct x; destruct y; auto; simpl in |- *; intro H; + intros x y; destruct x; destruct y; auto; simpl; intro H; discriminate H. Qed. @@ -898,7 +789,7 @@ Qed. Lemma Zopp_mult_distr_l_reverse : forall n m:Z, - n * m = - (n * m). Proof. - intros x y; symmetry in |- *; apply Zopp_mult_distr_l. + intros x y; symmetry ; apply Zopp_mult_distr_l. Qed. Theorem Zmult_opp_comm : forall n m:Z, - n * m = n * - m. @@ -922,34 +813,18 @@ Qed. Lemma weak_Zmult_plus_distr_r : forall (p:positive) (n m:Z), Zpos p * (n + m) = Zpos p * n + Zpos p * m. Proof. - intros x y' z'; case y'; case z'; auto with arith; intros y z; - (simpl in |- *; rewrite Pmult_plus_distr_l; trivial with arith) || - (simpl in |- *; ElimPcompare z y; intros E0; rewrite E0; - [ rewrite (Pcompare_Eq_eq z y E0); rewrite (Pcompare_refl (x * y)); - trivial with arith - | cut ((x * z ?= x * y)%positive Eq = Lt); - [ intros E; rewrite E; rewrite Pmult_minus_distr_l; - [ trivial with arith | apply ZC2; assumption ] - | apply nat_of_P_lt_Lt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); - intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_lt_Lt_compare_morphism z y E0) ] - | cut ((x * z ?= x * y)%positive Eq = Gt); - [ intros E; rewrite E; rewrite Pmult_minus_distr_l; auto with arith - | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; - do 2 rewrite nat_of_P_mult_morphism; elim (ZL4 x); - intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_gt_Gt_compare_morphism z y E0) ] ]). + intros x [ |y|y] [ |z|z]; simpl; trivial; f_equal; + apply Pmult_plus_distr_l || rewrite Pmult_compare_mono_l; + case_eq ((y ?= z) Eq)%positive; intros H; trivial; + rewrite Pmult_minus_distr_l; trivial; now apply ZC1. Qed. Theorem Zmult_plus_distr_r : forall n m p:Z, n * (m + p) = n * m + n * p. Proof. - intros x y z; case x; - [ auto with arith - | intros x'; apply weak_Zmult_plus_distr_r - | intros p; apply Zopp_inj; rewrite Zopp_plus_distr; - do 3 rewrite <- Zopp_mult_distr_l_reverse; rewrite Zopp_neg; - apply weak_Zmult_plus_distr_r ]. + intros [|x|x] y z. trivial. + apply weak_Zmult_plus_distr_r. + apply Zopp_inj; rewrite Zopp_plus_distr, !Zopp_mult_distr_l, !Zopp_neg. + apply weak_Zmult_plus_distr_r. Qed. Theorem Zmult_plus_distr_l : forall n m p:Z, (n + m) * p = n * p + m * p. @@ -962,7 +837,7 @@ Qed. Lemma Zmult_minus_distr_r : forall n m p:Z, (n - m) * p = n * p - m * p. Proof. - intros x y z; unfold Zminus in |- *. + intros x y z; unfold Zminus. rewrite <- Zopp_mult_distr_l_reverse. apply Zmult_plus_distr_l. Qed. @@ -1002,7 +877,7 @@ Qed. Lemma Zplus_diag_eq_mult_2 : forall n:Z, n + n = n * Zpos 2. Proof. - intros x; pattern x at 1 2 in |- *; rewrite <- (Zmult_1_r x); + intros x; pattern x at 1 2; rewrite <- (Zmult_1_r x); rewrite <- Zmult_plus_distr_r; reflexivity. Qed. @@ -1010,25 +885,25 @@ Qed. Lemma Zmult_succ_r : forall n m:Z, n * Zsucc m = n * m + n. Proof. - intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_r; + intros n m; unfold Zsucc; rewrite Zmult_plus_distr_r; rewrite (Zmult_comm n (Zpos 1)); rewrite Zmult_1_l; trivial with arith. Qed. Lemma Zmult_succ_r_reverse : forall n m:Z, n * m + n = n * Zsucc m. Proof. - intros; symmetry in |- *; apply Zmult_succ_r. + intros; symmetry ; apply Zmult_succ_r. Qed. Lemma Zmult_succ_l : forall n m:Z, Zsucc n * m = n * m + m. Proof. - intros n m; unfold Zsucc in |- *; rewrite Zmult_plus_distr_l; + intros n m; unfold Zsucc; rewrite Zmult_plus_distr_l; rewrite Zmult_1_l; trivial with arith. Qed. Lemma Zmult_succ_l_reverse : forall n m:Z, n * m + m = Zsucc n * m. Proof. - intros; symmetry in |- *; apply Zmult_succ_l. + intros; symmetry; apply Zmult_succ_l. Qed. @@ -1166,8 +1041,6 @@ Definition Z_of_nat (x:nat) := | S y => Zpos (P_of_succ_nat y) end. -Require Import BinNat. - Definition Zabs_N (z:Z) := match z with | Z0 => 0%N diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index 4a401a2fe..a6a25541d 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -37,8 +37,8 @@ Lemma Z_of_nat_complete : Proof. intro x; destruct x; intros; [ exists 0%nat; auto with arith - | specialize (ZL4 p); intros Hp; elim Hp; intros; exists (S x); intros; - simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x); + | specialize (nat_of_P_is_S p); intros Hp; elim Hp; intros; exists (S x); intros; + simpl in |- *; specialize (nat_of_P_of_succ_nat x); intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos); apply nat_of_P_inj; auto with arith | absurd (0 <= Zneg p); @@ -47,7 +47,7 @@ Proof. | assumption ] ]. Qed. -Lemma ZL4_inf : forall y:positive, {h : nat | nat_of_P y = S h}. +Lemma nat_of_P_is_S_inf : forall y:positive, {h : nat | nat_of_P y = S h}. Proof. intro y; induction y as [p H| p H1| ]; [ elim H; intros x H1; exists (S x + S x)%nat; unfold nat_of_P in |- *; @@ -59,13 +59,15 @@ Proof. | exists 0%nat; auto with arith ]. Qed. +Notation ZL4_inf := nat_of_P_is_S_inf (only parsing). + Lemma Z_of_nat_complete_inf : forall x:Z, 0 <= x -> {n : nat | x = Z_of_nat n}. Proof. intro x; destruct x; intros; [ exists 0%nat; auto with arith - | specialize (ZL4_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0); - intros; simpl in |- *; specialize (nat_of_P_o_P_of_succ_nat_eq_succ x0); + | specialize (nat_of_P_is_S_inf p); intros Hp; elim Hp; intros x0 H0; exists (S x0); + intros; simpl in |- *; specialize (nat_of_P_of_succ_nat x0); intro Hx0; rewrite <- H0 in Hx0; apply f_equal with (f := Zpos); apply nat_of_P_inj; auto with arith | absurd (0 <= Zneg p); @@ -127,20 +129,18 @@ Section Efficient_Rec. Let R_wf : well_founded R. Proof. - set - (f := - fun z => + set (f z := match z with | Zpos p => nat_of_P p | Z0 => 0%nat | Zneg _ => 0%nat - end) in *. + end). apply well_founded_lt_compat with f. - unfold R, f in |- *; clear f R. - intros x y; case x; intros; elim H; clear H. - case y; intros; apply lt_O_nat_of_P || inversion H0. - case y; intros; apply nat_of_P_lt_Lt_compare_morphism || inversion H0; auto. - intros; elim H; auto. + unfold R, f; clear f R. + intros [|x|x] [|y|y] (H,H'); + try (now elim H); try (discriminate H'). + apply nat_of_P_pos. + now apply Plt_lt. Qed. Lemma natlike_rec2 : diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 8543652c6..a90b5bd69 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -125,7 +125,7 @@ Qed. Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n. Proof. destruct n; simpl; auto. - apply nat_of_P_o_P_of_succ_nat_eq_succ. + apply nat_of_P_of_succ_nat. Qed. Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat. diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v index 5e7441462..10f07a864 100644 --- a/theories/ZArith/Zcompare.v +++ b/theories/ZArith/Zcompare.v @@ -13,32 +13,26 @@ (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) (**********************************************************************) -Require Export BinPos. -Require Export BinInt. -Require Import Lt. -Require Import Gt. -Require Import Plus. -Require Import Mult. +Require Export BinPos BinInt. +Require Import Lt Gt Plus Mult. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (***************************) (** * Comparison on integers *) Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq. Proof. - intro x; destruct x as [| p| p]; simpl in |- *; - [ reflexivity | apply Pcompare_refl | rewrite Pcompare_refl; reflexivity ]. + destruct n as [|p|p]; simpl; trivial. + apply Pcompare_refl. + apply CompOpp_iff, Pcompare_refl. Qed. Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m. Proof. - intros x y; destruct x as [| x'| x']; destruct y as [| y'| y']; simpl in |- *; - intro H; reflexivity || (try discriminate H); - [ rewrite (Pcompare_Eq_eq x' y' H); reflexivity - | rewrite (Pcompare_Eq_eq x' y'); - [ reflexivity - | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ]. + intros [|x|x] [|y|y] H; simpl in *; try easy; f_equal. + now apply Pcompare_Eq_eq. + apply CompOpp_iff in H. now apply Pcompare_Eq_eq. Qed. Ltac destr_zcompare := @@ -52,45 +46,40 @@ Ltac destr_zcompare := Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m. Proof. - intros x y; split; intro E; - [ apply Zcompare_Eq_eq; assumption | rewrite E; apply Zcompare_refl ]. + intros x y; split; intro E; subst. + now apply Zcompare_Eq_eq. now apply Zcompare_refl. Qed. Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n). Proof. - intros x y; destruct x; destruct y; simpl in |- *; - reflexivity || discriminate H || rewrite Pcompare_antisym; - reflexivity. + intros [|x|x] [|y|y]; simpl; try easy; f_equal; apply Pcompare_antisym. Qed. -Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. +Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m). Proof. - intros x y. - rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt). - split. - auto using CompOpp_inj. - intros; f_equal; auto. + intros. + destruct (n?=m) as [ ]_eqn:H; constructor; trivial. + now apply Zcompare_Eq_eq. + red; now rewrite <- Zcompare_antisym, H. Qed. -Lemma Zcompare_spec : forall n m, CompSpec eq Zlt n m (n ?= m). +Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. Proof. - intros. - destruct (n?=m) as [ ]_eqn:H; constructor; auto. - apply Zcompare_Eq_eq; auto. - red; rewrite <- Zcompare_antisym, H; auto. + intros x y. + rewrite <- Zcompare_antisym. change Gt with (CompOpp Lt). + split. + auto using CompOpp_inj. + intros; f_equal; auto. Qed. - (** * Transitivity of comparison *) Lemma Zcompare_Lt_trans : forall n m p:Z, (n ?= m) = Lt -> (m ?= p) = Lt -> (n ?= p) = Lt. Proof. - intros x y z; case x; case y; case z; simpl; - try discriminate; auto with arith. - intros; eapply Plt_trans; eauto. - intros p q r; rewrite 3 Pcompare_antisym; simpl. - intros; eapply Plt_trans; eauto. + intros n m p; destruct n,m,p; simpl; try discriminate; trivial. + eapply Plt_trans; eauto. + rewrite 3 Pcompare_antisym; simpl. intros; eapply Plt_trans; eauto. Qed. Lemma Zcompare_Gt_trans : @@ -107,281 +96,105 @@ Qed. Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n). Proof. - intros x y; case x; case y; simpl in |- *; auto with arith; intros; - rewrite <- ZC4; trivial with arith. + destruct n, m; simpl; trivial; intros; now rewrite <- ZC4. Qed. -Hint Local Resolve Pcompare_refl. - (** * Comparison first-order specification *) Lemma Zcompare_Gt_spec : - forall n m:Z, (n ?= m) = Gt -> exists h : positive, n + - m = Zpos h. -Proof. - intros x y; case x; case y; - [ simpl in |- *; intros H; discriminate H - | simpl in |- *; intros p H; discriminate H - | intros p H; exists p; simpl in |- *; auto with arith - | intros p H; exists p; simpl in |- *; auto with arith - | intros q p H; exists (p - q)%positive; unfold Zplus, Zopp in |- *; - unfold Zcompare in H; rewrite H; trivial with arith - | intros q p H; exists (p + q)%positive; simpl in |- *; trivial with arith - | simpl in |- *; intros p H; discriminate H - | simpl in |- *; intros q p H; discriminate H - | unfold Zcompare in |- *; intros q p; rewrite <- ZC4; intros H; - exists (q - p)%positive; simpl in |- *; rewrite (ZC1 q p H); - trivial with arith ]. + forall n m:Z, (n ?= m) = Gt -> exists h, n + - m = Zpos h. +Proof. + intros [|p|p] [|q|q]; simpl; try discriminate. + now exists q. + now exists p. + intros GT. exists (p-q)%positive. now rewrite GT. + now exists (p+q)%positive. + intros LT. apply CompOpp_iff in LT. simpl in LT. + exists (q-p)%positive. now rewrite LT. Qed. (** * Comparison and addition *) -Lemma weaken_Zcompare_Zplus_compatible : - (forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m)) -> - forall n m p:Z, (p + n ?= p + m) = (n ?= m). -Proof. - intros H x y z; destruct z; - [ reflexivity - | apply H - | rewrite (Zcompare_opp x y); rewrite Zcompare_opp; - do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; - apply H ]. -Qed. - -Hint Local Resolve ZC4. +Local Hint Resolve Pcompare_refl. -Lemma weak_Zcompare_Zplus_compatible : +Lemma weak_Zcompare_plus_compat : forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m). Proof. - intros x y z; case x; case y; simpl in |- *; auto with arith; - [ intros p; apply nat_of_P_lt_Lt_compare_complement_morphism; apply ZL17 - | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith; - apply nat_of_P_gt_Gt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply ZL16 | assumption ] - | intros p; ElimPcompare z p; intros E; auto with arith; - apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; apply ZL17 - | intros p q; ElimPcompare q p; intros E; rewrite E; - [ rewrite (Pcompare_Eq_eq q p E); apply Pcompare_refl - | apply nat_of_P_lt_Lt_compare_complement_morphism; - do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism with (1 := E) - | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *; - do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l; - exact (nat_of_P_gt_Gt_compare_morphism q p E) ] - | intros p q; ElimPcompare z p; intros E; rewrite E; auto with arith; - apply nat_of_P_gt_Gt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply lt_trans with (m := nat_of_P z); - [ apply ZL16 | apply ZL17 ] - | assumption ] - | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith; - simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; [ apply ZL16 | assumption ] - | intros p q; ElimPcompare z q; intros E; rewrite E; auto with arith; - simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ apply lt_trans with (m := nat_of_P z); [ apply ZL16 | apply ZL17 ] - | assumption ] - | intros p q; ElimPcompare z q; intros E0; rewrite E0; ElimPcompare z p; - intros E1; rewrite E1; ElimPcompare q p; intros E2; - rewrite E2; auto with arith; - [ absurd ((q ?= p)%positive Eq = Lt); - [ rewrite <- (Pcompare_Eq_eq z q E0); - rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); - discriminate - | assumption ] - | absurd ((q ?= p)%positive Eq = Gt); - [ rewrite <- (Pcompare_Eq_eq z q E0); - rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); - discriminate - | assumption ] - | absurd ((z ?= p)%positive Eq = Lt); - [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); - rewrite (Pcompare_refl q); discriminate - | assumption ] - | absurd ((z ?= p)%positive Eq = Lt); - [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate - | assumption ] - | absurd ((z ?= p)%positive Eq = Gt); - [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); - rewrite (Pcompare_refl q); discriminate - | assumption ] - | absurd ((z ?= p)%positive Eq = Gt); - [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate - | assumption ] - | absurd ((z ?= q)%positive Eq = Lt); - [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); - rewrite (Pcompare_refl p); discriminate - | assumption ] - | absurd ((p ?= q)%positive Eq = Gt); - [ rewrite <- (Pcompare_Eq_eq z p E1); rewrite E0; discriminate - | apply ZC2; assumption ] - | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); - rewrite (Pcompare_refl (p - z)); auto with arith - | simpl in |- *; rewrite <- ZC4; - apply nat_of_P_gt_Gt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); - rewrite le_plus_minus_r; - [ rewrite le_plus_minus_r; - [ apply nat_of_P_lt_Lt_compare_morphism; assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - assumption ] - | apply ZC2; assumption ] - | apply ZC2; assumption ] - | simpl in |- *; rewrite <- ZC4; - apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P z); - rewrite le_plus_minus_r; - [ rewrite le_plus_minus_r; - [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - assumption ] - | apply ZC2; assumption ] - | apply ZC2; assumption ] - | absurd ((z ?= q)%positive Eq = Lt); - [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate - | assumption ] - | absurd ((q ?= p)%positive Eq = Lt); - [ cut ((q ?= p)%positive Eq = Gt); - [ intros E; rewrite E; discriminate - | apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; apply lt_trans with (m := nat_of_P z); - [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption - | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ] - | assumption ] - | absurd ((z ?= q)%positive Eq = Gt); - [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); - rewrite (Pcompare_refl p); discriminate - | assumption ] - | absurd ((z ?= q)%positive Eq = Gt); - [ rewrite (Pcompare_Eq_eq z p E1); rewrite ZC1; - [ discriminate | assumption ] - | assumption ] - | absurd ((z ?= q)%positive Eq = Gt); - [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate - | assumption ] - | absurd ((q ?= p)%positive Eq = Gt); - [ rewrite ZC1; - [ discriminate - | apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; apply lt_trans with (m := nat_of_P z); - [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption - | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ] - | assumption ] - | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); apply Pcompare_refl - | simpl in |- *; apply nat_of_P_gt_Gt_compare_complement_morphism; - unfold gt in |- *; rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P p); - rewrite le_plus_minus_r; - [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P q); - rewrite plus_assoc; rewrite le_plus_minus_r; - [ rewrite (plus_comm (nat_of_P q)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; - assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | assumption ] - | assumption ] - | simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P q); - rewrite le_plus_minus_r; - [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); - rewrite plus_assoc; rewrite le_plus_minus_r; - [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | assumption ] - | assumption ] ] ]. + intros [|x|x] [|y|y] z; simpl; trivial; try apply ZC2; + try apply Plt_plus_r. + case Pcompare_spec; intros E0; trivial; try apply ZC2; + now apply Pminus_decr. + apply Pplus_compare_mono_l. + case Pcompare_spec; intros E0; trivial; try apply ZC2. + apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r. + case Pcompare_spec; intros E0; trivial; try apply ZC2. + now apply Pminus_decr. + case Pcompare_spec; intros E0; trivial; try apply ZC2. + apply Plt_trans with z. now apply Pminus_decr. apply Plt_plus_r. + case Pcompare_spec; intros E0; simpl; subst. + now case Pcompare_spec. + case Pcompare_spec; intros E1; simpl; subst; trivial. + now rewrite <- ZC4. + f_equal. + apply Pminus_compare_mono_r; trivial. + rewrite <- ZC4. symmetry. now apply Plt_trans with z. + case Pcompare_spec; intros E1; simpl; subst; trivial. + now rewrite E0. + symmetry. apply CompOpp_iff. now apply Plt_trans with z. + rewrite <- ZC4. + apply Pminus_compare_mono_l; trivial. Qed. Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m). Proof. - exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible). + intros x y [|z|z]; trivial. + apply weak_Zcompare_plus_compat. + rewrite (Zcompare_opp x y), Zcompare_opp, 2 Zopp_plus_distr, Zopp_neg. + apply weak_Zcompare_plus_compat. Qed. Lemma Zplus_compare_compat : forall (r:comparison) (n m p q:Z), (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r. Proof. - intros r x y z t; case r; - [ intros H1 H2; elim (Zcompare_Eq_iff_eq x y); elim (Zcompare_Eq_iff_eq z t); - intros H3 H4 H5 H6; rewrite H3; - [ rewrite H5; - [ elim (Zcompare_Eq_iff_eq (y + t) (y + t)); auto with arith - | auto with arith ] - | auto with arith ] - | intros H1 H2; elim (Zcompare_Gt_Lt_antisym (y + t) (x + z)); intros H3 H4; - apply H3; apply Zcompare_Gt_trans with (m := y + z); - [ rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym t z); - auto with arith - | do 2 rewrite <- (Zplus_comm z); rewrite Zcompare_plus_compat; - elim (Zcompare_Gt_Lt_antisym y x); auto with arith ] - | intros H1 H2; apply Zcompare_Gt_trans with (m := x + t); - [ rewrite Zcompare_plus_compat; assumption - | do 2 rewrite <- (Zplus_comm t); rewrite Zcompare_plus_compat; - assumption ] ]. + intros [ | | ] x y z t H H'. + apply Zcompare_Eq_eq in H. apply Zcompare_Eq_eq in H'. subst. + apply Zcompare_refl. + apply Zcompare_Lt_trans with (y+z). + now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat. + now rewrite Zcompare_plus_compat. + apply Zcompare_Gt_trans with (y+z). + now rewrite 2 (Zplus_comm _ z), Zcompare_plus_compat. + now rewrite Zcompare_plus_compat. Qed. Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt. Proof. - intro x; unfold Zsucc in |- *; pattern x at 2 in |- *; - rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat; - reflexivity. -Qed. - -Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m + 1) <> Lt. -Proof. - intros x y; split; - [ intro H; elim_compare x (y + 1); - [ intro H1; rewrite H1; discriminate - | intros H1; elim Zcompare_Gt_spec with (1 := H); intros h H2; - absurd ((nat_of_P h > 0)%nat /\ (nat_of_P h < 1)%nat); - [ unfold not in |- *; intros H3; elim H3; intros H4 H5; - absurd (nat_of_P h > 0)%nat; - [ unfold gt in |- *; apply le_not_lt; apply le_S_n; exact H5 - | assumption ] - | split; - [ elim (ZL4 h); intros i H3; rewrite H3; apply gt_Sn_O - | change (nat_of_P h < nat_of_P 1)%nat in |- *; - apply nat_of_P_lt_Lt_compare_morphism; - change ((Zpos h ?= 1) = Lt) in |- *; rewrite <- H2; - rewrite <- (fun m n:Z => Zcompare_plus_compat m n y); - rewrite (Zplus_comm x); rewrite Zplus_assoc; - rewrite Zplus_opp_r; simpl in |- *; exact H1 ] ] - | intros H1; rewrite H1; discriminate ] - | intros H; elim_compare x (y + 1); - [ intros H1; elim (Zcompare_Eq_iff_eq x (y + 1)); intros H2 H3; - rewrite (H2 H1); exact (Zcompare_succ_Gt y) - | intros H1; absurd ((x ?= y + 1) = Lt); assumption - | intros H1; apply Zcompare_Gt_trans with (m := Zsucc y); - [ exact H1 | exact (Zcompare_succ_Gt y) ] ] ]. + intro x; unfold Zsucc; pattern x at 2; rewrite <- (Zplus_0_r x); + now rewrite Zcompare_plus_compat. +Qed. + +Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m+1) <> Lt. +Proof. + intros x y; split; intros H. + (* -> *) + destruct (Zcompare_Gt_spec _ _ H) as (h,EQ). + replace x with (y+Zpos h) by (rewrite <- EQ; apply Zplus_minus). + rewrite Zcompare_plus_compat. apply Plt_1. + (* <- *) + assert (H' := Zcompare_succ_Gt y). + destruct (Zcompare_spec x (y+1)) as [->|LT|GT]; trivial. + now elim H. + apply Zcompare_Gt_Lt_antisym in GT. + apply Zcompare_Gt_trans with (y+1); trivial. Qed. (** * Successor and comparison *) Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m). Proof. - intros n m; unfold Zsucc in |- *; do 2 rewrite (fun t:Z => Zplus_comm t 1); - rewrite Zcompare_plus_compat; auto with arith. + intros n m; unfold Zsucc; + now rewrite 2 (Zplus_comm _ 1), Zcompare_plus_compat. Qed. (** * Multiplication and comparison *) @@ -389,28 +202,13 @@ Qed. Lemma Zcompare_mult_compat : forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m). Proof. - intros x; induction x as [p H| p H| ]; - [ intros y z; cut (Zpos (xI p) = Zpos p + Zpos p + 1); - [ intros E; rewrite E; do 4 rewrite Zmult_plus_distr_l; - do 2 rewrite Zmult_1_l; apply Zplus_compare_compat; - [ apply Zplus_compare_compat; apply H | trivial with arith ] - | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ] - | intros y z; cut (Zpos (xO p) = Zpos p + Zpos p); - [ intros E; rewrite E; do 2 rewrite Zmult_plus_distr_l; - apply Zplus_compare_compat; apply H - | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ] - | intros y z; do 2 rewrite Zmult_1_l; trivial with arith ]. + intros p [|n|n] [|m|m]; simpl; trivial. + apply Pmult_compare_mono_l. + f_equal. apply Pmult_compare_mono_l. Qed. - (** * Reverting [x ?= y] to trichotomy *) -Lemma rename : - forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. -Proof. - auto with arith. -Qed. - Lemma Zcompare_elim : forall (c1 c2 c3:Prop) (n m:Z), (n = m -> c1) -> @@ -421,11 +219,9 @@ Lemma Zcompare_elim : | Gt => c3 end. Proof. - intros c1 c2 c3 x y; intros. - apply rename with (x := x ?= y); intro r; elim r; - [ intro; apply H; apply (Zcompare_Eq_eq x y); assumption - | unfold Zlt in H0; assumption - | unfold Zgt in H1; assumption ]. + intros c1 c2 c3 x y EQ LT GT; intros. + case Zcompare_spec; auto. + intro H. apply GT. red. now rewrite <- Zcompare_antisym, H. Qed. Lemma Zcompare_eq_case : @@ -450,8 +246,8 @@ Lemma Zcompare_egal_dec : (n > m -> p > q) -> (n ?= m) = (p ?= q). Proof. intros x1 y1 x2 y2. - unfold Zgt in |- *; unfold Zlt in |- *; case (x1 ?= y1); case (x2 ?= y2); - auto with arith; symmetry in |- *; auto with arith. + unfold Zgt; unfold Zlt; case (x1 ?= y1); case (x2 ?= y2); + auto with arith; symmetry; auto with arith. Qed. (** * Relating [x ?= y] to [Zle], [Zlt], [Zge] or [Zgt] *) @@ -464,7 +260,7 @@ Lemma Zle_compare : | Gt => False end. Proof. - intros x y; unfold Zle in |- *; elim (x ?= y); auto with arith. + intros x y; unfold Zle; elim (x ?= y); auto with arith. Qed. Lemma Zlt_compare : @@ -487,7 +283,7 @@ Lemma Zge_compare : | Gt => True end. Proof. - intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. + intros x y; unfold Zge; elim (x ?= y); auto. Qed. Lemma Zgt_compare : @@ -498,8 +294,7 @@ Lemma Zgt_compare : | Gt => True end. Proof. - intros x y; unfold Zgt in |- *; elim (x ?= y); intros; - discriminate || trivial with arith. + intros x y; unfold Zgt; now elim (x ?= y). Qed. (*********************) @@ -517,7 +312,7 @@ Qed. Lemma Zmult_compare_compat_r : forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p). Proof. - intros x y z H; rewrite (Zmult_comm x z); rewrite (Zmult_comm y z); + intros x y z H; rewrite 2 (Zmult_comm _ z); apply Zmult_compare_compat_l; assumption. Qed. diff --git a/theories/ZArith/Zdiv_def.v b/theories/ZArith/Zdiv_def.v index 0e71bb4c3..a45d433c8 100644 --- a/theories/ZArith/Zdiv_def.v +++ b/theories/ZArith/Zdiv_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Nnat Ndiv_def. +Require Import BinPos BinNat BinInt Zbool Zcompare Zorder Zabs Znat Ndiv_def. Local Open Scope Z_scope. (** * Definitions of divisions for binary integers *) diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v index 588b33037..44983f691 100644 --- a/theories/ZArith/Zlog_def.v +++ b/theories/ZArith/Zlog_def.v @@ -12,55 +12,27 @@ Local Open Scope Z_scope. (** Definition of Zlog2 *) -Fixpoint Plog2_Z (p:positive) : Z := - match p with - | 1 => Z0 - | p~0 => Zsucc (Plog2_Z p) - | p~1 => Zsucc (Plog2_Z p) - end%positive. - Definition Zlog2 z := match z with - | Zpos p => Plog2_Z p + | Zpos (p~1) => Zpos (Psize_pos p) + | Zpos (p~0) => Zpos (Psize_pos p) | _ => 0 end. -Lemma Plog2_Z_nonneg : forall p, 0 <= Plog2_Z p. -Proof. - induction p; simpl; auto with zarith. -Qed. - -Lemma Plog2_Z_spec : forall p, - 2^(Plog2_Z p) <= Zpos p < 2^(Zsucc (Plog2_Z p)). -Proof. - induction p; simpl; - try rewrite 2 Zpower_succ_r; auto using Plog2_Z_nonneg with zarith. - (* p~1 *) - change (Zpos p~1) with (Zsucc (2 * Zpos p)). - split; destruct IHp as [LE LT]. - apply Zle_trans with (2 * Zpos p). - now apply Zmult_le_compat_l. - apply Zle_succ. - apply Zle_succ_l. apply Zle_succ_l in LT. - replace (Zsucc (Zsucc (2 * Zpos p))) with (2 * (Zsucc (Zpos p))). - now apply Zmult_le_compat_l. - simpl. now rewrite Pplus_one_succ_r. - (* p~0 *) - change (Zpos p~0) with (2 * Zpos p). - split; destruct IHp. - now apply Zmult_le_compat_l. - now apply Zmult_lt_compat_l. - (* 1 *) - now split. -Qed. - Lemma Zlog2_spec : forall n, 0 < n -> 2^(Zlog2 n) <= n < 2^(Zsucc (Zlog2 n)). Proof. - intros [|p|p] Hn; try discriminate. apply Plog2_Z_spec. + intros [|[p|p|]|] Hn; split; try easy; unfold Zlog2; + rewrite <- ?Zpos_succ_morphism, Zpower_Ppow. + eapply Zle_trans with (Zpos (p~0)). + apply Psize_pos_le. + apply Zlt_le_weak. exact (Pcompare_p_Sp (p~0)). + apply Psize_pos_gt. + apply Psize_pos_le. + apply Psize_pos_gt. Qed. Lemma Zlog2_nonpos : forall n, n<=0 -> Zlog2 n = 0. Proof. - intros [|p|p] Hn. reflexivity. now destruct Hn. reflexivity. + intros [|p|p] H; trivial; now destruct H. Qed. diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index ddb1eed9f..b80e96c2a 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -7,9 +7,12 @@ (************************************************************************) (**********************************************************************) + (** The integer logarithms with base 2. - There are three logarithms, + NOTA: This file is deprecated, please use Zlog2 defined in Zlog_def. + + There are three logarithms defined here, depending on the rounding of the real 2-based logarithm: - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] @@ -25,9 +28,12 @@ Section Log_pos. (* Log of positive integers *) (** First we build [log_inf] and [log_sup] *) - (** [log_inf] is exactly the same as the new [Plog2_Z] *) - - Definition log_inf : positive -> Z := Eval red in Plog2_Z. + Fixpoint log_inf (p:positive) : Z := + match p with + | xH => 0 (* 1 *) + | xO q => Zsucc (log_inf q) (* 2n *) + | xI q => Zsucc (log_inf q) (* 2n+1 *) + end. Fixpoint log_sup (p:positive) : Z := match p with @@ -38,8 +44,15 @@ Section Log_pos. (* Log of positive integers *) Hint Unfold log_inf log_sup. + Lemma Psize_log_inf : forall p, Zpos (Psize_pos p) = Zsucc (log_inf p). + Proof. + induction p; simpl; now rewrite ?Zpos_succ_morphism, ?IHp. + Qed. + Lemma Zlog2_log_inf : forall p, Zlog2 (Zpos p) = log_inf p. - Proof. reflexivity. Qed. + Proof. + unfold Zlog2. destruct p; simpl; trivial; apply Psize_log_inf. + Qed. Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. Proof. diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index b4bd470ab..f6b038cbd 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -18,13 +18,6 @@ Open Local Scope Z_scope. (** [n]th iteration of the function [f] *) -Fixpoint iter_pos (n:positive) (A:Type) (f:A -> A) (x:A) : A := - match n with - | xH => f x - | xO n' => iter_pos n' A f (iter_pos n' A f x) - | xI n' => f (iter_pos n' A f (iter_pos n' A f x)) - end. - Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := match n with | Z0 => x @@ -32,58 +25,9 @@ Definition iter (n:Z) (A:Type) (f:A -> A) (x:A) := | Zneg p => x end. -Theorem iter_nat_of_P : - forall (p:positive) (A:Type) (f:A -> A) (x:A), - iter_pos p A f x = iter_nat (nat_of_P p) A f x. -Proof. - intro n; induction n as [p H| p H| ]; - [ intros; simpl in |- *; rewrite (H A f x); - rewrite (H A f (iter_nat (nat_of_P p) A f x)); - rewrite (ZL6 p); symmetry in |- *; apply f_equal with (f := f); - apply iter_nat_plus - | intros; unfold nat_of_P in |- *; simpl in |- *; rewrite (H A f x); - rewrite (H A f (iter_nat (nat_of_P p) A f x)); - rewrite (ZL6 p); symmetry in |- *; apply iter_nat_plus - | simpl in |- *; auto with arith ]. -Qed. - Lemma iter_nat_of_Z : forall n A f x, 0 <= n -> iter n A f x = iter_nat (Zabs_nat n) A f x. intros n A f x; case n; auto. intros p _; unfold iter, Zabs_nat; apply iter_nat_of_P. intros p abs; case abs; trivial. Qed. - -Theorem iter_pos_plus : - forall (p q:positive) (A:Type) (f:A -> A) (x:A), - iter_pos (p + q) A f x = iter_pos p A f (iter_pos q A f x). -Proof. - intros n m; intros. - rewrite (iter_nat_of_P m A f x). - rewrite (iter_nat_of_P n A f (iter_nat (nat_of_P m) A f x)). - rewrite (iter_nat_of_P (n + m) A f x). - rewrite (nat_of_P_plus_morphism n m). - apply iter_nat_plus. -Qed. - -(** Preservation of invariants : if [f : A->A] preserves the invariant [Inv], - then the iterates of [f] also preserve it. *) - -Theorem iter_nat_invariant : - forall (n:nat) (A:Type) (f:A -> A) (Inv:A -> Prop), - (forall x:A, Inv x -> Inv (f x)) -> - forall x:A, Inv x -> Inv (iter_nat n A f x). -Proof. - simple induction n; intros; - [ trivial with arith - | simpl in |- *; apply H0 with (x := iter_nat n0 A f x); apply H; - trivial with arith ]. -Qed. - -Theorem iter_pos_invariant : - forall (p:positive) (A:Type) (f:A -> A) (Inv:A -> Prop), - (forall x:A, Inv x -> Inv (f x)) -> - forall x:A, Inv x -> Inv (iter_pos p A f x). -Proof. - intros; rewrite iter_nat_of_P; apply iter_nat_invariant; trivial with arith. -Qed. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index c7e6d5750..5f4a6e38d 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -10,14 +10,8 @@ (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) Require Export Arith_base. -Require Import BinPos. -Require Import BinInt. -Require Import Zcompare. -Require Import Zorder. -Require Import Decidable. -Require Import Peano_dec. -Require Import Min Max. -Require Export Compare_dec. +Require Import BinPos BinInt BinNat Zcompare Zorder. +Require Import Decidable Peano_dec Min Max Compare_dec. Open Local Scope Z_scope. @@ -26,46 +20,49 @@ Definition neq (x y:nat) := x <> y. (************************************************) (** Properties of the injection from nat into Z *) +Lemma Zpos_P_of_succ_nat : forall n:nat, + Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). +Proof. + intros [|n]. trivial. apply Zpos_succ_morphism. +Qed. + (** Injection and successor *) -Theorem inj_0 : Z_of_nat 0 = 0%Z. +Theorem inj_0 : Z_of_nat 0 = 0. Proof. reflexivity. Qed. Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n). Proof. - intro y; induction y as [| n H]; - [ unfold Zsucc in |- *; simpl in |- *; trivial with arith - | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *; - rewrite Zpos_succ_morphism; trivial with arith ]. + exact Zpos_P_of_succ_nat. +Qed. + +(** Injection and comparison *) + +Theorem inj_compare : forall n m:nat, + (Z_of_nat n ?= Z_of_nat m) = nat_compare n m. +Proof. + induction n; destruct m; trivial. + rewrite 2 inj_S, Zcompare_succ_compat. now simpl. Qed. (** Injection and equality. *) Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m. Proof. - intros x y H; rewrite H; trivial with arith. + intros; subst; trivial. Qed. -Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m). +Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m. Proof. - unfold neq, Zne, not in |- *; intros x y H1 H2; apply H1; generalize H2; - case x; case y; intros; - [ auto with arith - | discriminate H0 - | discriminate H0 - | simpl in H0; injection H0; - do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ; - intros E; rewrite E; auto with arith ]. + intros n m H. apply nat_compare_eq. + now rewrite <- inj_compare, H, Zcompare_refl. Qed. -Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m. +Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m). Proof. - intros x y H. - destruct (eq_nat_dec x y) as [H'|H']; auto. - exfalso. - exact (inj_neq _ _ H' H). + unfold neq, Zne. intros n m H. contradict H. now apply inj_eq_rev. Qed. Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m. @@ -73,17 +70,9 @@ Proof. split; [apply inj_eq | apply inj_eq_rev]. Qed. +(** Injection and order *) -(** Injection and order relations: *) - -Theorem inj_compare : forall n m:nat, - (Z_of_nat n ?= Z_of_nat m) = nat_compare n m. -Proof. - induction n; destruct m; trivial. - rewrite 2 inj_S, Zcompare_succ_compat. now simpl. -Qed. - -(* Both ways ... *) +(** Both ways ... *) Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m. Proof. @@ -137,50 +126,43 @@ Proof. apply inj_gt_iff. Qed. Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m. Proof. - intro x; induction x as [| n H]; intro y; destruct y as [| m]; - [ simpl in |- *; trivial with arith - | simpl in |- *; trivial with arith - | simpl in |- *; rewrite <- plus_n_O; trivial with arith - | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *; - rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l; - trivial with arith ]. + induction n as [|n IH]; intros [|m]; simpl; trivial. + rewrite <- plus_n_O; trivial. + change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)). + now rewrite inj_S, IH, 2 inj_S, Zplus_succ_l. Qed. Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m. Proof. - intro x; induction x as [| n H]; - [ simpl in |- *; trivial with arith - | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H; - rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; - trivial with arith ]. + induction n as [|n IH]; intros m; trivial. + rewrite inj_S, Zmult_succ_l, <- IH, <- inj_plus. + simpl. now rewrite plus_comm. Qed. Theorem inj_minus1 : forall n m:nat, (m <= n)%nat -> Z_of_nat (n - m) = Z_of_nat n - Z_of_nat m. Proof. - intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *; - rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus; - rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r; - trivial with arith. + intros n m H. + apply (Zplus_reg_l (Z_of_nat m)); unfold Zminus. + rewrite Zplus_permute, Zplus_opp_r, <- inj_plus, Zplus_0_r. + f_equal. symmetry. now apply le_plus_minus. Qed. Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0. Proof. - intros x y H; rewrite not_le_minus_0; - [ trivial with arith | apply gt_not_le; assumption ]. + intros. rewrite not_le_minus_0; auto with arith. Qed. Theorem inj_minus : forall n m:nat, Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m). Proof. - intros. - unfold Zmax. + intros n m. unfold Zmax. destruct (le_lt_dec m n) as [H|H]. - + (* m <= n *) rewrite inj_minus1; trivial. apply inj_le, Zle_minus_le_0 in H. revert H. unfold Zle. case Zcompare_spec; intuition. - + (* n < m *) rewrite inj_minus2; trivial. apply inj_lt, Zlt_gt in H. apply (Zplus_gt_compat_r _ _ (- Z_of_nat m)) in H. @@ -192,59 +174,170 @@ Theorem inj_min : forall n m:nat, Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m). Proof. intros n m. unfold Zmin. rewrite inj_compare. - case nat_compare_spec; intros; f_equal. - subst. apply min_idempotent. - apply min_l. auto with arith. - apply min_r. auto with arith. + case nat_compare_spec; intros; f_equal; subst; auto with arith. Qed. Theorem inj_max : forall n m:nat, Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m). Proof. intros n m. unfold Zmax. rewrite inj_compare. - case nat_compare_spec; intros; f_equal. - subst. apply max_idempotent. - apply max_r. auto with arith. - apply max_l. auto with arith. + case nat_compare_spec; intros; f_equal; subst; auto with arith. Qed. (** Composition of injections **) -Theorem Zpos_eq_Z_of_nat_o_nat_of_P : - forall p:positive, Zpos p = Z_of_nat (nat_of_P p). +Lemma Z_of_nat_of_P : forall p, Z_of_nat (nat_of_P p) = Zpos p. Proof. - intros x; elim x; simpl in |- *; auto. - intros p H; rewrite ZL6. - apply f_equal with (f := Zpos). - apply nat_of_P_inj. - rewrite nat_of_P_o_P_of_succ_nat_eq_succ; unfold nat_of_P in |- *; - simpl in |- *. - rewrite ZL6; auto. - intros p H; unfold nat_of_P in |- *; simpl in |- *. - rewrite ZL6; simpl in |- *. - rewrite inj_plus; repeat rewrite <- H. - rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity. + intros p. destruct (nat_of_P_is_S p) as (n,H). rewrite H. + simpl. f_equal. rewrite <- (nat_of_P_of_succ_nat n) in H. + symmetry. now apply nat_of_P_inj. Qed. -(** Misc *) +(** For compatibility *) +Definition Zpos_eq_Z_of_nat_o_nat_of_P p := eq_sym (Z_of_nat_of_P p). -Theorem intro_Z : - forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. +(******************************************************************) +(** Properties of the injection from N into Z *) + +Lemma Z_of_nat_of_N : forall n, Z_of_nat (nat_of_N n) = Z_of_N n. Proof. - intros x; exists (Z_of_nat x); split; - [ trivial with arith - | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r; - unfold Zle in |- *; elim x; intros; simpl in |- *; - discriminate ]. + intros [|n]. trivial. + simpl. apply Z_of_nat_of_P. Qed. -Lemma Zpos_P_of_succ_nat : forall n:nat, - Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n). +Lemma Z_of_N_of_nat : forall n, Z_of_N (N_of_nat n) = Z_of_nat n. +Proof. + now destruct n. +Qed. + +Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m. +Proof. + intros; f_equal; assumption. +Qed. + +Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m. +Proof. + intros [|n] [|m]; simpl; congruence. +Qed. + +Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m. +Proof. + split; [apply Z_of_N_eq | apply Z_of_N_eq_rev]. +Qed. + +Lemma Z_of_N_compare : forall n m, + Zcompare (Z_of_N n) (Z_of_N m) = Ncompare n m. +Proof. + intros [|n] [|m]; trivial. +Qed. + +Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> Z_of_N n <= Z_of_N m. +Proof. + intros. unfold Zle. now rewrite Z_of_N_compare. +Qed. + +Lemma Z_of_N_le : forall n m, (n<=m)%N -> Z_of_N n <= Z_of_N m. +Proof. + apply Z_of_N_le_iff. +Qed. + +Lemma Z_of_N_le_rev : forall n m, Z_of_N n <= Z_of_N m -> (n<=m)%N. +Proof. + apply Z_of_N_le_iff. +Qed. + +Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> Z_of_N n < Z_of_N m. +Proof. + intros. unfold Zlt. now rewrite Z_of_N_compare. +Qed. + +Lemma Z_of_N_lt : forall n m, (n<m)%N -> Z_of_N n < Z_of_N m. +Proof. + apply Z_of_N_lt_iff. +Qed. + +Lemma Z_of_N_lt_rev : forall n m, Z_of_N n < Z_of_N m -> (n<m)%N. +Proof. + apply Z_of_N_lt_iff. +Qed. + +Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> Z_of_N n >= Z_of_N m. +Proof. + intros. unfold Zge. now rewrite Z_of_N_compare. +Qed. + +Lemma Z_of_N_ge : forall n m, (n>=m)%N -> Z_of_N n >= Z_of_N m. +Proof. + apply Z_of_N_ge_iff. +Qed. + +Lemma Z_of_N_ge_rev : forall n m, Z_of_N n >= Z_of_N m -> (n>=m)%N. +Proof. + apply Z_of_N_ge_iff. +Qed. + +Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> Z_of_N n > Z_of_N m. +Proof. + intros. unfold Zgt. now rewrite Z_of_N_compare. +Qed. + +Lemma Z_of_N_gt : forall n m, (n>m)%N -> Z_of_N n > Z_of_N m. +Proof. + apply Z_of_N_gt_iff. +Qed. + +Lemma Z_of_N_gt_rev : forall n m, Z_of_N n > Z_of_N m -> (n>m)%N. +Proof. + apply Z_of_N_gt_iff. +Qed. + +Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. +Proof. + reflexivity. +Qed. + +Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. +Proof. + now destruct z. +Qed. + +Lemma Z_of_N_le_0 : forall n, 0 <= Z_of_N n. +Proof. + now destruct n. +Qed. + +Lemma Z_of_N_plus : forall n m, Z_of_N (n+m) = Z_of_N n + Z_of_N m. +Proof. + now destruct n, m. +Qed. + +Lemma Z_of_N_mult : forall n m, Z_of_N (n*m) = Z_of_N n * Z_of_N m. +Proof. + now destruct n, m. +Qed. + +Lemma Z_of_N_minus : forall n m, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). +Proof. + intros [|n] [|m]; simpl; trivial. + case Pcompare_spec; intros H. + subst. now rewrite Pminus_mask_diag. + rewrite Pminus_mask_Lt; trivial. + unfold Pminus. + destruct (Pminus_mask_Gt n m (ZC2 _ _ H)) as (q & -> & _); trivial. +Qed. + +Lemma Z_of_N_succ : forall n, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Proof. + intros [|n]; simpl; trivial. now rewrite Zpos_succ_morphism. +Qed. + +Lemma Z_of_N_min : forall n m, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Proof. + intros. unfold Zmin, Nmin. rewrite Z_of_N_compare. now case Ncompare. +Qed. + +Lemma Z_of_N_max : forall n m, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). Proof. - intros. - unfold Z_of_nat. - destruct n. - simpl; auto. - simpl (P_of_succ_nat (S n)). - apply Zpos_succ_morphism. + intros. unfold Zmax, Nmax. rewrite Z_of_N_compare. + case Ncompare_spec; intros; subst; trivial. Qed. diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v index 96d05760b..7121393bc 100644 --- a/theories/ZArith/Zpow_def.v +++ b/theories/ZArith/Zpow_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinInt Zmisc Ring_theory. +Require Import BinInt BinNat Ring_theory. Local Open Scope Z_scope. @@ -49,23 +49,38 @@ Proof. induction p; simpl; intros; rewrite ?IHp, ?Zmult_assoc; trivial. Qed. -(** An alternative Zpower *) +Lemma Zpower_Ppow : forall p q, (Zpos p)^(Zpos q) = Zpos (p^q). +Proof. + intros. unfold Ppow, Zpower, Zpower_pos. + symmetry. now apply iter_pos_swap_gen. +Qed. + +Lemma Zpower_Npow : forall n m, + (Z_of_N n)^(Z_of_N m) = Z_of_N (n^m). +Proof. + intros [|n] [|m]; simpl; trivial. + unfold Zpower_pos. generalize 1. induction m; simpl; trivial. + apply Zpower_Ppow. +Qed. -(** This Zpower_opt is extensionnaly equal to Zpower in ZArith, - but not convertible with it, and quicker : the number of - multiplications is logarithmic instead of linear. +(** An alternative Zpower *) - TODO: We should try someday to replace Zpower with this Zpower_opt. +(** This Zpower_alt is extensionnaly equal to Zpower in ZArith, + but not convertible with it. The number of + multiplications is logarithmic instead of linear, but + these multiplications are bigger. Experimentally, it seems + that Zpower_alt is slightly quicker than Zpower on average, + but can be quite slower on powers of 2. *) -Definition Zpower_opt n m := +Definition Zpower_alt n m := match m with | Z0 => 1 | Zpos p => Piter_op Zmult p n | Zneg p => 0 end. -Infix "^^" := Zpower_opt (at level 30, right associativity) : Z_scope. +Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope. Lemma iter_pos_mult_acc : forall f, (forall x y:Z, (f x)*y = f (x*y)) -> @@ -92,7 +107,7 @@ Qed. Lemma Zpower_equiv : forall a b, a^^b = a^b. Proof. intros a [|p|p]; trivial. - unfold Zpower_opt, Zpower, Zpower_pos. + unfold Zpower_alt, Zpower, Zpower_pos. revert a. induction p; simpl; intros. f_equal. @@ -105,17 +120,22 @@ Proof. now rewrite Zmult_1_r. Qed. -Lemma Zpower_opt_0_r : forall n, n^^0 = 1. +Lemma Zpower_alt_0_r : forall n, n^^0 = 1. Proof. reflexivity. Qed. -Lemma Zpower_opt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b. +Lemma Zpower_alt_succ_r : forall a b, 0<=b -> a^^(Zsucc b) = a * a^^b. Proof. intros a [|b|b] Hb; [ | |now elim Hb]; simpl. now rewrite Zmult_1_r. rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc. Qed. -Lemma Zpower_opt_neg_r : forall a b, b<0 -> a^^b = 0. +Lemma Zpower_alt_neg_r : forall a b, b<0 -> a^^b = 0. Proof. now destruct b. Qed. + +Lemma Zpower_alt_Ppow : forall p q, (Zpos p)^^(Zpos q) = Zpos (p^q). +Proof. + intros. now rewrite Zpower_equiv, Zpower_Ppow. +Qed. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index e08b7ebc3..c021b01a9 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -55,7 +55,7 @@ Proof. rewrite (Zpower_pos_nat z n). rewrite (Zpower_pos_nat z m). rewrite (Zpower_pos_nat z (n + m)). - rewrite (nat_of_P_plus_morphism n m). + rewrite (Pplus_plus n m). apply Zpower_nat_is_exp. Qed. |