diff options
Diffstat (limited to 'theories')
54 files changed, 449 insertions, 451 deletions
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index f002ee427c..dd10c758a5 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -46,7 +46,7 @@ Section Bool_eq_dec. Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - intros. + intros x y. exists (beq x y). constructor. Defined. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index ef78121d63..5eb2a99739 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -18,7 +18,7 @@ Theorem ifdec_left : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ B -> forall x y:C, ifdec H x y = x. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd B; trivial. Qed. @@ -26,7 +26,7 @@ Theorem ifdec_right : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ A -> forall x y:C, ifdec H x y = y. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd A; trivial. Qed. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 7e9087c377..8366e8257e 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -29,13 +29,13 @@ case diff_true_false; trivial with bool. Qed. Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. -intros. +intros A B H. inversion H. assumption. Qed. Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. -intros. +intros A B H. inversion H. assumption. Qed. @@ -45,7 +45,7 @@ destruct 1; auto with bool. Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. -destruct b; intro H. +intros A B b; destruct b; intro H. - left; inversion H; auto with bool. - right; inversion H; auto with bool. Qed. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index aff5008410..418fc88489 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -19,26 +19,26 @@ Definition zerob (n:nat) : bool := | S _ => false end. -Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. +Lemma zerob_true_intro (n : nat) : n = 0 -> zerob n = true. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. #[global] Hint Resolve zerob_true_intro: bool. -Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. +Lemma zerob_true_elim (n : nat) : zerob n = true -> n = 0. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. -Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. +Lemma zerob_false_intro (n : nat) : n <> 0 -> zerob n = false. Proof. destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. #[global] Hint Resolve zerob_false_intro: bool. -Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. +Lemma zerob_false_elim (n : nat) : zerob n = false -> n <> 0. Proof. destruct n; [ inversion 1 | auto with bool ]. Qed. diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index f23cf158ac..82a76e8afd 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9ff18ebe2c..d6a0ae5411 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -567,9 +567,7 @@ Section Normalize. Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m. Proof. - red in H, H0. red in H. - apply (snd (H _ _)). - assumption. + apply (_ : Normalizes R0 R1). assumption. Qed. Lemma flip_atom R : Normalizes R (flip (flip R)). diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index c489d82d0b..561822ef0c 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -352,14 +352,12 @@ Section Binary. Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R. Proof with auto. reduce_goal. - apply H. firstorder. + firstorder. Qed. Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R). Proof. - unfold flip; constructor; unfold flip. - - intros X. apply H. apply symmetry. apply X. - - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption. + firstorder. Qed. End Binary. diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 7169aa673d..cd6765bab9 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -46,7 +46,7 @@ Qed. (** The generic function that should be used to program, together with some useful tactics. *) -Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H). +Definition decide P {H : Decidable P} := @Decidable_witness _ H. Ltac _decide_ P H := let b := fresh "b" in diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index d96bd72561..4d9069b4d0 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. now transitivity y. Qed. -Arguments equiv_symmetric {A R} sa x y. -Arguments equiv_transitive {A R} sa x y z. +Arguments equiv_symmetric {A R} sa x y : rename. +Arguments equiv_transitive {A R} sa x y z : rename. (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *) diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index d597c0404a..5fe2cade3b 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of FSet Propositions *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 115c7cb365..d6277b3bb5 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -3327,7 +3327,7 @@ Ltac invlist f := (** * Exporting hints and tactics *) -Hint Rewrite +Global Hint Rewrite rev_involutive (* rev (rev l) = l *) rev_unit (* rev (l ++ a :: nil) = a :: rev l *) map_nth (* nth n (map f l) (f d) = f (nth n l d) *) diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index e9d434b488..ae1d978bfb 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -16,7 +16,7 @@ Lemma equal_f : forall {A B : Type} {f g : A -> B}, f = g -> forall x, f x = g x. Proof. - intros. + intros A B f g H x. rewrite H. auto. Qed. @@ -118,7 +118,7 @@ Definition f_equal__functional_extensionality_dep_good {A B f g} H a : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a. Proof. - apply forall_eq_rect with (H := H); clear H g. + apply (fun P k => forall_eq_rect _ P k _ H); clear H g. change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)). apply f_equal, functional_extensionality_dep_good_refl. Defined. diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 7ee3a99d60..21eed3a696 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. Register JMeq_hom as core.JMeq.hom. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. -Proof. -intros; destruct H; trivial. +Proof. +intros A B x y H; destruct H; trivial. Qed. #[global] @@ -150,7 +150,7 @@ Lemma JMeq_eq_dep : forall U (P:U->Type) p q (x:P p) (y:P q), p = q -> JMeq x y -> eq_dep U P p x q y. Proof. -intros. +intros U P p q x y H H0. destruct H. apply JMeq_eq in H0 as ->. reflexivity. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index aa0c419f0e..579e5e9630 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -489,7 +489,7 @@ the above form: variables. We are going to use them with [autorewrite]. *) - Hint Rewrite + Global Hint Rewrite F.empty_iff F.singleton_iff F.add_iff F.remove_iff F.union_iff F.inter_iff F.diff_iff : set_simpl. @@ -499,7 +499,7 @@ the above form: now split. Qed. - Hint Rewrite eq_refl_iff : set_eq_simpl. + Global Hint Rewrite eq_refl_iff : set_eq_simpl. (** ** Decidability of MSet Propositions *) diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f80929e320..2d210e24a6 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -651,7 +651,7 @@ Proof. destruct (rbal'_match l x r); ok. Qed. -Hint Rewrite In_node_iff In_leaf_iff +Global Hint Rewrite In_node_iff In_leaf_iff makeRed_spec makeBlack_spec lbal_spec rbal_spec rbal'_spec : rb. Ltac descolor := destruct_all Color.t. @@ -670,7 +670,7 @@ Proof. - descolor; autorew; rewrite IHl; intuition_in. - descolor; autorew; rewrite IHr; intuition_in. Qed. -Hint Rewrite ins_spec : rb. +Global Hint Rewrite ins_spec : rb. Instance ins_ok s x `{Ok s} : Ok (ins x s). Proof. @@ -685,7 +685,7 @@ Proof. unfold add. now autorew. Qed. -Hint Rewrite add_spec' : rb. +Global Hint Rewrite add_spec' : rb. Lemma add_spec s x y `{Ok s} : InT y (add x s) <-> X.eq y x \/ InT y s. @@ -754,7 +754,7 @@ Proof. * ok. apply lbal_ok; ok. Qed. -Hint Rewrite lbalS_spec rbalS_spec : rb. +Global Hint Rewrite lbalS_spec rbalS_spec : rb. (** ** Append for deletion *) @@ -807,7 +807,7 @@ Proof. [intros a y b | intros t Ht]; autorew; tauto. Qed. -Hint Rewrite append_spec : rb. +Global Hint Rewrite append_spec : rb. Lemma append_ok : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r). @@ -861,7 +861,7 @@ induct s x. rewrite ?IHr by trivial; intuition_in; order. Qed. -Hint Rewrite del_spec : rb. +Global Hint Rewrite del_spec : rb. Instance del_ok s x `{Ok s} : Ok (del x s). Proof. @@ -882,7 +882,7 @@ Proof. unfold remove. now autorew. Qed. -Hint Rewrite remove_spec : rb. +Global Hint Rewrite remove_spec : rb. Instance remove_ok s x `{Ok s} : Ok (remove x s). Proof. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 48df5fe884..420c17c9a4 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -127,7 +127,7 @@ Qed. End N2Nat. -Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double +Global Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min N2Nat.id @@ -147,7 +147,7 @@ Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Hint Rewrite id : Nnat. +Global Hint Rewrite id : Nnat. Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. (** [N.of_nat] is hence injective *) @@ -206,7 +206,7 @@ Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. -Hint Rewrite Nat2N.id : Nnat. +Global Hint Rewrite Nat2N.id : Nnat. (** Compatibility notations *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index e3e8f532b3..374af6de63 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -348,7 +348,7 @@ Local Notation "- x" := (ZnZ.opp x). Local Infix "*" := ZnZ.mul. Local Notation wB := (base ZnZ.digits). -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_opp ZnZ.spec_sub : cyclic. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 7c5b43096a..f74a78e876 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -51,7 +51,7 @@ Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul. -Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred +Global Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic. Ltac zify := unfold eq, zero, one, two, succ, pred, add, sub, mul in *; diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index c469a49903..7bb725538b 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -226,7 +226,7 @@ Proof. apply Z.lt_le_trans with (1:= H5); auto with zarith. apply Zpower_le_monotone; auto with zarith. rewrite Zplus_mod; auto with zarith. - rewrite -> Zmod_small with (a := t); auto with zarith. + rewrite -> (Zmod_small t); auto with zarith. apply Zmod_small; auto with zarith. split; auto with zarith. assert (0 <= 2 ^a * r); auto with zarith. @@ -489,15 +489,15 @@ Definition cast i j := Lemma cast_refl : forall i, cast i i = Some (fun P H => H). Proof. - unfold cast;intros. + unfold cast;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma cast_diff : forall i j, i =? j = false -> cast i j = None. Proof. - intros;unfold cast;intros; generalize (eqb_correct i j). + intros i j H;unfold cast;intros; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -509,15 +509,15 @@ Definition eqo i j := Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i). Proof. - unfold eqo;intros. + unfold eqo;intros i. generalize (eqb_correct i i). - rewrite eqb_refl;intros. + rewrite eqb_refl;intros e. rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial. Qed. Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None. Proof. - unfold eqo;intros; generalize (eqb_correct i j). + unfold eqo;intros i j H; generalize (eqb_correct i j). rewrite H;trivial. Qed. @@ -651,7 +651,7 @@ Proof. apply Zgcdn_is_gcd. unfold Zgcd_bound. generalize (to_Z_bounded b). - destruct φ b. + destruct φ b as [|p|p]. unfold size; auto with zarith. intros (_,H). cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto]. @@ -727,7 +727,7 @@ Proof. replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z. rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith. rewrite !Zmod_small; auto with zarith. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. case_eq (n <=? m + n)%int63; auto. rewrite leb_spec, H1; auto with zarith. assert (H1: (φ (m + n) = φ m + φ n)%Z). @@ -805,7 +805,7 @@ Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63. Proof. apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l. rewrite -> !lsl_spec, <-Zplus_mod. - apply f_equal2 with (f := Zmod); auto with zarith. + apply (f_equal2 Zmod); auto with zarith. Qed. Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63. @@ -954,6 +954,7 @@ Proof. intros _ HH; generalize (HH H1); discriminate. clear H. generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. + change 62%int63 with (digits - 1)%int63. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. @@ -973,14 +974,14 @@ Proof. case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2. 2: generalize (H3 F2); discriminate. clear H2 H3. - apply f_equal with (f := negb). - apply f_equal with (f := is_zero). + apply (f_equal negb). + apply (f_equal is_zero). apply to_Z_inj. rewrite -> !lsl_spec, !lsr_spec, !lsl_spec. pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto. rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith. rewrite !Zmult_mod_distr_r. - apply f_equal2 with (f := Zmult); auto. + apply (f_equal2 Zmult); auto. replace wB with (2^ d); auto with zarith. replace d with ((d - φ i) + φ i)%Z by ring. case (to_Z_bounded i); intros H1i H2i. @@ -1078,8 +1079,8 @@ Proof. 2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto. rewrite lsl_add_distr. rewrite (bit_split x) at 1; rewrite (bit_split y) at 1. - rewrite <-!add_assoc; apply f_equal2 with (f := add); auto. - rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto. + rewrite <-!add_assoc; apply (f_equal2 add); auto. + rewrite add_comm, <-!add_assoc; apply (f_equal2 add); auto. rewrite add_comm; auto. intros Heq. generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb. @@ -1360,7 +1361,7 @@ Lemma sqrt2_step_def rec ih il j: else j else j. Proof. - unfold sqrt2_step; case diveucl_21; intros;simpl. + unfold sqrt2_step; case diveucl_21; intros i j';simpl. case (j +c i);trivial. Qed. @@ -1390,7 +1391,7 @@ Proof. assert (W1:= to_Z_bounded a1). assert (W2:= to_Z_bounded a2). assert (Wb:= to_Z_bounded b). - assert (φ b>0) by (auto with zarith). + assert (φ b>0) as H by (auto with zarith). generalize (Z_div_mod (φ a1*wB+φ a2) φ b H). revert W. destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b). diff --git a/theories/Numbers/DecimalPos.v b/theories/Numbers/DecimalPos.v index 5611329b12..f86246d3c2 100644 --- a/theories/Numbers/DecimalPos.v +++ b/theories/Numbers/DecimalPos.v @@ -216,7 +216,7 @@ Proof. - trivial. - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). rewrite N.mul_succ_r. - change 10 at 2 with (Nat.iter 10%nat N.succ 0). + change 10 with (Nat.iter 10%nat N.succ 0) at 2. rewrite ?nat_iter_S, nat_iter_0. rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. destruct (to_lu (N.pos p)); simpl; auto. diff --git a/theories/Numbers/HexadecimalNat.v b/theories/Numbers/HexadecimalNat.v index 94a14b90bd..696e89bd8e 100644 --- a/theories/Numbers/HexadecimalNat.v +++ b/theories/Numbers/HexadecimalNat.v @@ -230,7 +230,7 @@ Proof. simpl_of_lu; rewrite ?Nat.add_succ_l, Nat.add_0_l, ?to_lu_succ, to_of_lu_sixteenfold by assumption; - unfold lnorm; simpl; now destruct nztail. + unfold lnorm; cbn; now destruct nztail. Qed. (** Second bijection result *) diff --git a/theories/Numbers/HexadecimalPos.v b/theories/Numbers/HexadecimalPos.v index 47f6d983b7..29029cb839 100644 --- a/theories/Numbers/HexadecimalPos.v +++ b/theories/Numbers/HexadecimalPos.v @@ -235,7 +235,7 @@ Proof. - trivial. - change (N.pos (Pos.succ p)) with (N.succ (N.pos p)). rewrite N.mul_succ_r. - change 0x10 at 2 with (Nat.iter 0x10%nat N.succ 0). + change 0x10 with (Nat.iter 0x10%nat N.succ 0) at 2. rewrite ?nat_iter_S, nat_iter_0. rewrite !N.add_succ_r, N.add_0_r, !to_lu_succ, IHp. destruct (to_lu (N.pos p)); simpl; auto. diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 0c097b6773..9d9244eefb 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -18,7 +18,7 @@ Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) -Hint Rewrite opp_0 : nz. +Global Hint Rewrite opp_0 : nz. Theorem add_pred_l n m : P n + m == P (n + m). Proof. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4d2361689d..832931e5ef 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -26,7 +26,7 @@ Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. Ltac order_pos' := try apply abs_nonneg; order_pos. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -566,7 +566,7 @@ Tactic Notation "bitwise" "as" simple_intropattern(m) simple_intropattern(Hm) Ltac bitwise := bitwise as ?m ?Hm. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. (** The streams of bits that correspond to a numbers are exactly the ones which are stationary after some point. *) diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 66cbba9e08..2ad8dfcedb 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -14,9 +14,9 @@ Require Import NZAxioms NZBase. Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ). -Hint Rewrite +Global Hint Rewrite pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz. -Hint Rewrite one_succ two_succ : nz'. +Global Hint Rewrite one_succ two_succ : nz'. Ltac nzsimpl := autorewrite with nz. Ltac nzsimpl' := autorewrite with nz nz'. @@ -39,7 +39,7 @@ Proof. intros n m. now rewrite add_succ_r, add_succ_l. Qed. -Hint Rewrite add_0_r add_succ_r : nz. +Global Hint Rewrite add_0_r add_succ_r : nz. Theorem add_comm : forall n m, n + m == m + n. Proof. @@ -58,7 +58,7 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite add_1_l add_1_r : nz. +Global Hint Rewrite add_1_l add_1_r : nz. Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. @@ -104,6 +104,6 @@ Proof. intro n; now nzsimpl'. Qed. -Hint Rewrite sub_1_r : nz. +Global Hint Rewrite sub_1_r : nz. End NZAddProp. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 3d6465191d..14728eaf40 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -28,7 +28,7 @@ Proof. now rewrite add_cancel_r. Qed. -Hint Rewrite mul_0_r mul_succ_r : nz. +Global Hint Rewrite mul_0_r mul_succ_r : nz. Theorem mul_comm : forall n m, n * m == m * n. Proof. @@ -69,7 +69,7 @@ Proof. intro n. now nzsimpl'. Qed. -Hint Rewrite mul_1_l mul_1_r : nz. +Global Hint Rewrite mul_1_l mul_1_r : nz. Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m. Proof. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 3b2a496229..00edcd641f 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -45,7 +45,7 @@ Module Type NZPowProp (Import B : NZPow' A) (Import C : NZMulOrderProp A). -Hint Rewrite pow_0_r pow_succ_r : nz. +Global Hint Rewrite pow_0_r pow_succ_r : nz. (** Power and basic constants *) @@ -76,14 +76,14 @@ Proof. - now nzsimpl. Qed. -Hint Rewrite pow_1_r pow_1_l : nz. +Global Hint Rewrite pow_1_r pow_1_l : nz. Lemma pow_2_r : forall a, a^2 == a*a. Proof. intros. rewrite two_succ. nzsimpl; order'. Qed. -Hint Rewrite pow_2_r : nz. +Global Hint Rewrite pow_2_r : nz. (** Power and nullity *) diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index 313b9adfd1..427a18d4ae 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -23,7 +23,7 @@ Module Type NBitsProp Include BoolEqualityFacts A. Ltac order_nz := try apply pow_nonzero; order'. -Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. +Global Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. (** Some properties of power and division *) @@ -368,7 +368,7 @@ Proof. split. apply bits_inj. intros EQ; now rewrite EQ. Qed. -Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. +Global Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. Tactic Notation "bitwise" "as" simple_intropattern(m) := apply bits_inj; intros m; autorewrite with bitwise. diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index e97f2dc748..7d50bdacad 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -876,7 +876,7 @@ Lemma compare_xO_xI p q : (p~0 ?= q~1) = switch_Eq Lt (p ?= q). Proof. exact (compare_cont_spec p q Lt). Qed. -Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. +Global Hint Rewrite compare_xO_xO compare_xI_xI compare_xI_xO compare_xO_xI : compare. Ltac simpl_compare := autorewrite with compare. Ltac simpl_compare_in H := autorewrite with compare in H. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 8813131d7b..18e55aefc6 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -40,8 +40,8 @@ Proof. reflexivity. Qed. -Hint Rewrite @compose_id_left @compose_id_right : core. -Hint Rewrite <- @compose_assoc : core. +Global Hint Rewrite @compose_id_left @compose_id_right : core. +Global Hint Rewrite <- @compose_assoc : core. (** [flip] is involutive. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 25af2d5ffb..090322054e 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -162,7 +162,7 @@ Ltac pi_eq_proofs := repeat pi_eq_proof. Ltac clear_eq_proofs := abstract_eq_proofs ; pi_eq_proofs. -Hint Rewrite <- eq_rect_eq : refl_id. +Global Hint Rewrite <- eq_rect_eq : refl_id. (** The [refl_id] database should be populated with lemmas of the form [coerce_* t eq_refl = t]. *) @@ -178,7 +178,7 @@ Lemma inj_pairT2_refl A (x : A) (P : A -> Type) (p : P x) : Eqdep.EqdepTheory.inj_pairT2 A P x p p eq_refl = eq_refl. Proof. apply UIP_refl. Qed. -Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. +Global Hint Rewrite @JMeq_eq_refl @UIP_refl_refl @inj_pairT2_refl : refl_id. Ltac rewrite_refl_id := autorewrite with refl_id. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index fce69437d7..d852ad24fe 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -319,7 +319,3 @@ Create HintDb program discriminated. Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. - -Definition obligation (A : Type) {a : A} := a. - -Register obligation as program.tactics.obligation. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d1be8812e9..69873d0321 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -43,7 +43,7 @@ Section Well_founded. forall (x:A) (r:Acc R x), F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r. Proof. - destruct r using Acc_inv_dep; auto. + intros x r; destruct r using Acc_inv_dep; auto. Qed. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s. @@ -95,12 +95,12 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - + intros. + + intros H a. apply (H (m a))... + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. + intros ? H ? H0. apply Acc_intro. - intros. + intros y H1. unfold MR in H1. rewrite H0 in H1. apply (H (m y))... @@ -174,7 +174,7 @@ Section Fix_rects. revert a'. pattern x, (Fix_F_sub A R P f x a). apply Fix_F_sub_rect. - intros. + intros ? H **. rewrite F_unfold. apply equiv_lowers. intros. @@ -197,11 +197,11 @@ Section Fix_rects. : forall x, Q _ (Fix_sub A R Rwf P f x). Proof with auto. unfold Fix_sub. - intros. + intros x. apply Fix_F_sub_rect. - intros. - assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))... - set (inv x0 X0 a). clearbody q. + intros x0 H a. + assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0... + set (q := inv x0 X0 a). clearbody q. rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))... @@ -242,9 +242,9 @@ Module WfExtensionality. Fix_sub A R Rwf P F_sub x = F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)). Proof. - intros ; apply Fix_eq ; auto. - intros. - assert(f = g). + intros A R Rwf P F_sub x; apply Fix_eq ; auto. + intros ? f g H. + assert(f = g) as H0. - extensionality y ; apply H. - rewrite H0 ; auto. Qed. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index b008c6c2aa..4e596a165c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -637,13 +637,13 @@ Qed. Lemma Qmult_1_l : forall n, 1*n == n. Proof. - intro; red; simpl; destruct (Qnum n); auto. + intro n; red; simpl; destruct (Qnum n); auto. Qed. Theorem Qmult_1_r : forall n, n*1==n. Proof. - intro; red; simpl. - rewrite Z.mul_1_r with (n := Qnum n). + intro n; red; simpl. + rewrite (Z.mul_1_r (Qnum n)). rewrite Pos.mul_comm; simpl; trivial. Qed. @@ -709,7 +709,7 @@ Qed. Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1. Proof. intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl; - intros; simpl_mult; try ring. + intros H **; simpl_mult; try ring. elim H; auto. Qed. @@ -722,7 +722,7 @@ Qed. Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x. Proof. - intros; unfold Qdiv. + intros x y H; unfold Qdiv. rewrite <- (Qmult_assoc x y (Qinv y)). rewrite (Qmult_inv_r y H). apply Qmult_1_r. @@ -730,7 +730,7 @@ Qed. Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x. Proof. - intros; unfold Qdiv. + intros x y ?; unfold Qdiv. rewrite (Qmult_assoc y x (Qinv y)). rewrite (Qmult_comm y x). fold (Qdiv (Qmult x y) y). @@ -845,7 +845,7 @@ Qed. Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z. Proof. - intros. + intros x y z ? ?. apply Qle_lt_trans with y; auto. apply Qlt_le_weak; auto. Qed. @@ -877,19 +877,19 @@ Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}. Proof. - unfold Qlt, Qle, Qeq; intros. + unfold Qlt, Qle, Qeq; intros x y. exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}. Proof. - unfold Qlt, Qle; intros. + unfold Qlt, Qle; intros x y. exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined. Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }. Proof. - intros. destruct q as [a b]. destruct a. + intros q. destruct q as [a b]. destruct a as [|p|p]. - exists xH. reflexivity. - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))). simpl. rewrite Pos.mul_1_r. @@ -1169,12 +1169,12 @@ Qed. Lemma Qinv_lt_contravar : forall a b : Q, 0 < a -> 0 < b -> (a < b <-> /b < /a). Proof. - intros. split. - - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. + intros a b H H0. split. + - intro H1. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0. rewrite <- (Qmult_inv_r a). rewrite Qmult_comm. apply Qmult_lt_l. apply Qinv_lt_0_compat. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). - - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). + - intro H1. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)). apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0. rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H. apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H). @@ -1190,7 +1190,7 @@ Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive. Proof. intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy. unfold Qpower_positive. -induction y; simpl; +induction y as [y IHy|y IHy|]; simpl; try rewrite IHy; try rewrite Hx; reflexivity. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5a23a20811..620ed6b5b7 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -180,4 +180,4 @@ intros; rewrite Q2R_mult. rewrite Q2R_inv; auto. Qed. -Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. +Global Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 533c675415..e94ae1e789 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -129,19 +129,19 @@ Qed. Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp. Proof. - intros; unfold Qplus'. + intros ? ? H ? ? H0; unfold Qplus'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp. Proof. - intros; unfold Qmult'. + intros ? ? H ? ? H0; unfold Qmult'. rewrite H, H0; auto with qarith. Qed. Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp. Proof. - intros; unfold Qminus'. + intros ? ? H ? ? H0; unfold Qminus'. rewrite H, H0; auto with qarith. Qed. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index 60fad8795a..5a599587d0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -285,14 +285,14 @@ Lemma CRlt_trans : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. apply (CRlt_le_trans _ y _ H). apply CRlt_asym. exact H0. -Defined. +Qed. Lemma CRlt_trans_flip : forall {R : ConstructiveReals} (x y z : CRcarrier R), y < z -> x < y -> x < z. Proof. intros. apply (CRlt_le_trans _ y). exact H0. apply CRlt_asym. exact H. -Defined. +Qed. Lemma CReq_refl : forall {R : ConstructiveReals} (x : CRcarrier R), x == x. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index 53b5aca38c..6ed5845440 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -232,7 +232,7 @@ Proof. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. -Defined. +Qed. Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Q), Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 069a1292cd..9a00408de3 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -112,7 +112,7 @@ Proof. pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H | apply H1 ]. -Defined. +Qed. Lemma Alembert_C2 : forall An:nat -> R, @@ -330,7 +330,7 @@ Proof. rewrite <- Rabs_Ropp; apply RRle_abs. rewrite double; pattern (Rabs (An n)) at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; apply Rabs_pos_lt; apply H. -Defined. +Qed. Lemma AlembertC3_step1 : forall (An:nat -> R) (x:R), @@ -374,7 +374,7 @@ Proof. [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ]. intro; unfold Bn; apply prod_neq_R0; [ apply H0 | apply pow_nonzero; assumption ]. -Defined. +Qed. Lemma AlembertC3_step2 : forall (An:nat -> R) (x:R), x = 0 -> { l:R | Pser An x l }. @@ -405,7 +405,7 @@ Proof. cut (x <> 0). intro; apply AlembertC3_step1; assumption. red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). -Defined. +Qed. Lemma Alembert_C4 : forall (An:nat -> R) (k:R), diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 8a11c155ce..4fb3846abc 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -320,7 +320,6 @@ Proof. - contradiction. - exact Hxltz. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_lt_le_trans : forall x y z : CReal, x < y -> y <= z -> x < z. @@ -330,7 +329,6 @@ Proof. - exact Hxltz. - contradiction. Qed. -(* Todo: this was Defined. Why *) Lemma CReal_le_trans : forall x y z : CReal, x <= y -> y <= z -> x <= z. @@ -347,7 +345,6 @@ Proof. apply (CReal_lt_le_trans _ y _ Hxlty). apply CRealLt_asym; exact Hyltz. Qed. -(* Todo: this was Defined. Why *) Lemma CRealEq_trans : forall x y z : CReal, CRealEq x y -> CRealEq y z -> CRealEq x z. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index a180e13444..bc45868244 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -733,13 +733,11 @@ Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal := bound := CReal_inv_pos_bound x Hxpos |}. -(* ToDo: make this more obviously computing *) - Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. intros x [n nmaj]. exists n. - apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl. - unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. + simpl in *. unfold CReal_opp_seq, Qminus. + abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)). Defined. Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 70d2861d17..c2b60e6478 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -75,7 +75,7 @@ Proof. rewrite inject_Q_plus, (opp_inject_Q 2). ring_simplify. exact H. rewrite Qinv_plus_distr. reflexivity. -Defined. +Qed. (* ToDo: Move to ConstructiveCauchyAbs.v *) Lemma Qabs_Rabs : forall q : Q, @@ -688,21 +688,7 @@ Proof. exact (a i j H0 H1). exists l. intros p. destruct (cv p). exists x. exact c. -Defined. - -(* ToDO: Belongs into sumbool.v *) -Section connectives. - - Variables A B : Prop. - - Hypothesis H1 : {A} + {~A}. - Hypothesis H2 : {B} + {~B}. - - Definition sumbool_or_not_or : {A \/ B} + {~(A \/ B)}. - case H1; case H2; tauto. - Defined. - -End connectives. +Qed. Lemma Qnot_le_iff_lt: forall x y : Q, ~ (x <= y)%Q <-> (y < x)%Q. @@ -740,13 +726,11 @@ Proof. clear maj. right. exists n. apply H0. - clear H0 H. intro n. - apply sumbool_or_not_or. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. - + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q). - * left; assumption. - * right; apply Qle_not_lt; assumption. + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq b n - seq a n)%Q) as [H1|H1]. + + now left; left. + + destruct (Qlt_le_dec (2 * 2 ^ n)%Q (seq d n - seq c n)%Q) as [H2|H2]. + * now left; right. + * now right; intros [H3|H3]; apply Qle_not_lt with (2 := H3). Qed. Definition CRealConstructive : ConstructiveReals diff --git a/theories/Reals/ClassicalDedekindReals.v b/theories/Reals/ClassicalDedekindReals.v index 500838ed26..0736b09761 100644 --- a/theories/Reals/ClassicalDedekindReals.v +++ b/theories/Reals/ClassicalDedekindReals.v @@ -233,17 +233,12 @@ Qed. (** *** Conversion from CReal to DReal *) -Definition DRealAbstr : CReal -> DReal. +Lemma DRealAbstr_aux : + forall x H, + isLowerCut (fun q : Q => + if sig_forall_dec (fun n : nat => seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n)) (H q) + then true else false). Proof. - intro x. - assert (forall (q : Q) (n : nat), - {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + - {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). - { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). - right. apply (Qlt_not_le _ _ q0). left. exact q0. } - - exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) - then true else false). repeat split. - intros. destruct (sig_forall_dec (fun n : nat => (seq x (-Z.of_nat n) <= q + (2^-Z.of_nat n))%Q) @@ -303,6 +298,20 @@ Proof. apply (Qmult_le_l _ _ 2) in q0. field_simplify in q0. apply (Qplus_le_l _ _ (-seq x (-Z.of_nat n))) in q0. ring_simplify in q0. contradiction. reflexivity. +Qed. + +Definition DRealAbstr : CReal -> DReal. +Proof. + intro x. + assert (forall (q : Q) (n : nat), + {(fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n} + + {~ (fun n0 : nat => (seq x (-Z.of_nat n0) <= q + (2^-Z.of_nat n0))%Q) n}). + { intros. destruct (Qlt_le_dec (q + (2^-Z.of_nat n)) (seq x (-Z.of_nat n))). + right. apply (Qlt_not_le _ _ q0). left. exact q0. } + + exists (fun q:Q => if sig_forall_dec (fun n:nat => Qle (seq x (-Z.of_nat n)) (q + (2^-Z.of_nat n))) (H q) + then true else false). + apply DRealAbstr_aux. Defined. (** *** Conversion from DReal to CReal *) diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 6692119738..6107775003 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -170,7 +170,7 @@ Proof. reg. exists H5; symmetry ; reg; rewrite <- H3; rewrite <- H4; reflexivity. assumption. -Defined. +Qed. (**********) Lemma antiderivative_P1 : diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index ef09188c33..8b78f73d2e 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -128,19 +128,37 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)). Qed. -Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x. -Proof. - intros; apply Rplus_lt_reg_l with (- exp 0); rewrite <- (Rplus_comm (exp x)); - assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0; - intros; elim H1; intros; unfold Rminus in H2; rewrite H2; - rewrite Ropp_0; rewrite Rplus_0_r; - replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). - rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; - pattern x at 1; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0)); - apply Rmult_lt_compat_l. - apply H. - rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption. - symmetry ; apply derive_pt_eq_0; apply derivable_pt_lim_exp. +Lemma exp_ineq1 : forall x : R, x <> 0 -> 1 + x < exp x. +Proof. + assert (Hd : forall c : R, + derivable_pt_lim (fun x : R => exp x - (x + 1)) c (exp c - 1)). + intros. + apply derivable_pt_lim_minus; [apply derivable_pt_lim_exp | ]. + replace (1) with (1 + 0) at 1 by lra. + apply derivable_pt_lim_plus; + [apply derivable_pt_lim_id | apply derivable_pt_lim_const]. + intros x xdz; destruct (Rtotal_order x 0) as [xlz|[xez|xgz]]. + - destruct (MVT_cor2 _ _ x 0 xlz (fun c _ => Hd c)) as [c [HH1 HH2]]. + rewrite exp_0 in HH1. + assert (H1 : 0 < x * exp c - x); [| lra]. + assert (H2 : x * exp 0 < x * exp c); [| rewrite exp_0 in H2; lra]. + apply Rmult_lt_gt_compat_neg_l; auto. + now apply exp_increasing. + - now case xdz. + - destruct (MVT_cor2 _ _ 0 x xgz (fun c _ => Hd c)) as [c [HH1 HH2]]. + rewrite exp_0 in HH1. + assert (H1 : 0 < x * exp c - x); [| lra]. + assert (H2 : x * exp 0 < x * exp c); [| rewrite exp_0 in H2; lra]. + apply Rmult_lt_compat_l; auto. + now apply exp_increasing. +Qed. + +Lemma exp_ineq1_le (x : R) : 1 + x <= exp x. +Proof. + destruct (Req_EM_T x 0) as [xeq|?]. + - rewrite xeq, exp_0; lra. + - left. + now apply exp_ineq1. Qed. Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }. @@ -159,7 +177,7 @@ Proof. unfold f; apply Rplus_le_reg_l with y; left; apply Rlt_trans with (1 + y). rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1. - replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ]. + replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y); lra | ring ]. unfold f; change (continuity (exp - fct_cte y)); apply continuity_minus; [ apply derivable_continuous; apply derivable_exp diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 7f5a859c81..2004f40f00 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -41,9 +41,13 @@ Proof. red; intro; rewrite H0 in H; elim (lt_irrefl _ H). Qed. -Lemma exist_exp0 : { l:R | exp_in 0 l }. +(* Value of [exp 0] *) +Lemma exp_0 : exp 0 = 1. Proof. - exists 1. + cut (exp_in 0 1). + cut (exp_in 0 (exp 0)). + apply uniqueness_sum. + exact (proj2_sig (exist_exp 0)). unfold exp_in; unfold infinite_sum; intros. exists 0%nat. intros; replace (sum_f_R0 (fun i:nat => / INR (fact i) * 0 ^ i) n) with 1. @@ -56,18 +60,6 @@ Proof. simpl. ring. unfold ge; apply le_O_n. -Defined. - -(* Value of [exp 0] *) -Lemma exp_0 : exp 0 = 1. -Proof. - cut (exp_in 0 (exp 0)). - cut (exp_in 0 1). - unfold exp_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_exp0). - exact (proj2_sig (exist_exp 0)). Qed. (*****************************************) @@ -384,9 +376,14 @@ Proof. intros; ring. Qed. -Lemma exist_cos0 : { l:R | cos_in 0 l }. +(* Value of [cos 0] *) +Lemma cos_0 : cos 0 = 1. Proof. - exists 1. + cut (cos_in 0 1). + cut (cos_in 0 (cos 0)). + apply uniqueness_sum. + rewrite <- Rsqr_0 at 1. + exact (proj2_sig (exist_cos (Rsqr 0))). unfold cos_in; unfold infinite_sum; intros; exists 0%nat. intros. unfold R_dist. @@ -400,17 +397,4 @@ Proof. rewrite Rplus_0_r. apply Hrecn; unfold ge; apply le_O_n. simpl; ring. -Defined. - -(* Value of [cos 0] *) -Lemma cos_0 : cos 0 = 1. -Proof. - cut (cos_in 0 (cos 0)). - cut (cos_in 0 1). - unfold cos_in; intros; eapply uniqueness_sum. - apply H0. - apply H. - exact (proj2_sig exist_cos0). - assert (H := proj2_sig (exist_cos (Rsqr 0))); unfold cos; - pattern 0 at 1; replace 0 with (Rsqr 0); [ exact H | apply Rsqr_0 ]. Qed. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 4ac54d280a..c3e67b9d5a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -53,7 +53,7 @@ Module Type CompareFacts (Import O:DecStrOrder'). rewrite compare_gt_iff; intuition. Qed. - Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. + Global Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order. Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare. Proof. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index abf7f681b0..c709149109 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -146,7 +146,7 @@ Module MoreInt (Import I:Int). (** A magic (but costly) tactic that goes from [int] back to the [Z] friendly world ... *) - Hint Rewrite -> + Global Hint Rewrite -> i2z_0 i2z_1 i2z_2 i2z_3 i2z_add i2z_opp i2z_sub i2z_mul i2z_max i2z_eqb i2z_ltb i2z_leb : i2z. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 9a1bbca99f..c11077607e 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -58,9 +58,9 @@ Open Scope Z_scope. Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b. Proof. - induction n. + intros n; induction n. simpl; auto with zarith. - destruct a; simpl; intros; auto with zarith; auto. + intros a; destruct a; simpl; intros; auto with zarith; auto. Qed. Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b. @@ -75,9 +75,9 @@ Open Scope Z_scope. Lemma Zgcdn_linear_bound : forall n a b, Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. - induction n. + intros n; induction n as [|n IHn]. intros; lia. - destruct a; intros; simpl; + intros a; destruct a as [|p|p]; intros b H; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; generalize (Z_div_mod b (Zpos p) (eq_refl Gt)); @@ -106,7 +106,7 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. - induction N. intros; lia. + intros N; induction N as [|N IHN]. intros; lia. intros [ | [ | n ] ]. 1-2: simpl; lia. intros. change (0 <= fibonacci (S n) + fibonacci n). @@ -116,11 +116,11 @@ Open Scope Z_scope. Lemma fibonacci_incr : forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m. Proof. - induction 1. + induction 1 as [|m H IH]. auto with zarith. apply Z.le_trans with (fibonacci m); auto. clear. - destruct m. + destruct m as [|m]. simpl; auto with zarith. change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). generalize (fibonacci_pos m); lia. @@ -137,10 +137,10 @@ Open Scope Z_scope. fibonacci (S n) <= a /\ fibonacci (S (S n)) <= b. Proof. - induction n. + intros n; induction n as [|n IHn]. intros [|a|a]; intros; simpl; lia. intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. - remember (S n) as m. + remember (S n) as m eqn:Heqm. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). destruct (Z.div_eucl b (Zpos a)) as (q,r). @@ -171,19 +171,19 @@ Open Scope Z_scope. 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a. 1,3 : intros; lia. + intros n a; destruct a as [|p|p]. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)). destruct 2; eauto. - clear n; induction k. + clear n; intros k; induction k as [|k IHk]. intros. apply Zgcdn_linear_bound. lia. - intros. - generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. - assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). + intros n b H H0 H1. + generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros H2. + assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)) as H3. apply IHk; auto. lia. replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. @@ -197,13 +197,13 @@ Open Scope Z_scope. Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a). Proof. - destruct a; [lia| | intro H; discriminate]. + intros a; destruct a as [|p|p]; [lia| | intro H; discriminate]. intros _. - induction p; [ | | compute; auto ]; + induction p as [p IHp|p IHp|]; [ | | compute; auto ]; simpl Zgcd_bound in *; rewrite plus_comm; simpl plus; set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl; - assert (n <> O) by (unfold n; destruct p; simpl; auto). + assert (n <> O) as H by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. @@ -229,11 +229,11 @@ Open Scope Z_scope. Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat -> Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b). Proof. - intros. + intros H. generalize (Zgcd_bound_fibonacci (Zpos a)). simpl Zgcd_bound in *. - remember (Pos.size_nat a+Pos.size_nat a)%nat as m. - assert (1 < m)%nat. + remember (Pos.size_nat a+Pos.size_nat a)%nat as m eqn:Heqm. + assert (1 < m)%nat as H0. { rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm; auto with arith. } destruct m as [ |m]; [inversion H0; auto| ]. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index b69af424b1..bc3f5706c9 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -83,10 +83,10 @@ Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed. Lemma Zpower2_Psize n p : Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat. Proof. - revert p; induction n. - destruct p; now split. + revert p; induction n as [|n IHn]. + intros p; destruct p; now split. assert (Hn := Nat2Z.is_nonneg n). - destruct p; simpl Pos.size_nat. + intros p; destruct p as [p|p|]; simpl Pos.size_nat. - specialize IHn with p. rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. - specialize IHn with p. @@ -138,7 +138,7 @@ Definition Zpow_mod a m n := Theorem Zpow_mod_pos_correct a m n : n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n. Proof. - intros Hn. induction m. + intros Hn. induction m as [m IHm|m IHm|]. - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag. rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r. rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial. @@ -193,7 +193,7 @@ Proof. assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). lia. - intros n Hn Rec. - rewrite Z.pow_succ_r by trivial. intros. + rewrite Z.pow_succ_r by trivial. intros H. assert (2<=p) by (apply prime_ge_2; auto). assert (2<=q) by (apply prime_ge_2; auto). destruct prime_mult with (2 := H); auto. @@ -229,7 +229,7 @@ Proof. (* x = 1 *) exists 0; rewrite Z.pow_0_r; auto. (* x = 0 *) - exists n; destruct H; rewrite Z.mul_0_r in H; auto. + exists n; destruct H as [? H]; rewrite Z.mul_0_r in H; auto. Qed. (** * Z.square: a direct definition of [z^2] *) diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 6f464d89bb..6b01d798e4 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp : forall (n m:nat) (z:Z), Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m. Proof. - induction n. + intros n; induction n as [|n IHn]. - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l. - intros. simpl. now rewrite IHn, Z.mul_assoc. Qed. @@ -135,7 +135,7 @@ Section Powers_of_2. Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n). Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg. Qed. @@ -164,7 +164,7 @@ Section Powers_of_2. Theorem shift_nat_correct n x : Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x. Proof. - induction n. + induction n as [|n IHn]. - trivial. - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn. Qed. @@ -295,7 +295,7 @@ Section power_div_with_rest. rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc. repeat split; auto. rewrite !Z.mul_1_l, H, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r. now rewrite Z.mul_1_l. - rewrite Pos2Z.neg_xO in H. @@ -303,7 +303,7 @@ Section power_div_with_rest. repeat split; auto. - repeat split; auto. rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc. - apply f_equal2 with (f := Z.add); auto. + apply (f_equal2 Z.add); auto. rewrite Z.add_comm, <- Z.add_diag. rewrite Z.mul_add_distr_l. replace (-1 * d) with (-d). diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 515372466a..e4129f8382 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1371,13 +1371,13 @@ Section S. destruct pol;auto. generalize (is_cnf_tt_inv (xcnf (negb true) f1)). destruct (is_cnf_tt (xcnf (negb true) f1)). - + intros. + + intros H. rewrite H by auto. reflexivity. + generalize (is_cnf_ff_inv (xcnf (negb true) f1)). destruct (is_cnf_ff (xcnf (negb true) f1)). - * intros. + * intros H. rewrite H by auto. unfold or_cnf_opt. simpl. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index 1616b5a2a4..a4b631fc13 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -38,7 +38,7 @@ Ltac inv H := inversion H ; try subst ; clear H. Lemma eq_le_iff : forall x, 0 = x <-> (0 <= x /\ x <= 0). Proof. intros. - split ; intros. + split ; intros H. - subst. compute. intuition congruence. - destruct H. @@ -48,7 +48,7 @@ Qed. Lemma lt_le_iff : forall x, 0 < x <-> 0 <= x - 1. Proof. - split ; intros. + split ; intros H. - apply Zlt_succ_le. ring_simplify. auto. @@ -70,12 +70,13 @@ Lemma le_neg : forall x, Proof. intro. rewrite lt_le_iff. - split ; intros. + split ; intros H. - apply Znot_le_gt in H. apply Zgt_le_succ in H. rewrite le_0_iff in H. ring_simplify in H; auto. - - assert (C := (Z.add_le_mono _ _ _ _ H H0)). + - intro H0. + assert (C := (Z.add_le_mono _ _ _ _ H H0)). ring_simplify in C. compute in C. apply C ; reflexivity. @@ -84,7 +85,7 @@ Qed. Lemma eq_cnf : forall x, (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0. Proof. - intros. + intros x. rewrite Z.eq_sym_iff. rewrite eq_le_iff. rewrite (le_0_iff x 0). @@ -108,7 +109,7 @@ Proof. auto using Z.le_antisymm. eauto using Z.le_trans. apply Z.le_neq. - destruct (Z.lt_trichotomy n m) ; intuition. + apply Z.lt_trichotomy. apply Z.add_le_mono_l; assumption. apply Z.mul_pos_pos ; auto. discriminate. @@ -160,18 +161,18 @@ Fixpoint Zeval_const (e: PExpr Z) : option Z := Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n. Proof. - destruct n. + intros r n; destruct n as [|p]. reflexivity. simpl. unfold Z.pow_pos. replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring. generalize 1. - induction p; simpl ; intros ; repeat rewrite IHp ; ring. + induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring. Qed. Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e. Proof. - induction e ; simpl ; try congruence. + intros env e; induction e ; simpl ; try congruence. reflexivity. rewrite ZNpower. congruence. Qed. @@ -201,7 +202,7 @@ Lemma pop2_bop2 : forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. unfold is_true. - destruct op ; simpl; intros. + intro op; destruct op ; simpl; intros q1 q2. - apply Z.eqb_eq. - rewrite <- Z.eqb_eq. rewrite negb_true_iff. @@ -220,7 +221,7 @@ Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:= Lemma Zeval_op2_hold : forall k op q1 q2, Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2. Proof. - destruct k. + intro k; destruct k. simpl ; tauto. simpl. apply pop2_bop2. Qed. @@ -235,18 +236,18 @@ Definition Zeval_formula' := Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f. Proof. - destruct k ; simpl. + intros env k; destruct k ; simpl. - tauto. - - destruct f ; simpl. - rewrite <- Zeval_op2_hold with (k:=Tauto.isBool). + - intros f; destruct f ; simpl. + rewrite <- (Zeval_op2_hold Tauto.isBool). simpl. tauto. Qed. Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f. Proof. - intros. + intros env f. unfold Zeval_formula. - destruct f. + destruct f as [Flhs Fop Frhs]. repeat rewrite Zeval_expr_compat. unfold Zeval_formula' ; simpl. unfold eval_expr. @@ -343,7 +344,7 @@ Lemma Zunsat_sound : forall f, Zunsat f = true -> forall env, eval_nformula env f -> False. Proof. unfold Zunsat. - intros. + intros f H env ?. destruct f. eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto. Qed. @@ -365,7 +366,7 @@ Lemma xnnormalise_correct : forall env f, eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f. Proof. - intros. + intros env f. rewrite Zeval_formula_compat'. unfold xnnormalise. destruct f as [lhs o rhs]. @@ -375,18 +376,18 @@ Proof. generalize ( eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env lhs); generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) - (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros. + (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0. - split ; intros. - + assert (z0 + (z - z0) = z0 + 0) by congruence. + + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence. rewrite Z.add_0_r in H0. rewrite <- H0. ring. + subst. ring. - - split ; repeat intro. + - split ; intros H H0. subst. apply H. ring. apply H. - assert (z0 + (z - z0) = z0 + 0) by congruence. + assert (z0 + (z - z0) = z0 + 0) as H1 by congruence. rewrite Z.add_0_r in H1. rewrite <- H1. ring. @@ -396,11 +397,11 @@ Proof. - split ; intros. + apply Zle_0_minus_le; auto. + apply Zle_minus_le_0; auto. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt; auto. + apply Zlt_left_lt in H. apply H. - - split ; intros. + - split ; intros H. + apply Zlt_0_minus_lt ; auto. + apply Zlt_left_lt in H. apply H. @@ -430,7 +431,7 @@ Ltac iff_ring := Lemma xnormalise_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; generalize (eval_pol env e) as x; intro. @@ -458,11 +459,11 @@ Lemma cnf_of_list_correct : make_conj (fun x : NFormula Z => eval_nformula env x -> False) f. Proof. unfold cnf_of_list. - intros. + intros T tg f env. set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) => if Zunsat x then acc else ((x, tg) :: nil) :: acc)). set (E := ((fun x : NFormula Z => eval_nformula env x -> False))). - induction f. + induction f as [|a f IHf]. - compute. tauto. - rewrite make_conj_cons. @@ -489,10 +490,10 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold normalise. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_ff. @@ -519,10 +520,10 @@ Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T := Lemma xnegate_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f. Proof. - intros. + intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; - generalize (eval_pol env e) as x; intro. + generalize (eval_pol env e) as x; intro x. - tauto. - rewrite eq_cnf. destruct (Z.eq_decidable x 0);tauto. @@ -533,10 +534,10 @@ Qed. Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t. Proof. - intros. + intros T env t tg. rewrite <- xnnormalise_correct. unfold negate. - generalize (xnnormalise t) as f;intro. + generalize (xnnormalise t) as f;intro f. destruct (Zunsat f) eqn:U. - assert (US := Zunsat_sound _ U env). rewrite eval_cnf_tt. @@ -569,10 +570,10 @@ Require Import Znumtheory. Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b. Proof. unfold ceiling. - intros. + intros a b H. apply Zdivide_mod in H. case_eq (Z.div_eucl a b). - intros. + intros z z0 H0. change z with (fst (z,z0)). rewrite <- H0. change (fst (Z.div_eucl a b)) with (Z.div a b). @@ -642,12 +643,12 @@ Definition isZ0 (x:Z) := Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0. Proof. - destruct x ; simpl ; intuition congruence. + intros x; destruct x ; simpl ; intuition congruence. Qed. Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1. @@ -682,8 +683,8 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop := Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p -> forall env, eval_pol env p = a * eval_pol env (Zdiv_pol p a). Proof. - intros until 2. - induction H0. + intros a p H H0. + induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j]. (* Pc *) simpl. intros. @@ -702,7 +703,7 @@ Qed. Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0. Proof. - induction p. 1-2: easy. + intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy. simpl. case_eq (Zgcd_pol p1). case_eq (Zgcd_pol p3). @@ -715,7 +716,7 @@ Qed. Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) -> Zdivide_pol y p. Proof. - intros. + intros p x y H H0. induction H. constructor. apply Z.divide_trans with (1:= H0) ; assumption. @@ -725,7 +726,7 @@ Qed. Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p. Proof. - induction p ; constructor ; auto. + intros p; induction p as [c| |]; constructor ; auto. exists c. ring. Qed. @@ -744,19 +745,19 @@ Lemma Zdivide_pol_sub : forall p a b, Zdivide_pol a (PsubC Z.sub p b) -> Zdivide_pol (Z.gcd a b) p. Proof. - induction p. + intros p; induction p as [c|? p IHp|p ? ? ? IHp2]. simpl. - intros. inversion H0. + intros a b H H0. inversion H0. constructor. apply Zgcd_minus ; auto. - intros. + intros ? ? H H0. constructor. simpl in H0. inversion H0 ; subst; clear H0. apply IHp ; auto. - simpl. intros. + simpl. intros a b H H0. inv H0. constructor. - apply Zdivide_pol_Zdivide with (1:= H3). + apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)). destruct (Zgcd_is_gcd a b) ; assumption. apply IHp2 ; assumption. Qed. @@ -765,15 +766,15 @@ Lemma Zdivide_pol_sub_0 : forall p a, Zdivide_pol a (PsubC Z.sub p 0) -> Zdivide_pol a p. Proof. - induction p. + intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2]. simpl. - intros. inversion H. + intros ? H. inversion H. constructor. rewrite Z.sub_0_r in *. assumption. - intros. + intros ? H. constructor. simpl in H. inversion H ; subst; clear H. apply IHp ; auto. - simpl. intros. + simpl. intros ? H. inv H. constructor. auto. apply IHp2 ; assumption. @@ -783,9 +784,9 @@ Qed. Lemma Zgcd_pol_div : forall p g c, Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c). Proof. - induction p ; simpl. + intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl. (* Pc *) - intros. inv H. + intros ? ? H. inv H. constructor. exists 0. now ring. (* Pinj *) @@ -793,28 +794,28 @@ Proof. constructor. apply IHp ; auto. (* PX *) intros g c. - case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros. + case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1. inv H1. unfold ZgcdM at 1. destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1]; destruct HH1 as [HH1 HH1'] ; rewrite HH1'. constructor. - apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2). + apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)). unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_sub ; auto. apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. apply Zdivide_pol_one. unfold ZgcdM in HH1. unfold ZgcdM. destruct (Zmax_spec (Z.gcd z1 z2) 1) as [HH2 | HH2]. - destruct HH2. rewrite H2 in *. + destruct HH2 as [H1 H2]. rewrite H2 in *. destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto. - destruct HH2. rewrite H2. + destruct HH2 as [H1 H2]. rewrite H2. destruct (Zgcd_is_gcd 1 z); auto. - apply Zdivide_pol_Zdivide with (x:= z). + apply (Zdivide_pol_Zdivide _ z). apply (IHp2 _ _ H); auto. destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto. constructor. apply Zdivide_pol_one. @@ -873,7 +874,7 @@ Definition is_pol_Z0 (p : PolC Z) : bool := Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0. Proof. unfold is_pol_Z0. - destruct p ; try discriminate. + intros p; destruct p as [z| |]; try discriminate. destruct z ; try discriminate. reflexivity. Qed. @@ -915,8 +916,8 @@ Fixpoint max_var (jmp : positive) (p : Pol Z) : positive := Lemma pos_le_add : forall y x, (x <= y + x)%positive. Proof. - intros. - assert ((Z.pos x) <= Z.pos (x + y))%Z. + intros y x. + assert ((Z.pos x) <= Z.pos (x + y))%Z as H. rewrite <- (Z.add_0_r (Zpos x)). rewrite <- Pos2Z.add_pos_pos. apply Z.add_le_mono_l. @@ -929,10 +930,10 @@ Qed. Lemma max_var_le : forall p v, (v <= max_var v p)%positive. Proof. - induction p; simpl. + intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - intros. apply Pos.le_refl. - - intros. + - intros v. specialize (IHp (p+v)%positive). eapply Pos.le_trans ; eauto. assert (xH + v <= p + v)%positive. @@ -942,7 +943,7 @@ Proof. } eapply Pos.le_trans ; eauto. apply pos_le_add. - - intros. + - intros v. apply Pos.max_case_strong;intros ; auto. specialize (IHp2 (Pos.succ v)%positive). eapply Pos.le_trans ; eauto. @@ -951,10 +952,10 @@ Qed. Lemma max_var_correct : forall p j v, In v (vars j p) -> Pos.le v (max_var j p). Proof. - induction p; simpl. + intros p; induction p; simpl. - tauto. - auto. - - intros. + - intros j v H. rewrite in_app_iff in H. destruct H as [H |[ H | H]]. + subst. @@ -980,7 +981,7 @@ Section MaxVar. (v <= acc -> v <= fold_left F l acc)%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl] ; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -993,7 +994,7 @@ Section MaxVar. (acc <= acc' -> fold_left F l acc <= fold_left F l acc')%positive. Proof. - induction l ; simpl ; [easy|]. + intros l; induction l as [|a l IHl]; simpl ; [easy|]. intros. apply IHl. unfold F. @@ -1006,13 +1007,13 @@ Section MaxVar. Lemma max_var_nformulae_correct_aux : forall l p o v, In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive. Proof. - intros. + intros l p o v H H0. generalize 1%positive as acc. revert p o v H H0. - induction l. + induction l as [|a l IHl]. - simpl. tauto. - simpl. - intros. + intros p o v H H0 ?. destruct H ; subst. + unfold F at 2. simpl. @@ -1128,14 +1129,14 @@ Require Import Wf_nat. Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l). Proof. - induction l. + intros l; induction l as [|a l IHl]. (* nil *) simpl. tauto. (* cons *) simpl. - intros. - destruct H. + intros a0 b y H. + destruct H as [H|H]. subst. unfold ltof. simpl. @@ -1180,8 +1181,8 @@ Lemma eval_Psatz_sound : forall env w l f', make_conj (eval_nformula env) l -> eval_Psatz l w = Some f' -> eval_nformula env f'. Proof. - intros. - apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto. + intros env w l f' H H0. + apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto. apply make_conj_in ; auto. Qed. @@ -1193,7 +1194,7 @@ Proof. unfold nformula_of_cutting_plane. unfold eval_nformula. unfold RingMicromega.eval_nformula. unfold eval_op1. - intros. + intros env e e' c H H0. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. (**) @@ -1201,10 +1202,10 @@ Proof. revert H0. case_eq (Zgcd_pol e) ; intros g c0. generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0). - intros. + intros H0 H1 H2. inv H2. change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *. - apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt. + apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt. apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r. apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0). apply Z.le_ge. @@ -1213,7 +1214,7 @@ Proof. rewrite <- H1. assumption. (* g <= 0 *) - intros. inv H2. auto with zarith. + intros H0 H1 H2. inv H2. auto with zarith. Qed. Lemma cutting_plane_sound : forall env f p, @@ -1222,34 +1223,34 @@ Lemma cutting_plane_sound : forall env f p, eval_nformula env (nformula_of_cutting_plane p). Proof. unfold genCuttingPlane. - destruct f as [e op]. + intros env f; destruct f as [e op]. destruct op. (* Equal *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (Zgcd_pol e) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1 H2 H3. inv H3. unfold makeCuttingPlane in H. rewrite H1 in H. revert H. change (eval_pol env e = 0) in H2. case_eq (Z.gtb g 0). - intros. - rewrite <- Zgt_is_gt_bool in H. + intros H H3. + rewrite <- Zgt_is_gt_bool in H. rewrite Zgcd_pol_correct_lt with (1:= H1) in H2. 2: auto using Z.gt_lt. - unfold nformula_of_cutting_plane. + unfold nformula_of_cutting_plane. change (eval_pol env (padd e' (Pc z)) = 0). inv H3. rewrite eval_pol_add. set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x. simpl. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite Zgt_is_gt_bool in H ; congruence. rewrite andb_false_iff in H0. - destruct H0. + destruct H0 as [H0|H0]. rewrite negb_false_iff in H0. apply Zeq_bool_eq in H0. subst. simpl. @@ -1259,13 +1260,13 @@ Proof. apply Zeq_bool_eq in H0. assert (HH := Zgcd_is_gcd g c). rewrite H0 in HH. - inv HH. + destruct HH as [H3 H4 ?]. apply Zdivide_opp_r in H4. rewrite Zdivide_ceiling ; auto. apply Z.sub_move_0_r. apply Z.div_unique_exact. now intros ->. now rewrite Z.add_move_0_r in H2. - intros. + intros H H3. unfold nformula_of_cutting_plane. inv H3. change (eval_pol env (padd e' (Pc 0)) = 0). @@ -1273,7 +1274,7 @@ Proof. simpl. now rewrite Z.add_0_r. (* NonEqual *) - intros. + intros ? H H0. inv H0. unfold eval_nformula in *. unfold RingMicromega.eval_nformula in *. @@ -1282,20 +1283,20 @@ Proof. rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon). simpl. now rewrite Z.add_0_r. (* Strict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane (PsubC Z.sub e 1)). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). simpl in *. rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon). now apply Z.lt_le_pred. (* NonStrict *) - destruct p as [[e' z] op]. + intros p; destruct p as [[e' z] op]. case_eq (makeCuttingPlane e). - intros. + intros ? ? H H0 H1. inv H1. - apply makeCuttingPlane_ns_sound with (env:=env) (2:= H). + apply (makeCuttingPlane_ns_sound env) with (2:= H). assumption. Qed. @@ -1304,12 +1305,15 @@ Lemma genCuttingPlaneNone : forall env f, eval_nformula env f -> False. Proof. unfold genCuttingPlane. - destruct f. + intros env f; destruct f as [p o]. destruct o. case_eq (Zgcd_pol p) ; intros g c. case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))). - intros. + intros H H0 H1 H2. flatten_bool. + match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end. + match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end. + match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end. rewrite negb_true_iff in H5. apply Zeq_bool_neq in H5. rewrite <- Zgt_is_gt_bool in H3. @@ -1359,7 +1363,7 @@ Lemma agree_env_subset : forall v1 v2 env env', agree_env v2 env env'. Proof. unfold agree_env. - intros. + intros v1 v2 env env' H ? ? ?. apply H. eapply Pos.le_trans ; eauto. Qed. @@ -1369,7 +1373,7 @@ Lemma agree_env_jump : forall fr j env env', agree_env (fr + j) env env' -> agree_env fr (Env.jump j env) (Env.jump j env'). Proof. - intros. + intros fr j env env' H. unfold agree_env ; intro. intros. unfold Env.jump. @@ -1382,7 +1386,7 @@ Lemma agree_env_tail : forall fr env env', agree_env (Pos.succ fr) env env' -> agree_env fr (Env.tail env) (Env.tail env'). Proof. - intros. + intros fr env env' H. unfold Env.tail. apply agree_env_jump. rewrite <- Pos.add_1_r in H. @@ -1393,7 +1397,7 @@ Qed. Lemma max_var_acc : forall p i j, (max_var (i + j) p = max_var i p + j)%positive. Proof. - induction p; simpl. + intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - intros. rewrite ! IHp. @@ -1415,27 +1419,27 @@ Lemma agree_env_eval_nformula : (AGREE : agree_env (max_var xH (fst e)) env env'), eval_nformula env e <-> eval_nformula env' e. Proof. - destruct e. - simpl; intros. + intros env env' e; destruct e as [p o]. + simpl; intros AGREE. assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p) = - (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)). + (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H. { revert env env' AGREE. generalize xH. - induction p ; simpl. + induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl. - reflexivity. - - intros. - apply IHp with (p := p1%positive). + - intros p1 **. + apply (IHp p1). apply agree_env_jump. eapply agree_env_subset; eauto. rewrite (Pos.add_comm p). rewrite max_var_acc. apply Pos.le_refl. - - intros. + - intros p ? ? AGREE. f_equal. f_equal. - { apply IHp1 with (p:= p). + { apply (IHp1 p). eapply agree_env_subset; eauto. apply Pos.le_max_l. } @@ -1446,7 +1450,7 @@ Proof. apply Pos.le_1_l. } { - apply IHp2 with (p := p). + apply (IHp2 p). apply agree_env_tail. eapply agree_env_subset; eauto. rewrite !Pplus_one_succ_r. @@ -1463,11 +1467,11 @@ Lemma agree_env_eval_nformulae : make_conj (eval_nformula env) l <-> make_conj (eval_nformula env') l. Proof. - induction l. + intros env env' l; induction l as [|a l IHl]. - simpl. tauto. - intros. rewrite ! make_conj_cons. - assert (eval_nformula env a <-> eval_nformula env' a). + assert (eval_nformula env a <-> eval_nformula env' a) as H. { apply agree_env_eval_nformula. eapply agree_env_subset ; eauto. @@ -1491,7 +1495,7 @@ Qed. Lemma eq_true_iff_eq : forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2. Proof. - destruct b1,b2 ; intuition congruence. + intros b1 b2; destruct b1,b2 ; intuition congruence. Qed. Ltac pos_tac := @@ -1520,7 +1524,7 @@ Qed. Lemma ZChecker_sound : forall w l, ZChecker l w = true -> forall env, make_impl (eval_nformula env) l False. Proof. - induction w using (well_founded_ind (well_founded_ltof _ bdepth)). + intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)). destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf]. - (* DoneProof *) simpl. discriminate. @@ -1529,12 +1533,12 @@ Proof. intros l. case_eq (eval_Psatz l w) ; [| discriminate]. intros f Hf. case_eq (Zunsat f). - intros. + intros H0 ? ?. apply (checker_nf_sound Zsor ZSORaddon l w). unfold check_normalised_formulas. unfold eval_Psatz in Hf. rewrite Hf. unfold Zunsat in H0. assumption. - intros. - assert (make_impl (eval_nformula env) (f::l) False). + intros H0 H1 env. + assert (make_impl (eval_nformula env) (f::l) False) as H2. apply H with (2:= H1). unfold ltof. simpl. @@ -1553,8 +1557,8 @@ Proof. case_eq (eval_Psatz l w) ; [ | discriminate]. intros f' Hlc. case_eq (genCuttingPlane f'). - intros. - assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False). + intros p H0 H1 env. + assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2. eapply (H pf) ; auto. unfold ltof. simpl. @@ -1565,13 +1569,13 @@ Proof. intro. apply H2. split ; auto. - apply eval_Psatz_sound with (env:=env) in Hlc. + apply (eval_Psatz_sound env) in Hlc. apply cutting_plane_sound with (1:= Hlc) (2:= H0). auto. (* genCuttingPlane = None *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hlc) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - (* SplitProof *) @@ -1581,18 +1585,20 @@ Proof. case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate]. intros cp1 GCP1 cp2 GCP2 ZC1 env. flatten_bool. + match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end. + match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end. destruct (eval_nformula_split env p). - + apply H with (env:=env) in H0. + + apply (fun H' ck => H _ H' _ ck env) in H0. rewrite <- make_conj_impl in *. intro ; apply H0. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (p,NonStrict)) ; auto. apply ltof_bdepth_split_l. - + apply H with (env:=env) in H1. + + apply (fun H' ck => H _ H' _ ck env) in H1. rewrite <- make_conj_impl in *. intro ; apply H1. rewrite make_conj_cons. split; auto. - apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto. + apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto. apply ltof_bdepth_split_r. - (* EnumProof *) intros l. @@ -1601,22 +1607,22 @@ Proof. case_eq (eval_Psatz l w2) ; [ | discriminate]. intros f1 Hf1 f2 Hf2. case_eq (genCuttingPlane f2). - destruct p as [ [p1 z1] op1]. + intros p; destruct p as [ [p1 z1] op1]. case_eq (genCuttingPlane f1). - destruct p as [ [p2 z2] op2]. + intros p; destruct p as [ [p2 z2] op2]. case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)). intros Hcond. flatten_bool. - rename H1 into HZ0. - rename H2 into Hop1. - rename H3 into Hop2. + match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end. + match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end. + match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end. intros HCutL HCutR Hfix env. (* get the bounds of the enum *) rewrite <- make_conj_impl. - intro. - assert (-z1 <= eval_pol env p1 <= z2). + intro H0. + assert (-z1 <= eval_pol env p1 <= z2) as H1. split. - apply eval_Psatz_sound with (env:=env) in Hf2 ; auto. + apply (eval_Psatz_sound env) in Hf2 ; auto. apply cutting_plane_sound with (1:= Hf2) in HCutR. unfold nformula_of_cutting_plane in HCutR. unfold eval_nformula in HCutR. @@ -1628,10 +1634,10 @@ Proof. rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity. now apply Z.le_sub_le_add_r in HCutR. (**) - apply is_pol_Z0_eval_pol with (env := env) in HZ0. + apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0. rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0. rewrite HZ0. - apply eval_Psatz_sound with (env:=env) in Hf1 ; auto. + apply (eval_Psatz_sound env) in Hf1 ; auto. apply cutting_plane_sound with (1:= Hf1) in HCutL. unfold nformula_of_cutting_plane in HCutL. unfold eval_nformula in HCutL. @@ -1647,7 +1653,7 @@ Proof. match goal with | |- context[?F pf (-z1) z2 = true] => set (FF := F) end. - intros. + intros Hfix. assert (HH :forall x, -z1 <= x <= z2 -> exists pr, (In pr pf /\ ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z). @@ -1655,16 +1661,18 @@ Proof. revert Hfix. generalize (-z1). clear z1. intro z1. revert z1 z2. - induction pf;simpl ;intros. + induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **. revert Hfix. now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x. flatten_bool. + match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end. + match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end. destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ]. 2: exists a; auto. rewrite <- Z.le_succ_l in LT. assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition. elim IHpf with (2:=H2) (3:= LE). - intros. + intros x0 ?. exists x0 ; split;tauto. intros until 1. apply H ; auto. @@ -1676,7 +1684,7 @@ Proof. apply Z.add_le_mono_r. assumption. (*/asser *) destruct (HH _ H1) as [pr [Hin Hcheker]]. - assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False). + assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2. eapply (H pr) ;auto. apply in_bdepth ; auto. rewrite <- make_conj_impl in H2. @@ -1690,15 +1698,15 @@ Proof. unfold eval_pol. ring. discriminate. (* No cutting plane *) - intros. + intros H0 H1 H2 env. rewrite <- make_conj_impl. - intros. + intros H3. apply eval_Psatz_sound with (2:= Hf1) in H3. apply genCuttingPlaneNone with (2:= H3) ; auto. (* No Cutting plane (bis) *) - intros. + intros H0 H1 env. rewrite <- make_conj_impl. - intros. + intros H2. apply eval_Psatz_sound with (2:= Hf2) in H2. apply genCuttingPlaneNone with (2:= H2) ; auto. - intros l. @@ -1708,15 +1716,15 @@ Proof. set (z1 := (Pos.succ fr)) in *. set (t1 := (Pos.succ z1)) in *. destruct (x <=? fr)%positive eqn:LE ; [|congruence]. - intros. + intros H0 env. set (env':= fun v => if Pos.eqb v z1 then if Z.leb (env x) 0 then 0 else env x else if Pos.eqb v t1 then if Z.leb (env x) 0 then -(env x) else 0 else env v). - apply H with (env:=env') in H0. + apply (fun H' ck => H _ H' _ ck env') in H0. + rewrite <- make_conj_impl in *. - intro. + intro H1. rewrite !make_conj_cons in H0. apply H0 ; repeat split. * @@ -1729,17 +1737,17 @@ Proof. destruct (env x <=? 0); ring. { unfold t1. pos_tac; normZ. - lia (Hyp H2). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). } { unfold t1, z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))). } { unfold z1. pos_tac; normZ. - lia (Add (Hyp LE) (Hyp H3)). + lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))). } * apply eval_nformula_bound_var. @@ -1749,7 +1757,7 @@ Proof. compute. congruence. rewrite Z.leb_gt in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))). * apply eval_nformula_bound_var. unfold env'. @@ -1758,15 +1766,15 @@ Proof. destruct (env x <=? 0) eqn:EQ. rewrite Z.leb_le in EQ. normZ. - lia (Add (Hyp EQ) (Hyp H2)). + lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))). compute; congruence. unfold t1. clear. pos_tac; normZ. - lia (Hyp H). + lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)). * - rewrite agree_env_eval_nformulae with (env':= env') in H1;auto. - unfold agree_env; intros. + rewrite (agree_env_eval_nformulae _ env') in H1;auto. + unfold agree_env; intros x0 H2. unfold env'. replace (x0 =? z1)%positive with false. replace (x0 =? t1)%positive with false. @@ -1776,13 +1784,13 @@ Proof. unfold fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))). } { unfold z1, fr in *. apply Pos2Z.pos_le_pos in H2. pos_tac; normZ. - lia (Add (Hyp H2) (Hyp H4)). + lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))). } + unfold ltof. simpl. @@ -1796,27 +1804,27 @@ Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, Proof. intros f w. unfold ZTautoChecker. - apply tauto_checker_sound with (eval' := eval_nformula). + apply (tauto_checker_sound _ _ _ _ eval_nformula). - apply Zeval_nformula_dec. - - intros until env. + - intros t ? env. unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. apply (check_inconsistent_sound Zsor ZSORaddon) ; auto. - - unfold Zdeduce. intros. revert H. + - unfold Zdeduce. intros ? ? ? H **. revert H. apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto. - - intros. + intros ? ? ? ? H. rewrite normalise_correct in H. rewrite Zeval_formula_compat; auto. - - intros. + intros ? ? ? ? H. rewrite negate_correct in H ; auto. rewrite Tauto.hold_eNOT. rewrite Zeval_formula_compat; auto. - intros t w0. unfold eval_tt. - intros. - rewrite make_impl_map with (eval := eval_nformula env). + intros H env. + rewrite (make_impl_map (eval_nformula env)). eapply ZChecker_sound; eauto. tauto. Qed. diff --git a/theories/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v index c12f46bed6..4b3bba9843 100644 --- a/theories/setoid_ring/Field_theory.v +++ b/theories/setoid_ring/Field_theory.v @@ -397,7 +397,7 @@ Qed. Theorem cross_product_eq a b c d : ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d. Proof. -intros. +intros H H0 H1. transitivity (a / b * (d / d)). - now rewrite rdiv_r_r, rmul_1_r. - now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r. @@ -418,23 +418,23 @@ Qed. Lemma pow_pos_0 p : pow_pos rmul 0 p == 0. Proof. -induction p;simpl;trivial; now rewrite !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !IHp. Qed. Lemma pow_pos_1 p : pow_pos rmul 1 p == 1. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p]. Proof. -induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. +induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp. Qed. Lemma pow_pos_mul_l x y p : pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p. Proof. -induction p;simpl;trivial; ring [IHp]. +induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp]. Qed. Lemma pow_pos_add_r x p1 p2 : @@ -446,7 +446,7 @@ Qed. Lemma pow_pos_mul_r x p1 p2 : pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2. Proof. -induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; +induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r; simpl; trivial; ring [IHp1]. Qed. @@ -459,8 +459,8 @@ Qed. Lemma pow_pos_div a b p : ~ b == 0 -> pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p. Proof. - intros. - induction p; simpl; trivial. + intros H. + induction p as [p IHp|p IHp|]; simpl; trivial. - rewrite IHp. assert (nz := pow_pos_nz p H). rewrite !rdiv4; trivial. @@ -578,14 +578,15 @@ Qed. Theorem PExpr_eq_semi_ok e e' : PExpr_eq e e' = true -> (e === e')%poly. Proof. -revert e'; induction e; destruct e'; simpl; try discriminate. +revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?]; + intro e'; destruct e'; simpl; try discriminate. - intros H l. now apply (morph_eq CRmorph). - case Pos.eqb_spec; intros; now subst. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2. - intros H. now rewrite IHe. -- intros H. destruct (if_true _ _ H). +- intros H. destruct (if_true _ _ H) as [H0 H1]. apply N.eqb_eq in H0. now rewrite IHe, H0. Qed. @@ -667,7 +668,7 @@ Proof. - case Pos.eqb_spec; [intro; subst | intros _]. + simpl. now rewrite rpow_pow. + destruct e;simpl;trivial. - repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl. + repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl. * now rewrite phi_1, pow_pos_1. * now rewrite phi_0, pow_pos_0. * now rewrite pow_pos_cst. @@ -686,7 +687,8 @@ Infix "**" := NPEmul (at level 40, left associativity). Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly. Proof. intros l. -revert e2; induction e1;destruct e2; simpl;try reflexivity; +revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n]; + intro e2; destruct e2; simpl;try reflexivity; repeat (case ceqb_spec; intro H; try rewrite H; clear H); simpl; try reflexivity; try ring [phi_0 phi_1]. apply (morph_mul CRmorph). @@ -801,7 +803,7 @@ Qed. Theorem PCond_app l l1 l2 : PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2. Proof. -induction l1. +induction l1 as [|a l1 IHl1]. - simpl. split; [split|destruct 1]; trivial. - simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc. Qed. @@ -813,7 +815,7 @@ Definition absurd_PCond := cons 0%poly nil. Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond. Proof. unfold absurd_PCond; simpl. -red; intros. +red; intros ? H. apply H. apply phi_0. Qed. @@ -901,7 +903,7 @@ Theorem isIn_ok e1 p1 e2 p2 : Proof. Opaque NPEpow. revert p1 p2. -induction e2; intros p1 p2; +induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2; try refine (default_isIn_ok e1 _ p1 p2); simpl isIn. - specialize (IHe2_1 p1 p2). destruct isIn as [([|p],e)|]. @@ -936,7 +938,7 @@ induction e2; intros p1 p2; destruct IHe2_2 as (IH,GT). split; trivial. set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d. npe_simpl. rewrite IH. npe_ring. -- destruct n; trivial. +- destruct n as [|p]; trivial. specialize (IHe2 p1 (p * p2)%positive). destruct isIn as [(n,e)|]; trivial. destruct IHe2 as (IH,GT). split; trivial. @@ -983,7 +985,7 @@ Lemma split_aux_ok1 e1 p e2 : /\ e2 === right res * common res)%poly. Proof. Opaque NPEpow NPEmul. - intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). + intros res. unfold res;clear res; generalize (isIn_ok e1 p e2 xH). destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl. - intros (H1,H2); split; npe_simpl. + now rewrite PE_1_l. @@ -1000,7 +1002,8 @@ Theorem split_aux_ok: forall e1 p e2, (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2) /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly. Proof. -induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl. +intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n]; + intros k e2; try refine (split_aux_ok1 _ k e2);simpl. destruct (IHe1_1 k e2) as (H1,H2). destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4). clear IHe1_1 IHe1_2. @@ -1101,7 +1104,8 @@ Eval compute Theorem Pcond_Fnorm l e : PCond l (condition (Fnorm e)) -> ~ (denum (Fnorm e))@l == 0. Proof. -induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app; +induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok. - simpl. rewrite phi_1; exact rI_neq_rO. - simpl. rewrite phi_1; exact rI_neq_rO. @@ -1141,7 +1145,8 @@ Theorem Fnorm_FEeval_PEeval l fe: PCond l (condition (Fnorm fe)) -> FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l. Proof. -induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; +induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n]; + simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl; intros (Hc1,Hc2) || intros Hc; try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1); try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2); @@ -1260,7 +1265,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_dev _ _). apply eq_trans with (nnum / NPphi_dev l (Pc c)). apply rdiv_ext; @@ -1285,7 +1290,7 @@ Proof. destruct (Nnorm _ _ _) as [c | | ] eqn: HN; try ( apply rdiv_ext; eapply ring_rw_pow_correct; eauto). - destruct (ceqb_spec c cI). + destruct (ceqb_spec c cI) as [H0|]. set (nnum := NPphi_pow _ _). apply eq_trans with (nnum / NPphi_pow l (Pc c)). apply rdiv_ext; @@ -1415,7 +1420,8 @@ Theorem Field_simplify_eq_pow_in_correct : NPphi_pow l np1 == NPphi_pow l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). simpl. apply Field_simplify_aux_ok; trivial. @@ -1434,7 +1440,8 @@ forall n l lpe fe1 fe2, PCond l (condition nfe1 ++ condition nfe2) -> NPphi_dev l np1 == NPphi_dev l np2. Proof. - intros. subst nfe1 nfe2 lmp np1 np2. + intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?. + subst nfe1 nfe2 lmp np1 np2. rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph get_sign_spec). repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial). apply Field_simplify_aux_ok; trivial. @@ -1458,7 +1465,7 @@ Lemma fcons_ok : forall l l1, (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. Proof. intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. -induction l1; simpl; intros. +induction l1 as [|a l1 IHl1]; simpl; intros. trivial. elim PCond_fcons_inv with (1 := H); intros. destruct l1; trivial. split; trivial. apply IHl1; trivial. @@ -1480,7 +1487,7 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons_fcons_inv: forall l a l1, PCond l (Fcons a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons. - simpl; now split. - case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2); repeat split; trivial. @@ -1501,7 +1508,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) := Theorem PFcons0_fcons_inv: forall l a l1, PCond l (Fcons0 a l1) -> ~ a @ l == 0 /\ PCond l l1. Proof. -induction l1 as [|e l1]; simpl Fcons0. +intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0. - simpl; now split. - generalize (ring_correct O l nil a e). lazy zeta; simpl Peq. case Peq; intros H; rewrite !PCond_cons; intros (H1,H2); @@ -1529,7 +1536,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). destruct (H0 _ H3) as (H4,H5). split; trivial. simpl. apply field_is_integral_domain; trivial. -- intros. destruct (H _ H0). split; trivial. +- intros ? H ? ? H0. destruct (H _ H0). split; trivial. apply PEpow_nz; trivial. Qed. @@ -1580,7 +1587,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail). split; trivial. apply ropp_neq_0; trivial. rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial. -- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. +- intros ? H ? ? H0. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial. Qed. Definition Fcons2 e l := Fcons1 (PEsimp e) l. @@ -1674,7 +1681,7 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0. Lemma add_inj_r p x y : gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y. Proof. -elim p using Pos.peano_ind; simpl; intros. +elim p using Pos.peano_ind; simpl; [intros H|intros ? H ?]. apply S_inj; trivial. apply H. apply S_inj. @@ -1710,8 +1717,8 @@ Lemma gen_phiN_inj x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y. Proof. -destruct x; destruct y; simpl; intros; trivial. - elim gen_phiPOS_not_0 with p. +destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial. + elim gen_phiPOS_not_0 with p'. symmetry . rewrite (same_gen Rsth Reqe ARth); trivial. elim gen_phiPOS_not_0 with p. @@ -1770,14 +1777,14 @@ Lemma gen_phiZ_inj x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y. Proof. -destruct x; destruct y; simpl; intros. +destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H. trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). symmetry ; trivial. - elim gen_phiPOS_not_0 with p. + elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). elim gen_phiPOS_not_0 with p. @@ -1790,12 +1797,12 @@ destruct x; destruct y; simpl; intros. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). rewrite H. apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_discr_sgn with p0 p. + elim gen_phiPOS_discr_sgn with p' p. symmetry ; trivial. - replace p0 with p; trivial. + replace p' with p; trivial. apply gen_phiPOS_inject. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). - rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)). + rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite H; trivial. reflexivity. Qed. |