From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- theories/Arith/Between.v | 24 ++-- theories/Arith/EqNat.v | 4 +- theories/Arith/Gt.v | 16 +-- theories/Arith/Le.v | 12 +- theories/Arith/Lt.v | 26 ++--- theories/Arith/Max.v | 4 +- theories/Arith/Minus.v | 20 ++-- theories/Arith/Mult.v | 16 +-- theories/Arith/Peano_dec.v | 5 +- theories/Arith/Plus.v | 12 +- theories/Bool/Bool.v | 30 ++--- theories/Bool/IfProp.v | 2 +- theories/Classes/CMorphisms.v | 4 +- theories/Classes/Equivalence.v | 8 +- theories/Classes/Morphisms.v | 6 +- theories/Classes/RelationPairs.v | 5 + theories/Classes/SetoidTactics.v | 16 +-- theories/Compat/Coq84.v | 54 +++++---- theories/Compat/Coq85.v | 27 +++++ theories/Compat/Coq86.v | 9 ++ theories/Compat/vo.itarget | 1 + theories/FSets/FMapFacts.v | 10 +- theories/FSets/FMapList.v | 2 +- theories/FSets/FMapPositive.v | 10 +- theories/FSets/FMapWeakList.v | 2 +- theories/FSets/FSetDecide.v | 19 +-- theories/FSets/FSetList.v | 2 +- theories/FSets/FSetPositive.v | 28 ++--- theories/FSets/FSetWeakList.v | 2 +- theories/Init/Datatypes.v | 2 + theories/Init/Logic_Type.v | 2 +- theories/Init/Notations.v | 8 +- theories/Init/Peano.v | 3 - theories/Init/Prelude.v | 1 + theories/Init/Specif.v | 3 +- theories/Init/Tactics.v | 8 +- theories/Init/Tauto.v | 101 ++++++++++++++++ theories/Init/Wf.v | 2 +- theories/Init/vo.itarget | 3 +- theories/Lists/List.v | 117 +++++++++++++++---- theories/Lists/ListSet.v | 109 ++++++++++++++++- theories/Lists/Streams.v | 2 +- theories/Logic/ClassicalFacts.v | 78 +++++++++++++ theories/Logic/Decidable.v | 2 +- theories/Logic/Eqdep.v | 2 +- theories/Logic/EqdepFacts.v | 2 +- theories/Logic/Hurkens.v | 3 +- theories/Logic/PropFacts.v | 50 ++++++++ theories/MSets/MSetAVL.v | 1 + theories/MSets/MSetDecide.v | 19 +-- theories/MSets/MSetInterface.v | 3 + theories/MSets/MSetList.v | 2 +- theories/MSets/MSetPositive.v | 28 ++--- theories/MSets/MSetRBT.v | 4 +- theories/MSets/MSetWeakList.v | 2 +- theories/Numbers/BigNumPrelude.v | 4 +- theories/Numbers/Cyclic/Int31/Ring31.v | 20 ++-- theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 +- theories/Numbers/Integer/Abstract/ZDivEucl.v | 14 ++- theories/Numbers/Integer/BigZ/BigZ.v | 24 ++-- theories/Numbers/Integer/BigZ/ZMake.v | 12 +- theories/Numbers/NatInt/NZGcd.v | 2 - theories/Numbers/Natural/BigN/BigN.v | 26 ++--- theories/Numbers/Natural/BigN/NMake.v | 2 +- theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +- theories/Numbers/Natural/Peano/NPeano.v | 84 +++++++++++++- theories/Numbers/Rational/BigQ/BigQ.v | 14 +-- theories/Numbers/Rational/BigQ/QMake.v | 37 +++--- theories/Numbers/Rational/SpecViaQ/QSig.v | 10 +- theories/PArith/BinPos.v | 3 +- theories/Program/Equality.v | 11 +- theories/Program/Subset.v | 1 + theories/Program/Tactics.v | 4 +- theories/Program/Wf.v | 4 +- theories/QArith/Qcabs.v | 129 +++++++++++++++++++++ theories/QArith/Qcanon.v | 120 +++++++++---------- theories/QArith/Qreduction.v | 22 +++- theories/QArith/vo.itarget | 1 + theories/Reals/RIneq.v | 12 +- theories/Reals/Ranalysis_reg.v | 109 +++++++++-------- theories/Reals/Raxioms.v | 8 +- theories/Reals/Sqrt_reg.v | 2 +- theories/Relations/Operators_Properties.v | 2 +- theories/Relations/Relation_Definitions.v | 6 +- theories/Relations/Relation_Operators.v | 6 +- theories/Sets/Classical_sets.v | 2 +- theories/Sets/Constructive_sets.v | 2 +- theories/Sets/Ensembles.v | 5 +- theories/Sets/Finite_sets.v | 4 +- theories/Sets/Image.v | 2 +- theories/Sets/Multiset.v | 6 +- theories/Sets/Partial_Order.v | 4 +- theories/Sets/Powerset.v | 22 ++-- theories/Sets/Powerset_Classical_facts.v | 14 +-- theories/Sets/Powerset_facts.v | 2 +- theories/Sets/Relations_1.v | 4 +- theories/Sets/Relations_2.v | 8 +- theories/Sets/Relations_3.v | 12 +- theories/Sorting/Permutation.v | 4 +- theories/Strings/Ascii.v | 2 +- theories/Strings/String.v | 10 +- theories/Structures/OrdersFacts.v | 6 +- theories/Vectors/VectorDef.v | 14 ++- .../Wellfounded/Lexicographic_Exponentiation.v | 6 +- theories/Wellfounded/Lexicographic_Product.v | 9 +- theories/ZArith/Int.v | 18 +-- theories/ZArith/Zsqrt_compat.v | 4 +- theories/ZArith/Zwf.v | 4 +- theories/theories.itarget | 25 ---- 109 files changed, 1239 insertions(+), 580 deletions(-) create mode 100644 theories/Compat/Coq86.v create mode 100644 theories/Init/Tauto.v create mode 100644 theories/Logic/PropFacts.v create mode 100644 theories/QArith/Qcabs.v delete mode 100644 theories/theories.itarget (limited to 'theories') diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index f998e861..58d3a2b3 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -20,20 +20,20 @@ Section Between. | bet_emp : between k k | bet_S : forall l, between k l -> P l -> between k (S l). - Hint Constructors between: arith v62. + Hint Constructors between: arith. Lemma bet_eq : forall k l, l = k -> between k l. Proof. induction 1; auto with arith. Qed. - Hint Resolve bet_eq: arith v62. + Hint Resolve bet_eq: arith. Lemma between_le : forall k l, between k l -> k <= l. Proof. induction 1; auto with arith. Qed. - Hint Immediate between_le: arith v62. + Hint Immediate between_le: arith. Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. @@ -41,7 +41,7 @@ Section Between. intros; absurd (S k <= k); auto with arith. destruct H; auto with arith. Qed. - Hint Resolve between_Sk_l: arith v62. + Hint Resolve between_Sk_l: arith. Lemma between_restr : forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m. @@ -53,7 +53,7 @@ Section Between. | exists_S : forall l, exists_between k l -> exists_between k (S l) | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). - Hint Constructors exists_between: arith v62. + Hint Constructors exists_between: arith. Lemma exists_le_S : forall k l, exists_between k l -> S k <= l. Proof. @@ -62,13 +62,13 @@ Section Between. Lemma exists_lt : forall k l, exists_between k l -> k < l. Proof exists_le_S. - Hint Immediate exists_le_S exists_lt: arith v62. + Hint Immediate exists_le_S exists_lt: arith. Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. Proof. intros; apply le_S_n; auto with arith. Qed. - Hint Immediate exists_S_le: arith v62. + Hint Immediate exists_S_le: arith. Definition in_int p q r := p <= r /\ r < q. @@ -76,7 +76,7 @@ Section Between. Proof. red; auto with arith. Qed. - Hint Resolve in_int_intro: arith v62. + Hint Resolve in_int_intro: arith. Lemma in_int_lt : forall p q r, in_int p q r -> p < q. Proof. @@ -95,13 +95,13 @@ Section Between. Proof. induction 1; auto with arith. Qed. - Hint Resolve in_int_S: arith v62. + Hint Resolve in_int_S: arith. Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. induction 1; auto with arith. Qed. - Hint Immediate in_int_Sp_q: arith v62. + Hint Immediate in_int_Sp_q: arith. Lemma between_in_int : forall k l, between k l -> forall r, in_int k l r -> P r. @@ -183,5 +183,5 @@ Section Between. End Between. Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le - in_int_S in_int_intro: arith v62. -Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62. + in_int_S in_int_intro: arith. +Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 206fc0ab..f998c19f 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -25,7 +25,7 @@ Theorem eq_nat_refl n : eq_nat n n. Proof. induction n; simpl; auto. Qed. -Hint Resolve eq_nat_refl: arith v62. +Hint Resolve eq_nat_refl: arith. (** [eq] restricted to [nat] and [eq_nat] are equivalent *) @@ -46,7 +46,7 @@ Proof. apply eq_nat_is_eq. Qed. -Hint Immediate eq_eq_nat eq_nat_eq: arith v62. +Hint Immediate eq_eq_nat eq_nat_eq: arith. Theorem eq_nat_elim : forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index dfd57694..67c94fdf 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -133,14 +133,14 @@ Qed. (** * Hints *) -Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62. -Hint Immediate gt_S_n gt_pred : arith v62. -Hint Resolve gt_irrefl gt_asym : arith v62. -Hint Resolve le_not_gt gt_not_le : arith v62. -Hint Immediate le_S_gt gt_S_le : arith v62. -Hint Resolve gt_le_S le_gt_S : arith v62. -Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. -Hint Resolve plus_gt_compat_l: arith v62. +Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith. +Hint Immediate gt_S_n gt_pred : arith. +Hint Resolve gt_irrefl gt_asym : arith. +Hint Resolve le_not_gt gt_not_le : arith. +Hint Immediate le_S_gt gt_S_le : arith. +Hint Resolve gt_le_S le_gt_S : arith. +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith. +Hint Resolve plus_gt_compat_l: arith. (* begin hide *) Notation gt_O_eq := gt_0_eq (only parsing). diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index ceb91187..0fbcec57 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -30,8 +30,8 @@ Notation le_refl := Nat.le_refl (compat "8.4"). Notation le_trans := Nat.le_trans (compat "8.4"). Notation le_antisym := Nat.le_antisymm (compat "8.4"). -Hint Resolve le_trans: arith v62. -Hint Immediate le_antisym: arith v62. +Hint Resolve le_trans: arith. +Hint Immediate le_antisym: arith. (** * Properties of [le] w.r.t 0 *) @@ -59,16 +59,16 @@ Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof Nat.lt_le_incl. -Hint Resolve le_0_n le_Sn_0: arith v62. -Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62. -Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62. +Hint Resolve le_0_n le_Sn_0: arith. +Hint Resolve le_n_S le_n_Sn le_Sn_n : arith. +Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith. (** * Properties of [le] w.r.t predecessor *) Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *) Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *) -Hint Resolve le_pred_n: arith v62. +Hint Resolve le_pred_n: arith. (** * A different elimination principle for the order on natural numbers *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index f824ee6f..bfc2b91a 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -25,7 +25,7 @@ Local Open Scope nat_scope. Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *) -Hint Resolve lt_irrefl: arith v62. +Hint Resolve lt_irrefl: arith. (** * Relationship between [le] and [lt] *) @@ -44,9 +44,9 @@ Proof. apply Nat.lt_succ_r. Qed. -Hint Immediate lt_le_S: arith v62. -Hint Immediate lt_n_Sm_le: arith v62. -Hint Immediate le_lt_n_Sm: arith v62. +Hint Immediate lt_le_S: arith. +Hint Immediate lt_n_Sm_le: arith. +Hint Immediate le_lt_n_Sm: arith. Theorem le_not_lt n m : n <= m -> ~ m < n. Proof. @@ -58,7 +58,7 @@ Proof. apply Nat.lt_nge. Qed. -Hint Immediate le_not_lt lt_not_le: arith v62. +Hint Immediate le_not_lt lt_not_le: arith. (** * Asymmetry *) @@ -79,8 +79,8 @@ Proof. intros. now apply Nat.neq_sym, Nat.neq_0_lt_0. Qed. -Hint Resolve lt_0_Sn lt_n_0 : arith v62. -Hint Immediate neq_0_lt lt_0_neq: arith v62. +Hint Resolve lt_0_Sn lt_n_0 : arith. +Hint Immediate neq_0_lt lt_0_neq: arith. (** * Order and successor *) @@ -97,8 +97,8 @@ Proof. apply Nat.succ_lt_mono. Qed. -Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62. -Hint Immediate lt_S_n : arith v62. +Hint Resolve lt_n_Sn lt_S lt_n_S : arith. +Hint Immediate lt_S_n : arith. (** * Predecessor *) @@ -117,8 +117,8 @@ Proof. intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0. Qed. -Hint Immediate lt_pred: arith v62. -Hint Resolve lt_pred_n_n: arith v62. +Hint Immediate lt_pred: arith. +Hint Resolve lt_pred_n_n: arith. (** * Transitivity properties *) @@ -126,7 +126,7 @@ Notation lt_trans := Nat.lt_trans (compat "8.4"). Notation lt_le_trans := Nat.lt_le_trans (compat "8.4"). Notation le_lt_trans := Nat.le_lt_trans (compat "8.4"). -Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. +Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) @@ -139,7 +139,7 @@ Qed. Notation lt_le_weak := Nat.lt_le_incl (compat "8.4"). -Hint Immediate lt_le_weak: arith v62. +Hint Immediate lt_le_weak: arith. (** * Dichotomy *) diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 65534b2e..49152549 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -42,7 +42,7 @@ Notation max_SS := Nat.succ_max_distr (only parsing). (* end hide *) Hint Resolve - Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62. + Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith. Hint Resolve - Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. + Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index bc3a318c..1fc8f790 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -107,13 +107,13 @@ Qed. (** * Hints *) -Hint Resolve minus_n_O: arith v62. -Hint Resolve minus_Sn_m: arith v62. -Hint Resolve minus_diag_reverse: arith v62. -Hint Resolve minus_plus_simpl_l_reverse: arith v62. -Hint Immediate plus_minus: arith v62. -Hint Resolve minus_plus: arith v62. -Hint Resolve le_plus_minus: arith v62. -Hint Resolve le_plus_minus_r: arith v62. -Hint Resolve lt_minus: arith v62. -Hint Immediate lt_O_minus_lt: arith v62. +Hint Resolve minus_n_O: arith. +Hint Resolve minus_Sn_m: arith. +Hint Resolve minus_diag_reverse: arith. +Hint Resolve minus_plus_simpl_l_reverse: arith. +Hint Immediate plus_minus: arith. +Hint Resolve minus_plus: arith. +Hint Resolve le_plus_minus: arith. +Hint Resolve le_plus_minus_r: arith. +Hint Resolve lt_minus: arith. +Hint Immediate lt_O_minus_lt: arith. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index 96581243..a173efc1 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -31,13 +31,13 @@ Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *) Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *) Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *) -Hint Resolve mult_1_l mult_1_r: arith v62. +Hint Resolve mult_1_l mult_1_r: arith. (** ** Commutativity *) Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *) -Hint Resolve mult_comm: arith v62. +Hint Resolve mult_comm: arith. (** ** Distributivity *) @@ -53,9 +53,9 @@ Notation mult_minus_distr_r := Notation mult_minus_distr_l := Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *) -Hint Resolve mult_plus_distr_r: arith v62. -Hint Resolve mult_minus_distr_r: arith v62. -Hint Resolve mult_minus_distr_l: arith v62. +Hint Resolve mult_plus_distr_r: arith. +Hint Resolve mult_minus_distr_r: arith. +Hint Resolve mult_minus_distr_l: arith. (** ** Associativity *) @@ -66,8 +66,8 @@ Proof. symmetry. apply Nat.mul_assoc. Qed. -Hint Resolve mult_assoc_reverse: arith v62. -Hint Resolve mult_assoc: arith v62. +Hint Resolve mult_assoc_reverse: arith. +Hint Resolve mult_assoc: arith. (** ** Inversion lemmas *) @@ -92,7 +92,7 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. -Hint Resolve mult_O_le: arith v62. +Hint Resolve mult_O_le: arith. Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 340a7968..f8020a50 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -38,8 +38,7 @@ intros m n. generalize (eq_refl (S n)). generalize n at -1. induction (S n) as [|n0 IHn0]; try discriminate. -clear n; intros n H; injection H; clear H; intro H. -rewrite <- H; intros le_mn1 le_mn2; clear n H. +clear n; intros n [= <-] le_mn1 le_mn2. pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2). 2: reflexivity. generalize def_n2; revert le_mn1 le_mn2. @@ -50,7 +49,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2. now destruct (Nat.nle_succ_diag_l _ le_mn0). + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). -+ intros def_n0; injection def_n0; intros ->. ++ intros def_n0. injection def_n0 as ->. rewrite (UIP_nat _ _ def_n0 eq_refl); simpl. assert (H : le_mn1 = le_mn2). now apply IHn0. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 3b823da6..600e5e51 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -177,12 +177,12 @@ Proof (succ_plus_discr n 3). (** * Compatibility Hints *) -Hint Immediate plus_comm : arith v62. -Hint Resolve plus_assoc plus_assoc_reverse : arith v62. -Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62. -Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62. -Hint Immediate lt_plus_trans : arith v62. -Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62. +Hint Immediate plus_comm : arith. +Hint Resolve plus_assoc plus_assoc_reverse : arith. +Hint Resolve plus_le_compat_l plus_le_compat_r : arith. +Hint Resolve le_plus_l le_plus_r le_plus_trans : arith. +Hint Immediate lt_plus_trans : arith. +Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith. (** For compatibility, we "Require" the same files as before *) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 721ab693..06096c66 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -39,13 +39,13 @@ Lemma diff_true_false : true <> false. Proof. discriminate. Qed. -Hint Resolve diff_true_false : bool v62. +Hint Resolve diff_true_false : bool. Lemma diff_false_true : false <> true. Proof. discriminate. Qed. -Hint Resolve diff_false_true : bool v62. +Hint Resolve diff_false_true : bool. Hint Extern 1 (false <> true) => exact diff_false_true. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. @@ -82,7 +82,7 @@ Definition leb (b1 b2:bool) := | true => b2 = true | false => True end. -Hint Unfold leb: bool v62. +Hint Unfold leb: bool. Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true. Proof. @@ -242,14 +242,14 @@ Lemma orb_true_intro : Proof. intros; apply orb_true_iff; trivial. Qed. -Hint Resolve orb_true_intro: bool v62. +Hint Resolve orb_true_intro: bool. Lemma orb_false_intro : forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false. Proof. intros. subst. reflexivity. Qed. -Hint Resolve orb_false_intro: bool v62. +Hint Resolve orb_false_intro: bool. Lemma orb_false_elim : forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false. @@ -268,7 +268,7 @@ Lemma orb_true_r : forall b:bool, b || true = true. Proof. destr_bool. Qed. -Hint Resolve orb_true_r: bool v62. +Hint Resolve orb_true_r: bool. Lemma orb_true_l : forall b:bool, true || b = true. Proof. @@ -284,13 +284,13 @@ Lemma orb_false_r : forall b:bool, b || false = b. Proof. destr_bool. Qed. -Hint Resolve orb_false_r: bool v62. +Hint Resolve orb_false_r: bool. Lemma orb_false_l : forall b:bool, false || b = b. Proof. destr_bool. Qed. -Hint Resolve orb_false_l: bool v62. +Hint Resolve orb_false_l: bool. Notation orb_b_false := orb_false_r (only parsing). Notation orb_false_b := orb_false_l (only parsing). @@ -301,7 +301,7 @@ Lemma orb_negb_r : forall b:bool, b || negb b = true. Proof. destr_bool. Qed. -Hint Resolve orb_negb_r: bool v62. +Hint Resolve orb_negb_r: bool. Notation orb_neg_b := orb_negb_r (only parsing). @@ -318,7 +318,7 @@ Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3. Proof. destr_bool. Qed. -Hint Resolve orb_comm orb_assoc: bool v62. +Hint Resolve orb_comm orb_assoc: bool. (*******************************) (** * Properties of [andb] *) @@ -392,7 +392,7 @@ Lemma andb_false_elim : Proof. destruct b1; simpl; auto. Defined. -Hint Resolve andb_false_elim: bool v62. +Hint Resolve andb_false_elim: bool. (** Complementation *) @@ -400,7 +400,7 @@ Lemma andb_negb_r : forall b:bool, b && negb b = false. Proof. destr_bool. Qed. -Hint Resolve andb_negb_r: bool v62. +Hint Resolve andb_negb_r: bool. Notation andb_neg_b := andb_negb_r (only parsing). @@ -418,7 +418,7 @@ Proof. destr_bool. Qed. -Hint Resolve andb_comm andb_assoc: bool v62. +Hint Resolve andb_comm andb_assoc: bool. (*******************************************) (** * Properties mixing [andb] and [orb] *) @@ -688,7 +688,7 @@ Lemma andb_prop_intro : Proof. destr_bool; tauto. Qed. -Hint Resolve andb_prop_intro: bool v62. +Hint Resolve andb_prop_intro: bool. Notation andb_true_intro2 := (fun b1 b2 H1 H2 => andb_prop_intro b1 b2 (conj H1 H2)) @@ -699,7 +699,7 @@ Lemma andb_prop_elim : Proof. destr_bool; auto. Qed. -Hint Resolve andb_prop_elim: bool v62. +Hint Resolve andb_prop_elim: bool. Notation andb_prop2 := andb_prop_elim (only parsing). diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 11f3d1d6..4257b4bc 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -12,7 +12,7 @@ Inductive IfProp (A B:Prop) : bool -> Prop := | Iftrue : A -> IfProp A B true | Iffalse : B -> IfProp A B false. -Hint Resolve Iftrue Iffalse: bool v62. +Hint Resolve Iftrue Iffalse: bool. Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A. destruct 1; intros; auto with bool. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index c41eb2fa..1cfca416 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -452,7 +452,7 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in @@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive Section Normalize. Context (A : Type). - Class Normalizes (m : crelation A) (m' : crelation A) : Prop := + Class Normalizes (m : crelation A) (m' : crelation A) := normalizes : relation_equivalence m m'. (** Current strategy: add [flip] everywhere and reduce using [subrelation] diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c4588947..80b0b7e4 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1. -Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1. -Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. Next Obligation. Proof. intros A R sa x y z Hxy Hyz. @@ -123,7 +123,7 @@ Section Respecting. End Respecting. -(** The default equivalence on function spaces, with higher-priority than [eq]. *) +(** The default equivalence on function spaces, with higher priority than [eq]. *) Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : Reflexive (pointwise_relation A eqB) | 9. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 8d942d90..06511ace 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -465,12 +465,12 @@ Ltac partial_application_tactic := let rec do_partial_apps H m cont := match m with | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; - [(do_partial_apps H m' ltac:idtac)|clear H] + [(do_partial_apps H m' ltac:(idtac))|clear H] | _ => cont end in let rec do_partial H ar m := - match ar with + lazymatch ar with | 0%nat => do_partial_apps H m ltac:(fail 1) | S ?n' => match m with @@ -483,7 +483,7 @@ Ltac partial_application_tactic := let n := fresh in evar (n:nat) ; let v := eval compute in n in clear n ; let H := fresh in - assert(H:Params m' v) by typeclasses eauto ; + assert(H:Params m' v) by (subst m'; once typeclasses eauto) ; let v' := eval compute in v in subst m'; (sk H v' || fail 1)) || fk diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index cbde5f9a..8d1c4982 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -43,6 +43,9 @@ Generalizable Variables A B RA RB Ri Ro f. Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A := fun a a' => R (f a) (f a'). +(** Instances on RelCompFun must match syntactically *) +Typeclasses Opaque RelCompFun. + Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope. Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope. @@ -65,6 +68,8 @@ Instance snd_measure : @Measure (A * B) B Snd. Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) := relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2). +Typeclasses Opaque RelProd. + Infix "*" := RelProd : signature_scope. Section RelCompFun_Instances. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 145d451f..190397ae 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "by" tactic3(t) := - setoidreplace (default_relation x y) ltac:t. + setoidreplace (default_relation x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (default_relation x y) ltac:t o. + setoidreplaceat (default_relation x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (default_relation x y) id ltac:t. + setoidreplacein (default_relation x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (default_relation x y) id ltac:t o. + setoidreplaceinat (default_relation x y) id ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) := @@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "by" tactic3(t) := - setoidreplace (rel x y) ltac:t. + setoidreplace (rel x y) ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceat (rel x y) ltac:t o. + setoidreplaceat (rel x y) ltac:(t) o. Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) @@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "by" tactic3(t) := - setoidreplacein (rel x y) id ltac:t. + setoidreplacein (rel x y) id ltac:(t). Tactic Notation "setoid_replace" constr(x) "with" constr(y) "using" "relation" constr(rel) "in" hyp(id) "at" int_or_var_list(o) "by" tactic3(t) := - setoidreplaceinat (rel x y) id ltac:t o. + setoidreplaceinat (rel x y) id ltac:(t) o. (** The [add_morphism_tactic] tactic is run at each [Add Morphism] command before giving the hand back to the user to discharge the diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 90083b00..a3e23f91 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -7,6 +7,10 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.4 *) + +(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *) +Require Export Coq.Compat.Coq85. + (** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *) (** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available. But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *) Require Coq.omega.Omega. @@ -15,21 +19,31 @@ Ltac omega := Coq.omega.Omega.omega. (** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *) Global Set Asymmetric Patterns. +(** The automatic elimination schemes for records were dropped by default in 8.5. This restores the default behavior of Coq 8.4. *) +Global Set Nonrecursive Elimination Schemes. + (** See bug 3545 *) Global Set Universal Lemma Under Conjunction. -(** In 8.5, [refine] leaves over dependent subgoals. *) -Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable. +(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *) +Global Unset Refolding Reduction. (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *) -Ltac constructor_84 := constructor. Ltac constructor_84_n n := constructor n. Ltac constructor_84_tac tac := once (constructor; tac). -Tactic Notation "constructor" := constructor_84. +Tactic Notation "constructor" := Coq.Init.Notations.constructor. Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac. +(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *) +Ltac econstructor_84_n n := econstructor n. +Ltac econstructor_84_tac tac := once (econstructor; tac). + +Tactic Notation "econstructor" := Coq.Init.Notations.econstructor. +Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n. +Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac. + (** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *) Tactic Notation "reflexivity" := reflexivity. Tactic Notation "assumption" := assumption. @@ -45,29 +59,21 @@ Tactic Notation "left" := left. Tactic Notation "eleft" := eleft. Tactic Notation "right" := right. Tactic Notation "eright" := eright. -Tactic Notation "constructor" := constructor. -Tactic Notation "econstructor" := econstructor. Tactic Notation "symmetry" := symmetry. Tactic Notation "split" := split. Tactic Notation "esplit" := esplit. -Global Set Regular Subst Tactic. - -(** Some names have changed in the standard library, so we add aliases. *) -Require Coq.ZArith.Int. -Module Export Coq. - Module Export ZArith. - Module Int. - Module Z_as_Int. - Include Coq.ZArith.Int.Z_as_Int. - (* FIXME: Should these get a (compat "8.4")? Or be moved to Z_as_Int, probably? *) - Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing). - Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing). - Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing). - End Z_as_Int. - End Int. - End ZArith. -End Coq. - (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *) Require Coq.Numbers.Natural.Peano.NPeano. + +(** The following coercions were declared by default in Specif.v. *) +Coercion sig_of_sig2 : sig2 >-> sig. +Coercion sigT_of_sigT2 : sigT2 >-> sigT. +Coercion sigT_of_sig : sig >-> sigT. +Coercion sig_of_sigT : sigT >-> sig. +Coercion sigT2_of_sig2 : sig2 >-> sigT2. +Coercion sig2_of_sigT2 : sigT2 >-> sig2. + +(** In 8.4, the statement of admitted lemmas did not depend on the section + variables. *) +Unset Keep Admitted Variables. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 6e2b3564..64ba6b1e 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -7,3 +7,30 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.5 *) + +(** Any compatibility changes to make future versions of Coq behave like Coq 8.6 + are likely needed to make them behave like Coq 8.5. *) +Require Export Coq.Compat.Coq86. + +(** We use some deprecated options in this file, so we disable the + corresponding warning, to silence the build of this file. *) +Local Set Warnings "-deprecated-option". + +(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not + behave as "intros [H|H]" but leave instead hypotheses quantified in + the goal, here producing subgoals A->C and B->C. *) + +Global Unset Bracketing Last Introduction Pattern. +Global Unset Regular Subst Tactic. +Global Unset Structural Injection. +Global Unset Shrink Abstract. +Global Unset Shrink Obligations. +Global Set Refolding Reduction. + +(** The resolution algorithm for type classes has changed. *) +Global Set Typeclasses Legacy Resolution. +Global Set Typeclasses Limit Intros. +Global Unset Typeclasses Filtered Unification. + +(** Allow silently letting unification constraints float after a "." *) +Global Unset Solve Unification Constraints. diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v new file mode 100644 index 00000000..6952fdf1 --- /dev/null +++ b/theories/Compat/Coq86.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). +Notation option_map := option_map (compat "8.4"). + Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -1986,7 +1988,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H; clear H; intros; subst. + injection H as -> ->. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2050,10 +2052,10 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H; intros; subst. - inversion_clear H1. + destruct p; injection H as -> ->; intros H4. + inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. - inversion_clear H4. + inversion_clear H4. rename H1 into H3. rewrite (@InfA_alt _ eqke) in H3; eauto with *. apply (H3 (y,x0)); auto. Qed. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 13cb559b..5acdb7eb 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -8,7 +8,7 @@ (** * Finite map library *) -(** This file proposes an implementation of the non-dependant interface +(** This file proposes an implementation of the non-dependent interface [FMapInterface.S] using lists of pairs ordered (increasing) with respect to left projection. *) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 9e59f0c5..b1c0fdaa 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -274,8 +274,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H; - intro EQ; rewrite EQ; right; apply in_eq. + rewrite append_neutral_r; apply in_or_app; injection H as ->; + right; apply in_eq. rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. congruence. @@ -315,7 +315,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + injection H1 as -> ->; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -346,7 +346,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq. + injection H1 as -> ->; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -689,7 +689,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. - injection H0; clear H0; intros _ H0; subst. + injection H0 as H0 _; subst. eapply xelements_bits_lt_1; eauto. apply E.bits_lt_trans with p. eapply xelements_bits_lt_1; eauto. diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 0f11dd7a..130cbee8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -8,7 +8,7 @@ (** * Finite map library *) -(** This file proposes an implementation of the non-dependant interface +(** This file proposes an implementation of the non-dependent interface [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *) Require Import FMapInterface. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index ad067eb3..1db6a71e 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -357,17 +357,8 @@ the above form: | _ => idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (FSet_Prop P) holds by + tryif prop (FSet_Prop P) holds by (auto 100 with FSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (FSet_elt_Prop P) holds by + tryif prop (FSet_elt_Prop P) holds by (auto 100 with FSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index 1f36306c..9c3ec71a 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [FSetInterface.S] using strictly ordered list. *) Require Export FSetInterface. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 7398c6d6..507f1cda 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -1007,10 +1007,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H; intros; subst; clear H. apply Hp. + intros p Hp x H. injection H as <-. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H; intros; subst; clear H. apply Hp. + intros p Hp H. injection H as <-. apply Hp. reflexivity. intros. discriminate. Qed. @@ -1066,11 +1066,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (min_elt r); simpl in *. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. discriminate. Qed. @@ -1094,15 +1094,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1119,11 +1119,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (max_elt l); simpl in *. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. discriminate. Qed. @@ -1147,15 +1147,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 2ea32e97..9dbea884 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [FSetInterface.WS] using lists without redundancy. *) Require Import FSetInterface. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 4850c9ca..ddaf08bf 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -151,6 +151,7 @@ Inductive option (A:Type) : Type := | Some : A -> option A | None : option A. +Arguments Some {A} a. Arguments None {A}. Definition option_map (A B:Type) (f:A->B) (o : option A) : option B := @@ -225,6 +226,7 @@ Inductive list (A : Type) : Type := | cons : A -> list A -> list A. Arguments nil {A}. +Arguments cons {A} a l. Infix "::" := cons (at level 60, right associativity) : list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 4a5f2ad6..4536dfc0 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -64,7 +64,7 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate identity_sym not_identity_sym: core v62. +Hint Immediate identity_sym not_identity_sym: core. Notation refl_id := identity_refl (compat "8.3"). Notation sym_id := identity_sym (compat "8.3"). diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index ab6bf472..48fbe079 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -76,17 +76,21 @@ Reserved Notation "{ x : A & P }" (at level 0, x at level 99). Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99). Delimit Scope type_scope with type. +Delimit Scope function_scope with function. Delimit Scope core_scope with core. +Bind Scope type_scope with Sortclass. +Bind Scope function_scope with Funclass. + Open Scope core_scope. +Open Scope function_scope. Open Scope type_scope. (** ML Tactic Notations *) Declare ML Module "coretactics". Declare ML Module "extratactics". -Declare ML Module "eauto". +Declare ML Module "g_auto". Declare ML Module "g_class". Declare ML Module "g_eqdecide". Declare ML Module "g_rewrite". -Declare ML Module "tauto". diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 3749baf6..6c4a6350 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -33,7 +33,6 @@ Open Scope nat_scope. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). -Hint Resolve eq_S: v62. Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -41,7 +40,6 @@ Hint Resolve f_equal_nat: core. Notation pred := Nat.pred (compat "8.4"). Definition f_equal_pred := f_equal pred. -Hint Resolve f_equal_pred: v62. Theorem pred_Sn : forall n:nat, n = pred (S n). Proof. @@ -85,7 +83,6 @@ Notation plus := Nat.add (compat "8.4"). Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. -Hint Resolve f_equal2_plus: v62. Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). Hint Resolve f_equal2_nat: core. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 04a263ad..03f2328d 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -15,6 +15,7 @@ Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. +Require Export Coq.Init.Tauto. (* Initially available plugins (+ nat_syntax_plugin loaded in Datatypes) *) Declare ML Module "extraction_plugin". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 6c022185..9fc00e80 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -9,6 +9,7 @@ (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. +Set Reversible Pattern Implicit. Require Import Notations. Require Import Datatypes. @@ -298,7 +299,7 @@ Proof. apply (h2 h1). Defined. -Hint Resolve left right inleft inright: core v62. +Hint Resolve left right inleft inright: core. Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 59fdbb42..5d1e87ae 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -55,12 +55,6 @@ Ltac contradict H := | _ => (elim H;fail) || pos H end. -(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*) - -Ltac swap H := - idtac "swap is OBSOLETE: use contradict instead."; - intro; apply H; clear H. - (* To contradict an hypothesis without copying its type. *) Ltac absurd_hyp H := @@ -79,7 +73,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). +Ltac destr_eq H := discriminate H || (try (injection H as H)). (* Similar variants of destruct *) diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v new file mode 100644 index 00000000..1e409607 --- /dev/null +++ b/theories/Init/Tauto.v @@ -0,0 +1,101 @@ +Require Import Notations. +Require Import Datatypes. +Require Import Logic. + +Local Declare ML Module "tauto". + +Local Ltac not_dep_intros := + repeat match goal with + | |- (forall (_: ?X1), ?X2) => intro + | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro + end. + +Local Ltac axioms flags := + match reverse goal with + | |- ?X1 => is_unit_or_eq flags X1; constructor 1 + | _:?X1 |- _ => is_empty flags X1; elimtype X1; assumption + | _:?X1 |- ?X1 => assumption + end. + +Local Ltac simplif flags := + not_dep_intros; + repeat + (match reverse goal with + | id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id + | id: (Coq.Init.Logic.not _) |- _ => red in id + | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id + | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ => + (* generalize (id0 id1); intro; clear id0 does not work + (see Marco Maggiesi's bug PR#301) + so we instead use Assert and exact. *) + assert X2; [exact (id0 id1) | clear id0] + | id: forall (_ : ?X1), ?X2|- _ => + is_unit_or_eq flags X1; cut X2; + [ intro; clear id + | (* id : forall (_: ?X1), ?X2 |- ?X2 *) + cut X1; [exact id| constructor 1; fail] + ] + | id: forall (_ : ?X1), ?X2|- _ => + flatten_contravariant_conj flags X1 X2 id + (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *) + | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ => + assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3) + by (do 2 intro; apply id; split; assumption); + clear id + | id: forall (_:?X1), ?X2|- _ => + flatten_contravariant_disj flags X1 X2 id + (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *) + | |- ?X1 => is_conj flags X1; split + | |- (Coq.Init.Logic.iff _ _) => split + | |- (Coq.Init.Logic.not _) => red + end; + not_dep_intros). + +Local Ltac tauto_intuit flags t_reduce t_solver := + let rec t_tauto_intuit := + (simplif flags; axioms flags + || match reverse goal with + | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (forall (_: X1), X2); + [ exact id + | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; + solve [ t_tauto_intuit ]]] + | id:forall (_:not ?X1), ?X3|- _ => + cut X3; + [ intro; clear id; t_tauto_intuit + | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]] + | |- ?X1 => + is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit] + end + || + (* NB: [|- _ -> _] matches any product *) + match goal with | |- forall (_ : _), _ => intro; t_tauto_intuit + | |- _ => t_reduce;t_solver + end + || + t_solver + ) in t_tauto_intuit. + +Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver. +Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed". +Local Ltac tauto_classical flags := + (apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed"). +Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags. + +Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags). +Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags). + +Ltac intuition := with_uniform_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac). + +Ltac dintuition := with_power_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)). +Local Ltac dintuition_then tac := with_power_flags ltac:(fun flags => intuition_gen flags tac). + +Tactic Notation "intuition" := intuition. +Tactic Notation "intuition" tactic(t) := intuition_then t. + +Tactic Notation "dintuition" := dintuition. +Tactic Notation "dintuition" tactic(t) := dintuition_then t. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 985ecaf2..b5b17e5e 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -34,7 +34,7 @@ Section Well_founded. destruct 1; trivial. Defined. - Global Implicit Arguments Acc_inv [x y] [x]. + Global Arguments Acc_inv [x] _ [y] _, [x] _ y _. (** A relation is well-founded if every element is accessible *) diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget index cc62e66c..99877065 100644 --- a/theories/Init/vo.itarget +++ b/theories/Init/vo.itarget @@ -7,4 +7,5 @@ Prelude.vo Specif.vo Tactics.vo Wf.vo -Nat.vo \ No newline at end of file +Nat.vo +Tauto.vo diff --git a/theories/Lists/List.v b/theories/Lists/List.v index cc7586fe..30f1dec2 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -7,7 +7,7 @@ (************************************************************************) Require Setoid. -Require Import PeanoNat Le Gt Minus Bool. +Require Import PeanoNat Le Gt Minus Bool Lt. Set Implicit Arguments. (* Set Universe Polymorphism. *) @@ -21,12 +21,13 @@ Set Implicit Arguments. Open Scope list_scope. -(** Standard notations for lists. +(** Standard notations for lists. In a special module to avoid conflicts. *) Module ListNotations. -Notation " [ ] " := nil (format "[ ]") : list_scope. -Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +Notation "[ ]" := nil (format "[ ]") : list_scope. +Notation "[ x ]" := (cons x nil) : list_scope. +Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope. End ListNotations. Import ListNotations. @@ -195,7 +196,7 @@ Section Facts. Qed. Theorem app_nil_r : forall l:list A, l ++ [] = l. - Proof. + Proof. induction l; simpl; f_equal; auto. Qed. @@ -248,8 +249,7 @@ Section Facts. generalize (app_nil_r l); intros E. rewrite -> E; auto. intros. - injection H. - intro. + injection H as H H0. assert ([] = l ++ a0 :: l0) by auto. apply app_cons_not_nil in H1 as []. Qed. @@ -335,16 +335,16 @@ Section Facts. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H; clear H; intros; f_equal; eauto. + injection H as H H0; f_equal; eauto. Qed. End Facts. -Hint Resolve app_assoc app_assoc_reverse: datatypes v62. -Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62. -Hint Immediate app_eq_nil: datatypes v62. -Hint Resolve app_eq_unit app_inj_tail: datatypes v62. -Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62. +Hint Resolve app_assoc app_assoc_reverse: datatypes. +Hint Resolve app_comm_cons app_cons_not_nil: datatypes. +Hint Immediate app_eq_nil: datatypes. +Hint Resolve app_eq_unit app_inj_tail: datatypes. +Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes. @@ -518,7 +518,7 @@ Section Elts. Proof. revert l. induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. - - exists nil; exists l. injection H; clear H; intros; now subst. + - exists nil; exists l. now injection H as ->. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed. @@ -1385,9 +1385,8 @@ End Fold_Right_Recursor. Lemma combine_split : forall (l:list A)(l':list B), length l = length l' -> split (combine l l') = (l,l'). Proof. - induction l; destruct l'; simpl; intros; auto; try discriminate. - injection H; clear H; intros. - rewrite IHl; auto. + induction l, l'; simpl; trivial; try discriminate. + now intros [= ->%IHl]. Qed. Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B), @@ -1471,7 +1470,7 @@ End Fold_Right_Recursor. destruct (in_app_or _ _ _ H); clear H. destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2; clear H2; intros; subst; intuition. + injection H2 as -> ->; intuition. intuition. Qed. @@ -1545,7 +1544,7 @@ Section length_order. End length_order. Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: - datatypes v62. + datatypes. (******************************) @@ -1614,7 +1613,7 @@ Section SetIncl. End SetIncl. Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons - incl_app: datatypes v62. + incl_app: datatypes. (**************************************) @@ -1634,6 +1633,80 @@ Section Cutting. end end. + Lemma firstn_nil n: firstn n [] = []. + Proof. induction n; now simpl. Qed. + + Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l). + Proof. now simpl. Qed. + + Lemma firstn_all l: firstn (length l) l = l. + Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed. + + Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l. + Proof. induction n as [|k iHk]. + - intro. inversion 1 as [H1|?]. + rewrite (length_zero_iff_nil l) in H1. subst. now simpl. + - destruct l as [|x xs]; simpl. + * now reflexivity. + * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H. + Qed. + + Lemma firstn_O l: firstn 0 l = []. + Proof. now simpl. Qed. + + Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n. + Proof. + induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl]. + - auto with arith. + - apply Peano.le_n_S, iHk. + Qed. + + Lemma firstn_length_le: forall l:list A, forall n:nat, + n <= length l -> length (firstn n l) = n. + Proof. induction l as [|x xs Hrec]. + - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl. + - destruct n. + * now simpl. + * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H). + Qed. + + Lemma firstn_app n: + forall l1 l2, + firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2). + Proof. induction n as [|k iHk]; intros l1 l2. + - now simpl. + - destruct l1 as [|x xs]. + * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O. + * rewrite <- app_comm_cons. simpl. f_equal. apply iHk. + Qed. + + Lemma firstn_app_2 n: + forall l1 l2, + firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2. + Proof. induction n as [| k iHk];intros l1 l2. + - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r. + rewrite firstn_app. rewrite <- minus_diag_reverse. + unfold firstn at 2. rewrite app_nil_r. apply firstn_all. + - destruct l2 as [|x xs]. + * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith. + * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k). + auto with arith. + rewrite H0, firstn_all2; [reflexivity | auto with arith]. + Qed. + + Lemma firstn_firstn: + forall l:list A, + forall i j : nat, + firstn i (firstn j l) = firstn (min i j) l. + Proof. induction l as [|x xs Hl]. + - intros. simpl. now rewrite ?firstn_nil. + - destruct i. + * intro. now simpl. + * destruct j. + + now simpl. + + simpl. f_equal. apply Hl. + Qed. + Fixpoint skipn (n:nat)(l:list A) : list A := match n with | 0 => l @@ -2292,7 +2365,7 @@ Notation rev_acc := rev_append (only parsing). Notation rev_acc_rev := rev_append_rev (only parsing). Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) -Hint Resolve app_nil_end : datatypes v62. +Hint Resolve app_nil_end : datatypes. (* end hide *) Section Repeat. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index fd0464fb..655d3940 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -48,7 +48,11 @@ Section first_definitions. end end. - (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *) + (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing. + Invariant: any element should occur at most once in [x], see for + instance [set_add]. We hence remove here only the first occurrence + of [a] in [x]. *) + Fixpoint set_remove (a:A) (x:set) : set := match x with | nil => empty_set @@ -227,6 +231,68 @@ Section first_definitions. intros; elim (Aeq_dec a a0); intros; discriminate. Qed. + Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l. + Proof. + split. apply set_add_elim. apply set_add_intro. + Qed. + + Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor; [ tauto | constructor ]. + - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial. + rewrite set_add_iff. intuition. + Qed. + + Lemma set_remove_1 (a b : A) (l : set) : + In a (set_remove b l) -> In a l. + Proof. + induction l as [|x xs Hrec]. + - intros. auto. + - simpl. destruct (Aeq_dec b x). + * tauto. + * intro H. destruct H. + + rewrite H. apply in_eq. + + apply in_cons. apply Hrec. assumption. + Qed. + + Lemma set_remove_2 (a b:A) (l : set) : + NoDup l -> In a (set_remove b l) -> a <> b. + Proof. + induction l as [|x l IH]; intro ND; simpl. + - tauto. + - inversion_clear ND. + destruct (Aeq_dec b x) as [<-|Hbx]. + + congruence. + + destruct 1; subst; auto. + Qed. + + Lemma set_remove_3 (a b : A) (l : set) : + In a l -> a <> b -> In a (set_remove b l). + Proof. + induction l as [|x xs Hrec]. + - now simpl. + - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition. + congruence. + Qed. + + Lemma set_remove_iff (a b : A) (l : set) : + NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b). + Proof. + split; try split. + - eapply set_remove_1; eauto. + - eapply set_remove_2; eauto. + - destruct 1; apply set_remove_3; auto. + Qed. + + Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l). + Proof. + induction 1 as [|x l H H' IH]; simpl. + - constructor. + - destruct (Aeq_dec a x) as [<-|Hax]; trivial. + constructor; trivial. + rewrite set_remove_iff; trivial. intuition. + Qed. Lemma set_union_intro1 : forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y). @@ -264,18 +330,26 @@ Section first_definitions. tauto. Qed. + Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'. + Proof. + split. apply set_union_elim. apply set_union_intro. + Qed. + + Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l'). + Proof. + induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup. + Qed. + Lemma set_union_emptyL : forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_union_emptyR : forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x. intros a x H; case (set_union_elim _ _ _ H); auto || contradiction. Qed. - Lemma set_inter_intro : forall (a:A) (x y:set), set_In a x -> set_In a y -> set_In a (set_inter x y). @@ -326,6 +400,21 @@ Section first_definitions. eauto with datatypes. Qed. + Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'. + Proof. + split. + - apply set_inter_elim. + - destruct 1. now apply set_inter_intro. + Qed. + + Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto. + constructor; auto. rewrite set_inter_iff; tauto. + Qed. + Lemma set_diff_intro : forall (a:A) (x y:set), set_In a x -> ~ set_In a y -> set_In a (set_diff x y). @@ -360,6 +449,20 @@ Section first_definitions. rewrite H; trivial. Qed. + Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'. + Proof. + split. + - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto. + - destruct 1. now apply set_diff_intro. + Qed. + + Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l'). + Proof. + induction 1 as [|x l H H' IH]; intro Hl'; simpl. + - constructor. + - destruct (set_mem x l'); auto using set_add_nodup. + Qed. + Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x). red; intros a x H. apply (set_diff_elim2 _ _ _ H). diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 7ec3d250..1c302b22 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -51,7 +51,7 @@ Lemma tl_nth_tl : Proof. simple induction n; simpl; auto. Qed. -Hint Resolve tl_nth_tl: datatypes v62. +Hint Resolve tl_nth_tl: datatypes. Lemma Str_nth_tl_plus : forall (n m:nat) (s:Stream), diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index c947062a..afd64efd 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -34,6 +34,8 @@ Table of contents: 3 3. Independence of general premises and drinker's paradox +4. Classical logic and principle of unrestricted minimization + *) (************************************************************************) @@ -658,3 +660,79 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. + +(** ** Principle of unrestricted minimization *) + +Require Import Coq.Arith.PeanoNat. + +Definition Minimal (P:nat -> Prop) (n:nat) : Prop := + P n /\ forall k, P k -> n<=k. + +Definition Minimization_Property (P : nat -> Prop) : Prop := + forall n, P n -> exists m, Minimal P m. + +Section Unrestricted_minimization_entails_excluded_middle. + + Hypothesis unrestricted_minimization: forall P, Minimization_Property P. + + Theorem unrestricted_minimization_entails_excluded_middle : forall A, A\/~A. + Proof. + intros A. + pose (P := fun n:nat => n=0/\A \/ n=1). + assert (P 1) as h. + { unfold P. intuition. } + assert (P 0 <-> A) as p₀. + { split. + + intros [[_ h₀]|[=]]. assumption. + + unfold P. tauto. } + apply unrestricted_minimization in h as ([|[|m]] & hm & hmm). + + intuition. + + right. + intros HA. apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA. assumption. + + destruct hm as [([=],_) | [=] ]. + Qed. + +End Unrestricted_minimization_entails_excluded_middle. + +Require Import Wf_nat. + +Section Excluded_middle_entails_unrestricted_minimization. + + Hypothesis em : forall A, A\/~A. + + Theorem excluded_middle_entails_unrestricted_minimization : + forall P, Minimization_Property P. + Proof. + intros P n HPn. + assert (dec : forall n, P n \/ ~ P n) by auto using em. + assert (ex : exists n, P n) by (exists n; assumption). + destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _). + exists n'. assumption. + Qed. + +End Excluded_middle_entails_unrestricted_minimization. + +(** However, minimization for a given predicate does not necessarily imply + decidability of this predicate *) + +Section Example_of_undecidable_predicate_with_the_minimization_property. + + Variable s : nat -> bool. + + Let P n := exists k, n<=k /\ s k = true. + + Example undecidable_predicate_with_the_minimization_property : + Minimization_Property P. + Proof. + unfold Minimization_Property. + intros h hn. + exists 0. split. + + unfold P in *. destruct hn as (k&hk₁&hk₂). + exists k. split. + * rewrite <- hk₁. + apply PeanoNat.Nat.le_0_l. + * assumption. + + intros **. apply PeanoNat.Nat.le_0_l. + Qed. + +End Example_of_undecidable_predicate_with_the_minimization_property. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 2ba7253c..8b6054f9 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -50,7 +50,7 @@ Qed. Theorem dec_iff : forall A B:Prop, decidable A -> decidable B -> decidable (A<->B). Proof. -unfold decidable; tauto. +unfold decidable. tauto. Qed. Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P. diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index f3a2783e..5ef86b8e 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -33,5 +33,5 @@ Export EqdepTheory. (** Exported hints *) -Hint Resolve eq_dep_eq: eqdep v62. +Hint Resolve eq_dep_eq: eqdep. Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c..bd59159b 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 8ded7476..841f843c 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -631,6 +631,8 @@ End NoRetractFromTypeToProp. Module TypeNeqSmallType. +Unset Universe Polymorphism. + Section Paradox. (** ** Universe [U] is equal to one of its elements. *) @@ -655,7 +657,6 @@ Proof. reflexivity. Qed. - Theorem paradox : False. Proof. Generic.paradox p. diff --git a/theories/Logic/PropFacts.v b/theories/Logic/PropFacts.v new file mode 100644 index 00000000..309539e5 --- /dev/null +++ b/theories/Logic/PropFacts.v @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Prop) + (inj : forall A B, (f A <-> f B) -> (A <-> B)) + (ext : forall A B, A <-> B -> f A <-> f B) + : forall A, f (f A) <-> A. +Proof. +intros. +enough (f (f (f A)) <-> f A) by (apply inj; assumption). +split; intro H. +- now_show (f A). + enough (f A <-> True) by firstorder. + enough (f (f A) <-> f True) by (apply inj; assumption). + split; intro H'. + + now_show (f True). + enough (f (f (f A)) <-> f True) by firstorder. + apply ext; firstorder. + + now_show (f (f A)). + enough (f (f A) <-> True) by firstorder. + apply inj; firstorder. +- now_show (f (f (f A))). + enough (f A <-> f (f (f A))) by firstorder. + apply ext. + split; intro H'. + + now_show (f (f A)). + enough (f A <-> f (f A)) by firstorder. + apply ext; firstorder. + + now_show A. + enough (f A <-> A) by firstorder. + apply inj; firstorder. +Defined. diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index cc023cc3..a3c265a2 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -417,6 +417,7 @@ Local Open Scope Int_scope. Let's do its job by hand: *) Ltac join_tac := + let l := fresh "l" in intro l; induction l as [| lh ll _ lx lr Hlr]; [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join; [ | destruct ((rh+2) idtac end. - (** [if t then t1 else t2] executes [t] and, if it does not - fail, then [t1] will be applied to all subgoals - produced. If [t] fails, then [t2] is executed. *) - Tactic Notation - "if" tactic(t) - "then" tactic(t1) - "else" tactic(t2) := - first [ t; first [ t1 | fail 2 ] | t2 ]. - Ltac abstract_term t := - if (is_var t) then fail "no need to abstract a variable" + tryif (is_var t) then fail "no need to abstract a variable" else (let x := fresh "x" in set (x := t) in *; try clearbody x). Ltac abstract_elements := @@ -478,11 +469,11 @@ the above form: repeat ( match goal with | H : context [ @Logic.eq ?T ?x ?y ] |- _ => - if (change T with E.t in H) then fail - else if (change T with t in H) then fail + tryif (change T with E.t in H) then fail + else tryif (change T with t in H) then fail else clear H | H : ?P |- _ => - if prop (MSet_Prop P) holds by + tryif prop (MSet_Prop P) holds by (auto 100 with MSet_Prop) then fail else clear H @@ -747,7 +738,7 @@ the above form: | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False => contradict H; fsetdec_body | H: ?P -> False |- ?Q -> False => - if prop (MSet_elt_Prop P) holds by + tryif prop (MSet_elt_Prop P) holds by (auto 100 with MSet_Prop) then (contradict H; fsetdec_body) else fsetdec_body diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index bd881168..74a7f6df 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -345,6 +345,9 @@ Module Type WRawSets (E : DecidableType). predicate [Ok]. If [Ok] isn't decidable, [isok] may be the always-false function. *) Parameter isok : t -> bool. + (** MS: + Dangerous instance, the [isok s = true] hypothesis cannot be discharged + with typeclass resolution. Is it really an instance? *) Declare Instance isok_Ok s `(isok s = true) : Ok s | 10. (** Logical predicates *) diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index fb0d1ad9..05c20eb8 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [MSetInterface.S] using strictly ordered list. *) Require Export MSetInterface OrdersFacts OrdersLists. diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index 8dd240f4..be95a037 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -908,10 +908,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H; intros; subst; clear H. apply Hp. + intros p Hp x H. injection H as <-. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H; intros; subst; clear H. apply Hp. + intros p Hp H. injection H as <-. apply Hp. reflexivity. intros. discriminate. Qed. @@ -968,11 +968,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (min_elt r); simpl in *. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. discriminate. Qed. @@ -996,15 +996,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1021,11 +1021,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H. intros <-. apply IHr. reflexivity. + injection H as <-. apply IHr. reflexivity. destruct o; simpl. - injection H. intros <-. reflexivity. + injection H as <-. reflexivity. destruct (max_elt l); simpl in *. - injection H. intros <-. apply IHl. reflexivity. + injection H as <-. apply IHl. reflexivity. discriminate. Qed. @@ -1049,15 +1049,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H; intros <-. + intros p Hp. rewrite Hp in H. injection H as <-. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp. destruct o. - injection H. intros <- Hl. clear H. + injection H as <-. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H. intros <-. clear H. + injection H as <-. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index 751d4f35..83a2343d 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -911,7 +911,7 @@ Proof. { inversion_clear O. assert (InT x l) by now apply min_elt_spec1. auto. } simpl. case X.compare_spec; try order. - destruct lc; injection E; clear E; intros; subst l s0; auto. + destruct lc; injection E; subst l s0; auto. Qed. Lemma remove_min_spec1 s x s' `{Ok s}: @@ -1948,7 +1948,7 @@ Module Make (X: Orders.OrderedType) <: generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. - intros H U. injection U. clear U; intros; subst. simpl. + intros H U. injection U as -> <-. simpl. destruct (H x s0); auto. subst; intuition. Qed. diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 372acd56..2ac57a93 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -8,7 +8,7 @@ (** * Finite sets library *) -(** This file proposes an implementation of the non-dependant +(** This file proposes an implementation of the non-dependent interface [MSetWeakInterface.S] using lists without redundancy. *) Require Import MSetInterface. diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 45a7527c..bd893087 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -10,7 +10,7 @@ (** * BigNumPrelude *) -(** Auxillary functions & theorems used for arbitrary precision efficient +(** Auxiliary functions & theorems used for arbitrary precision efficient numbers. *) @@ -22,7 +22,7 @@ Require Export Zpow_facts. Declare ML Module "numbers_syntax_plugin". (* *** Nota Bene *** - All results that were general enough has been moved in ZArith. + All results that were general enough have been moved in ZArith. Only remain here specialized lemmas and compatibility elements. (P.L. 5/11/2007). *) diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index 215b8bd5..d160f5f1 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -19,13 +19,13 @@ Local Open Scope list_scope. Ltac isInt31cst_lst l := match l with - | nil => constr:true + | nil => constr:(true) | ?t::?l => match t with | D1 => isInt31cst_lst l | D0 => isInt31cst_lst l - | _ => constr:false + | _ => constr:(false) end - | _ => constr:false + | _ => constr:(false) end. Ltac isInt31cst t := @@ -38,17 +38,17 @@ Ltac isInt31cst t := ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20 ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil) in isInt31cst_lst l - | Int31.On => constr:true - | Int31.In => constr:true - | Int31.Tn => constr:true - | Int31.Twon => constr:true - | _ => constr:false + | Int31.On => constr:(true) + | Int31.In => constr:(true) + | Int31.Tn => constr:(true) + | Int31.Twon => constr:(true) + | _ => constr:(false) end. Ltac Int31cst t := match isInt31cst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** The generic ring structure inferred from the Cyclic structure *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index c115a831..04fc5a8d 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -369,7 +369,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H; clear H; intros. + destruct 1; injection H as ? ?. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -411,7 +411,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1; clear H1; intros. + injection H1 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -522,7 +522,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4; clear H4; intros. + injection H4 as ? ?. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcf..c2fa69e5 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index ec495d09..7c76011f 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -138,7 +138,7 @@ intros NEQ. generalize (BigZ.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigZ.zify. rewrite EQr, EQq; auto. Qed. @@ -148,26 +148,26 @@ Ltac isBigZcst t := match t with | BigZ.Pos ?t => isBigNcst t | BigZ.Neg ?t => isBigNcst t - | BigZ.zero => constr:true - | BigZ.one => constr:true - | BigZ.two => constr:true - | BigZ.minus_one => constr:true - | _ => constr:false + | BigZ.zero => constr:(true) + | BigZ.one => constr:(true) + | BigZ.two => constr:(true) + | BigZ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigZcst t := match isBigZcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigZ_to_N t := match t with | BigZ.Pos ?t => BigN_to_N t - | BigZ.zero => constr:0%N - | BigZ.one => constr:1%N - | BigZ.two => constr:2%N - | _ => constr:NotConstant + | BigZ.zero => constr:(0%N) + | BigZ.one => constr:(1%N) + | BigZ.two => constr:(2%N) + | _ => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 8673b8a5..fec6e068 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType. Proof. apply Bool.eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min n m := match compare n m with Gt => m | _ => n end. @@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType. (* Pos Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos py) with (Zneg py). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType. (* Neg Pos *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr; + try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr; simpl; rewrite Hq, NN.spec_0; auto). change (- Zpos px) with (Zneg px). assert (GT : Zpos py > 0) by (compute; auto). generalize (Z_div_mod (Zpos px) (Zpos py) GT). unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r'). - intros (EQ,MOD). injection 1. intros Hr' Hq'. + intros (EQ,MOD). injection 1 as Hq' Hr'. rewrite NN.spec_eqb, NN.spec_0, Hr'. break_nonneg r pr EQr. subst; simpl. rewrite NN.spec_0; auto. @@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType. (* Neg Neg *) generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r). break_nonneg x px EQx; break_nonneg y py EQy; - try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto). + try (injection 1 as -> ->; auto). simpl. intros <-; auto. Qed. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 1d367294..44088f8c 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -60,8 +60,6 @@ Proof. intros n. exists 0. now nzsimpl. Qed. -Hint Rewrite divide_1_l divide_0_r : nz. - Lemma divide_0_l : forall n, (0 | n) -> n==0. Proof. intros n (m,Hm). revert Hm. now nzsimpl. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 29a1145e..e8ff516f 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -110,7 +110,7 @@ intros NEQ. generalize (BigN.spec_div_eucl a b). generalize (Z_div_mod_full [a] [b] NEQ). destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r'). -intros (EQ,_). injection 1. intros EQr EQq. +intros (EQ,_). injection 1 as EQr EQq. BigN.zify. rewrite EQr, EQq; auto. Qed. @@ -119,10 +119,10 @@ Qed. Ltac isStaticWordCst t := match t with - | W0 => constr:true + | W0 => constr:(true) | WW ?t1 ?t2 => match isStaticWordCst t1 with - | false => constr:false + | false => constr:(false) | true => isStaticWordCst t2 end | _ => isInt31cst t @@ -139,30 +139,30 @@ Ltac isBigNcst t := | BigN.N6 ?t => isStaticWordCst t | BigN.Nn ?n ?t => match isnatcst n with | true => isStaticWordCst t - | false => constr:false + | false => constr:(false) end - | BigN.zero => constr:true - | BigN.one => constr:true - | BigN.two => constr:true - | _ => constr:false + | BigN.zero => constr:(true) + | BigN.one => constr:(true) + | BigN.two => constr:(true) + | _ => constr:(false) end. Ltac BigNcst t := match isBigNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Ltac BigN_to_N t := match isBigNcst t with | true => eval vm_compute in (BigN.to_N t) - | false => constr:NotConstant + | false => constr:(NotConstant) end. Ltac Ncst t := match isNcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. (** Registration for the "ring" tactic *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736..1425041a 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 601fa108..5177fae6 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -147,7 +147,7 @@ pr pr " Local Notation Size := (SizePlus O)."; pr ""; - pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1); + pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1); pr ""; pr " Definition dom_t n := match n with"; diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 58b1b018..d0168bd9 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,8 +8,88 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import PeanoNat NAxioms. +Require Import PeanoNat Even NAxioms. -(** * [PeanoNat.Nat] already implements [NAxiomSig] *) +(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *) + +(** [PeanoNat.Nat] already implements [NAxiomSig] *) Module Nat <: NAxiomsSig := Nat. + +(** Compat notations for stuff that used to be at the beginning of NPeano. *) + +Notation leb := Nat.leb (compat "8.4"). +Notation ltb := Nat.ltb (compat "8.4"). +Notation leb_le := Nat.leb_le (compat "8.4"). +Notation ltb_lt := Nat.ltb_lt (compat "8.4"). +Notation pow := Nat.pow (compat "8.4"). +Notation pow_0_r := Nat.pow_0_r (compat "8.4"). +Notation pow_succ_r := Nat.pow_succ_r (compat "8.4"). +Notation square := Nat.square (compat "8.4"). +Notation square_spec := Nat.square_spec (compat "8.4"). +Notation Even := Nat.Even (compat "8.4"). +Notation Odd := Nat.Odd (compat "8.4"). +Notation even := Nat.even (compat "8.4"). +Notation odd := Nat.odd (compat "8.4"). +Notation even_spec := Nat.even_spec (compat "8.4"). +Notation odd_spec := Nat.odd_spec (compat "8.4"). + +Lemma Even_equiv n : Even n <-> Even.even n. +Proof. symmetry. apply Even.even_equiv. Qed. +Lemma Odd_equiv n : Odd n <-> Even.odd n. +Proof. symmetry. apply Even.odd_equiv. Qed. + +Notation divmod := Nat.divmod (compat "8.4"). +Notation div := Nat.div (compat "8.4"). +Notation modulo := Nat.modulo (compat "8.4"). +Notation divmod_spec := Nat.divmod_spec (compat "8.4"). +Notation div_mod := Nat.div_mod (compat "8.4"). +Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4"). +Notation sqrt_iter := Nat.sqrt_iter (compat "8.4"). +Notation sqrt := Nat.sqrt (compat "8.4"). +Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4"). +Notation sqrt_spec := Nat.sqrt_spec (compat "8.4"). +Notation log2_iter := Nat.log2_iter (compat "8.4"). +Notation log2 := Nat.log2 (compat "8.4"). +Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4"). +Notation log2_spec := Nat.log2_spec (compat "8.4"). +Notation log2_nonpos := Nat.log2_nonpos (compat "8.4"). +Notation gcd := Nat.gcd (compat "8.4"). +Notation divide := Nat.divide (compat "8.4"). +Notation gcd_divide := Nat.gcd_divide (compat "8.4"). +Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4"). +Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4"). +Notation gcd_greatest := Nat.gcd_greatest (compat "8.4"). +Notation testbit := Nat.testbit (compat "8.4"). +Notation shiftl := Nat.shiftl (compat "8.4"). +Notation shiftr := Nat.shiftr (compat "8.4"). +Notation bitwise := Nat.bitwise (compat "8.4"). +Notation land := Nat.land (compat "8.4"). +Notation lor := Nat.lor (compat "8.4"). +Notation ldiff := Nat.ldiff (compat "8.4"). +Notation lxor := Nat.lxor (compat "8.4"). +Notation double_twice := Nat.double_twice (compat "8.4"). +Notation testbit_0_l := Nat.testbit_0_l (compat "8.4"). +Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4"). +Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4"). +Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4"). +Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4"). +Notation shiftr_spec := Nat.shiftr_spec (compat "8.4"). +Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4"). +Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4"). +Notation div2_bitwise := Nat.div2_bitwise (compat "8.4"). +Notation odd_bitwise := Nat.odd_bitwise (compat "8.4"). +Notation div2_decr := Nat.div2_decr (compat "8.4"). +Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4"). +Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4"). +Notation land_spec := Nat.land_spec (compat "8.4"). +Notation ldiff_spec := Nat.ldiff_spec (compat "8.4"). +Notation lor_spec := Nat.lor_spec (compat "8.4"). +Notation lxor_spec := Nat.lxor_spec (compat "8.4"). + +Infix "<=?" := Nat.leb (at level 70) : nat_scope. +Infix " isBigZcst t | BigQ.Qq ?n ?d => match isBigZcst n with | true => isBigNcst d - | false => constr:false + | false => constr:(false) end - | BigQ.zero => constr:true - | BigQ.one => constr:true - | BigQ.minus_one => constr:true - | _ => constr:false + | BigQ.zero => constr:(true) + | BigQ.one => constr:(true) + | BigQ.minus_one => constr:(true) + | _ => constr:(false) end. Ltac BigQcst t := match isBigQcst t with - | true => constr:t - | false => constr:NotConstant + | true => constr:(t) + | false => constr:(NotConstant) end. Add Field BigQfield : BigQfieldth diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 4ac36425..b9fed9d5 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -1050,13 +1050,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Theorem spec_of_Qc: forall q, [[of_Qc q]] = q. Proof. intros; apply Qc_decomp; simpl; intros. - rewrite strong_spec_of_Qc; auto. + rewrite strong_spec_of_Qc. apply canon. Qed. Theorem spec_oppc: forall q, [[opp q]] = -[[q]]. Proof. intros q; unfold Qcopp, to_Qc, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. rewrite spec_opp, <- Qred_opp, Qred_correct. apply Qeq_refl. @@ -1085,10 +1085,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1099,10 +1099,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] + [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_add_norm; auto. unfold Qcplus, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qplus_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1147,10 +1147,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1161,10 +1161,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x] * [y])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_mul_norm; auto. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1185,10 +1185,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1199,10 +1199,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc (/[x])). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_inv_norm; auto. unfold Qcinv, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qinv_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1247,13 +1247,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^2)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_square; auto. simpl Qcpower. replace (Q2Qc [x] * 1) with (Q2Qc [x]); try ring. simpl. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. Qed. @@ -1264,14 +1264,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold to_Qc. transitivity (Q2Qc ([x]^Zpos p)). unfold Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete; apply spec_power_pos; auto. induction p using Pos.peano_ind. simpl; ring. rewrite Pos2Nat.inj_succ; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. - apply Qc_decomp; intros _ _; unfold this. + apply Qc_decomp; unfold this. apply Qred_complete. setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. @@ -1281,4 +1281,3 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. Qed. End Make. - diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index a40d9405..8e20fd06 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -115,7 +115,10 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy. Local Obligation Tactic := solve_wd2 || solve_wd1. Instance : Measure to_Q. -Instance eq_equiv : Equivalence eq := {}. +Instance eq_equiv : Equivalence eq. +Proof. + change eq with (RelCompFun Qeq to_Q); apply _. +Defined. Program Instance lt_wd : Proper (eq==>eq==>iff) lt. Program Instance le_wd : Proper (eq==>eq==>iff) le. @@ -141,7 +144,10 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed. (** Let's implement [TotalOrder] *) Definition lt_compat := lt_wd. -Instance lt_strorder : StrictOrder lt := {}. +Instance lt_strorder : StrictOrder lt. +Proof. + change lt with (RelCompFun Qlt to_Q); apply _. +Qed. Lemma le_lteq : forall x y, x<=y <-> x p. Proof. revert q. @@ -508,7 +507,7 @@ Qed. Lemma mul_xO_discr p q : p~0 * q <> q. Proof. induction q; try discriminate. - rewrite mul_xO_r; injection; assumption. + rewrite mul_xO_r; injection; auto. Qed. (** ** Simplification properties of multiplication *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 27e1ca84..d6f9bb9d 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -8,7 +8,6 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Export ProofIrrelevance. Require Export JMeq. Require Import Coq.Program.Tactics. @@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p := | [ H : X = Y |- _ ] => match p with | H => fail 2 - | _ => rewrite (proof_irrelevance (X = Y) p H) + | _ => rewrite (UIP _ X Y p H) end | _ => fail " No hypothesis with same type " end @@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. apply proof_irrelevance. Qed. +Proof. apply UIP. Qed. Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. @@ -238,8 +237,8 @@ Ltac inject_left H := Ltac inject_right H := progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H. -Ltac autoinjections_left := repeat autoinjection ltac:inject_left. -Ltac autoinjections_right := repeat autoinjection ltac:inject_right. +Ltac autoinjections_left := repeat autoinjection ltac:(inject_left). +Ltac autoinjections_right := repeat autoinjection ltac:(inject_right). Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_existTs ; simplify_IH_hyps. @@ -333,7 +332,7 @@ Ltac simplify_one_dep_elim_term c := (let hyp := fresh in intros hyp ; move hyp before y ; revert_until hyp ; generalize dependent y ; refine (solution_right _ _ _ _)(* ; intros until 0 *)) - | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) + | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H) | ?t = ?u -> _ => let hyp := fresh in intros hyp ; exfalso ; discriminate | ?x = ?y -> _ => let hyp := fresh in diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c8f37318..2a3ec926 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,6 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. +Require Export ProofIrrelevance. Local Open Scope program_scope. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 66ca3e57..dfd6b0ea 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -252,7 +252,7 @@ Ltac autoinjection tac := Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H. -Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject). +Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)). (** Destruct an hypothesis by first copying it to avoid dependencies. *) @@ -264,7 +264,7 @@ Ltac bang := match goal with | |- ?x => match x with - | appcontext [False_rect _ ?p] => elim p + | context [False_rect _ ?p] => elim p end end. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 154200d7..c490ea51 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -89,7 +89,7 @@ Section Measure_well_founded. Lemma measure_wf: well_founded MR. Proof with auto. unfold well_founded. - cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a). + cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). intros. apply (H (m a))... apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). @@ -211,7 +211,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => + context C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v new file mode 100644 index 00000000..c0ababff --- /dev/null +++ b/theories/QArith/Qcabs.v @@ -0,0 +1,129 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Qred (Qabs x) = Qabs x. +Proof. intros H; now rewrite (Qred_abs x), H. Qed. + +Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}. +Notation "[ q ]" := (Qcabs q) (q at next level, format "[ q ]") : Qc_scope. + +Ltac Qc_unfolds := + unfold Qcabs, Qcminus, Qcopp, Qcplus, Qcmult, Qcle, Q2Qc, this. + +Lemma Qcabs_case (x:Qc) (P : Qc -> Type) : + (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x]. +Proof. + intros A B. + apply (Qabs_case x (fun x => forall Hx, P {|this:=x;canon:=Hx|})). + intros; case (Qc_decomp x {|canon:=Hx|}); auto. + intros; case (Qc_decomp (-x) {|canon:=Hx|}); auto. +Qed. + +Lemma Qcabs_pos x : 0 <= x -> [x] = x. +Proof. + intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + set (a := x) at 1; case (canon x); subst a; apply Qred_complete. + now apply Qabs_pos. +Qed. + +Lemma Qcabs_neg x : x <= 0 -> [x] = - x. +Proof. + intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + now apply Qred_complete; apply Qabs_neg. +Qed. + +Lemma Qcabs_nonneg x : 0 <= [x]. +Proof. intros; apply Qabs_nonneg. Qed. + +Lemma Qcabs_opp x : [(-x)] = [x]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x). + set (K := canon [x]); simpl in K; case K; clear K. + case Qred_abs; apply Qred_complete; apply Qabs_opp. +Qed. + +Lemma Qcabs_triangle x y : [x+y] <= [x] + [y]. +Proof. + Qc_unfolds; case Qred_abs; rewrite !Qred_le; apply Qabs_triangle. +Qed. + +Lemma Qcabs_Qcmult x y : [x*y] = [x]*[y]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x) (this y); case Qred_abs. + apply Qred_complete; apply Qabs_Qmult. +Qed. + +Lemma Qcabs_Qcminus x y: [x-y] = [y-x]. +Proof. + apply Qc_decomp; Qc_unfolds; fold (this x) (this y) (this (-x)) (this (-y)). + set (a := x) at 2; case (canon x); subst a. + set (a := y) at 1; case (canon y); subst a. + rewrite !Qred_opp; fold (Qred x - Qred y)%Q (Qred y - Qred x)%Q. + repeat case Qred_abs; f_equal; apply Qabs_Qminus. +Qed. + +Lemma Qcle_Qcabs x : x <= [x]. +Proof. apply Qle_Qabs. Qed. + +Lemma Qcabs_triangle_reverse x y : [x] - [y] <= [x - y]. +Proof. + unfold Qcle, Qcabs, Qcminus, Qcplus, Qcopp, Q2Qc, this; + fold (this x) (this y) (this (-x)) (this (-y)). + case Qred_abs; rewrite !Qred_le, !Qred_opp, Qred_abs. + apply Qabs_triangle_reverse. +Qed. + +Lemma Qcabs_Qcle_condition x y : [x] <= y <-> -y <= x <= y. +Proof. + Qc_unfolds; fold (this x) (this y). + destruct (Qabs_Qle_condition x y) as [A B]. + split; intros H. + + destruct (A H) as [X Y]; split; auto. + now case (canon x); apply Qred_le. + + destruct H as [X Y]; apply B; split; auto. + now case (canon y); case Qred_opp. +Qed. + +Lemma Qcabs_diff_Qcle_condition x y r : [x-y] <= r <-> x - r <= y <= x + r. +Proof. + Qc_unfolds; fold (this x) (this y) (this r). + case Qred_abs; repeat rewrite Qred_opp. + set (a := y) at 1; case (canon y); subst a. + set (a := r) at 2; case (canon r); subst a. + set (a := Qred r) at 2 3; + assert (K := canon (Q2Qc r)); simpl in K; case K; clear K; subst a. + set (a := Qred y) at 1; + assert (K := canon (Q2Qc y)); simpl in K; case K; clear K; subst a. + fold (x - Qred y)%Q (x - Qred r)%Q. + destruct (Qabs_diff_Qle_condition x (Qred y) (Qred r)) as [A B]. + split. + + clear B; rewrite !Qred_le. auto. + + clear A; rewrite !Qred_le. auto. +Qed. + +Lemma Qcabs_null x : [x] = 0 -> x = 0. +Proof. + intros H. + destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B]. + + rewrite H; apply Qcle_refl. + + apply Qcle_antisym; auto. +Qed. \ No newline at end of file diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index d966b050..9f9651d8 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -21,37 +21,30 @@ Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. Open Scope Qc_scope. +(** An alternative statement of [Qred q = q] via [Z.gcd] *) + Lemma Qred_identity : forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q. Proof. - unfold Qred; intros (a,b); simpl. - generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)). - intros. - rewrite H1 in H; clear H1. - destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. - destruct H0. - rewrite Z.mul_1_l in H, H0. - subst; simpl; auto. + intros (a,b) H; simpl in *. + rewrite <- Z.ggcd_gcd in H. + generalize (Z.ggcd_correct_divisors a ('b)). + destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst. + rewrite !Z.mul_1_l. now intros (<-,<-). Qed. Lemma Qred_identity2 : forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z. Proof. - unfold Qred; intros (a,b); simpl. - generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)). - intros. - rewrite <- H; rewrite <- H in H1; clear H. - destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst. - injection H2; intros; clear H2. - destruct H0. - clear H0 H3. - destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate. - f_equal. - apply Pos.mul_reg_r with bb. - injection H2; intros. - rewrite <- H0. - rewrite H; simpl; auto. - elim H1; auto. + intros (a,b) H; simpl in *. + generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)). + rewrite <- Z.ggcd_gcd. + destruct Z.ggcd as (g,(aa,bb)); simpl in *. + injection H as <- <-. intros H (_,H'). + destruct g as [|g|g]; [ discriminate | | now elim H ]. + destruct bb as [|b|b]; simpl in *; try discriminate. + injection H' as H'. f_equal. + apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed. Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z. @@ -61,6 +54,23 @@ Proof. apply Qred_identity; auto. Qed. +(** Coercion from [Qc] to [Q] and equality *) + +Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. +Proof. + intros (q,hq) (q',hq') H. simpl in *. + assert (H' := Qred_complete _ _ H). + rewrite hq, hq' in H'. subst q'. f_equal. + apply eq_proofs_unicity. intros. repeat decide equality. +Qed. +Hint Resolve Qc_is_canon. + +Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'. +Proof. + intros. apply Qc_is_canon. now rewrite H. +Qed. + +(** [Q2Qc] : a conversion from [Q] to [Qc]. *) Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q. Proof. @@ -71,20 +81,12 @@ Qed. Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q). Arguments Q2Qc q%Q. -Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'. +Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. - intros (q,proof_q) (q',proof_q'). - simpl. - intros H. - assert (H0:=Qred_complete _ _ H). - assert (q = q') by congruence. - subst q'. - assert (proof_q = proof_q'). - apply eq_proofs_unicity; auto; intros. - repeat decide equality. - congruence. + split; intro H. + - now injection H as H%Qred_eq_iff. + - apply Qc_is_canon. simpl. now rewrite H. Qed. -Hint Resolve Qc_is_canon. Notation " 0 " := (Q2Qc 0) : Qc_scope. Notation " 1 " := (Q2Qc 1) : Qc_scope. @@ -107,8 +109,7 @@ Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq. Proof. unfold Qccompare. intros; rewrite <- Qeq_alt. - split; auto. - intro H; rewrite H; auto with qarith. + split; auto. now intros <-. Qed. Lemma Qclt_alt : forall p q, (p (p?=q = Lt). @@ -121,12 +122,12 @@ Proof. intros; exact (Qgt_alt p q). Qed. -Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). +Lemma Qcle_alt : forall p q, (p<=q) <-> (p?=q <> Gt). Proof. intros; exact (Qle_alt p q). Qed. -Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). +Lemma Qcge_alt : forall p q, (p>=q) <-> (p?=q <> Lt). Proof. intros; exact (Qge_alt p q). Qed. @@ -166,7 +167,7 @@ Qed. Ltac qc := match goal with | q:Qc |- _ => destruct q; qc - | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct + | _ => apply Qc_is_canon; simpl; rewrite !Qred_correct end. Opaque Qred. @@ -216,6 +217,18 @@ Proof. intros; qc; apply Qmult_assoc. Qed. +(** [0] is absorbing for multiplication: *) + +Lemma Qcmult_0_l : forall n, 0*n = 0. +Proof. + intros; qc; split. +Qed. + +Theorem Qcmult_0_r : forall n, n*0=0. +Proof. + intros; qc; rewrite Qmult_comm; split. +Qed. + (** [1] is a neutral element for multiplication: *) Lemma Qcmult_1_l : forall n, 1*n = n. @@ -253,7 +266,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H; clear H; intros. + injection H as H. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. @@ -303,7 +316,7 @@ Proof. apply Qcmult_1_l. Qed. -(** Properties of order upon Q. *) +(** Properties of order upon Qc. *) Lemma Qcle_refl : forall x, x<=x. Proof. @@ -372,9 +385,11 @@ Proof. unfold Qcle, Qclt; intros; apply Qle_not_lt; auto. Qed. -Lemma Qcle_lt_or_eq : forall x y, x<=y -> x xO -> 0^n = 0. Proof. destruct n; simpl. destruct 1; auto. intros. - now apply Qc_is_canon. + now apply Qc_is_canon. Qed. Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n. @@ -525,16 +540,3 @@ intros. field. auto. Qed. - - -Theorem Qc_decomp: forall x y: Qc, - (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y. -Proof. - intros (q, Hq) (q', Hq'); simpl; intros H. - assert (H1 := H Hq Hq'). - subst q'. - assert (Hq = Hq'). - apply Eqdep_dec.eq_proofs_unicity; auto; intros. - repeat decide equality. - congruence. -Qed. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index c50c38b2..131214f5 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -93,11 +93,17 @@ Proof. Close Scope Z_scope. Qed. +Lemma Qred_eq_iff q q' : Qred q = Qred q' <-> q == q'. +Proof. + split. + - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q'). + now rewrite E. + - apply Qred_complete. +Qed. + Add Morphism Qred : Qred_comp. Proof. - intros q q' H. - rewrite (Qred_correct q); auto. - rewrite (Qred_correct q'); auto. + intros. now rewrite !Qred_correct. Qed. Definition Qplus' (p q : Q) := Qred (Qplus p q). @@ -149,3 +155,13 @@ Theorem Qred_compare: forall x y, Proof. intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct. Qed. + +Lemma Qred_le q q' : Qred q <= Qred q' <-> q <= q'. +Proof. + now rewrite !Qle_alt, <- Qred_compare. +Qed. + +Lemma Qred_lt q q' : Qred q < Qred q' <-> q < q'. +Proof. + now rewrite !Qlt_alt, <- Qred_compare. +Qed. diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget index b3faef88..b550b471 100644 --- a/theories/QArith/vo.itarget +++ b/theories/QArith/vo.itarget @@ -2,6 +2,7 @@ Qabs.vo QArith_base.vo QArith.vo Qcanon.vo +Qcabs.vo Qfield.vo Qpower.vo Qreals.vo diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index f26bac2b..379fee6f 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -389,7 +389,7 @@ Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. Proof. split; ring. Qed. -Hint Resolve Rplus_ne: real v62. +Hint Resolve Rplus_ne: real. (**********) @@ -425,7 +425,6 @@ Proof. apply (f_equal (fun v => v + r)). Qed. -(*i Old i*)Hint Resolve Rplus_eq_compat_l: v62. (**********) Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 = r + r2 -> r1 = r2. @@ -501,21 +500,21 @@ Lemma Rmult_0_r : forall r, r * 0 = 0. Proof. intro; ring. Qed. -Hint Resolve Rmult_0_r: real v62. +Hint Resolve Rmult_0_r: real. (**********) Lemma Rmult_0_l : forall r, 0 * r = 0. Proof. intro; ring. Qed. -Hint Resolve Rmult_0_l: real v62. +Hint Resolve Rmult_0_l: real. (**********) Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r. Proof. intro; split; ring. Qed. -Hint Resolve Rmult_ne: real v62. +Hint Resolve Rmult_ne: real. (**********) Lemma Rmult_1_r : forall r, r * 1 = r. @@ -530,7 +529,6 @@ Proof. auto with real. Qed. -(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62. Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r. Proof. @@ -646,7 +644,7 @@ Lemma Ropp_0 : -0 = 0. Proof. ring. Qed. -Hint Resolve Ropp_0: real v62. +Hint Resolve Ropp_0: real. (**********) Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0. diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v index 2465f039..0c27d407 100644 --- a/theories/Reals/Ranalysis_reg.v +++ b/theories/Reals/Ranalysis_reg.v @@ -35,7 +35,7 @@ Qed. (**********) Ltac intro_hyp_glob trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -55,7 +55,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 @@ -82,7 +82,7 @@ Ltac intro_hyp_glob trm := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(forall x0:R, aux x0 <> 0) |- (derivable _) => intro_hyp_glob X1 @@ -108,7 +108,8 @@ Ltac intro_hyp_glob trm := | (pow_fct _) => idtac | Rabs => idtac | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in + let HYPPD := fresh "HYPPD" in match goal with | _:(derivable p) |- _ => idtac | |- (derivable p) => idtac @@ -130,7 +131,7 @@ Ltac intro_hyp_glob trm := (**********) Ltac intro_hyp_pt trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => match goal with | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -156,7 +157,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (?X1 / ?X2)%F => - let aux := constr:X2 in + let aux := constr:(X2) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt @@ -202,7 +203,7 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | (/ ?X1)%F => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | _:(aux pt <> 0) |- (derivable_pt _ _) => intro_hyp_pt X1 pt @@ -249,7 +250,8 @@ Ltac intro_hyp_pt trm pt := | _ => idtac end | ?X1 => - let p := constr:X1 in + let p := constr:(X1) in + let HYPPD := fresh "HYPPD" in match goal with | _:(derivable_pt p pt) |- _ => idtac | |- (derivable_pt p pt) => idtac @@ -341,8 +343,10 @@ Ltac is_diff_pt := | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) => assumption | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ] | |- (True -> derivable_pt _ _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_diff_pt | _ => try @@ -411,6 +415,7 @@ Ltac is_diff_glob := apply (derivable_comp X2 X1); is_diff_glob | _:(derivable ?X1) |- (derivable ?X1) => assumption | |- (True -> derivable _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_diff_glob | _ => try @@ -490,14 +495,17 @@ Ltac is_cont_pt := | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => assumption | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ] | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => apply derivable_continuous_pt; assumption | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) => + let HypDDPT := fresh "HypDDPT" in cut (continuity X1); [ intro HypDDPT; apply HypDDPT | apply derivable_continuous; assumption ] | |- (True -> continuity_pt _ _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_cont_pt | _ => try @@ -567,6 +575,7 @@ Ltac is_cont_glob := apply (continuity_comp X2 X1); try is_cont_glob || assumption | _:(continuity ?X1) |- (continuity ?X1) => assumption | |- (True -> continuity _) => + let HypTruE := fresh "HypTruE" in intro HypTruE; clear HypTruE; is_cont_glob | _:(derivable ?X1) |- (continuity ?X1) => apply derivable_continuous; assumption @@ -578,89 +587,89 @@ Ltac is_cont_glob := (**********) Ltac rew_term trm := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 + X4)) - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end - | _ => constr:(p1 + p2)%F + | _ => constr:((p1 + p2)%F) end | (?X1 - ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 - X4)) - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end - | _ => constr:(p1 - p2)%F + | _ => constr:((p1 - p2)%F) end | (?X1 / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * / ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 / X4)) - | _ => constr:(p1 / p2)%F + | _ => constr:((p1 / p2)%F) end | _ => - match constr:p2 with - | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F - | _ => constr:(p1 / p2)%F + match constr:(p2) with + | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F) + | _ => constr:((p1 / p2)%F) end end | (?X1 * ?X2) => let p1 := rew_term X1 with p2 := rew_term X2 in - match constr:p1 with + match constr:(p1) with | (fct_cte ?X3) => - match constr:p2 with + match constr:(p2) with | (fct_cte ?X4) => constr:(fct_cte (X3 * X4)) - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end - | _ => constr:(p1 * p2)%F + | _ => constr:((p1 * p2)%F) end | (- ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (- X2)) - | _ => constr:(- p)%F + | _ => constr:((- p)%F) end | (/ ?X1) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X2) => constr:(fct_cte (/ X2)) - | _ => constr:(/ p)%F + | _ => constr:((/ p)%F) end - | (?X1 AppVar) => constr:X1 + | (?X1 AppVar) => constr:(X1) | (?X1 ?X2) => let p := rew_term X2 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (X1 X3)) | _ => constr:(comp X1 p) end - | AppVar => constr:id + | AppVar => constr:(id) | (AppVar ^ ?X1) => constr:(pow_fct X1) | (?X1 ^ ?X2) => let p := rew_term X1 in - match constr:p with + match constr:(p) with | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3)) | _ => constr:(comp (pow_fct X2) p) end @@ -669,7 +678,7 @@ Ltac rew_term trm := (**********) Ltac deriv_proof trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_plus X1 X2 pt p1 p2) @@ -684,14 +693,14 @@ Ltac deriv_proof trm pt := | id:(?X2 pt <> 0) |- _ => let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in constr:(derivable_pt_div X1 X2 pt p1 p2 id) - | _ => constr:False + | _ => constr:(False) end | (/ ?X1)%F => match goal with | id:(?X1 pt <> 0) |- _ => let p1 := deriv_proof X1 pt in constr:(derivable_pt_inv X1 pt p1 id) - | _ => constr:False + | _ => constr:(False) end | (comp ?X1 ?X2) => let pt_f1 := eval cbv beta in (X2 pt) in @@ -710,21 +719,21 @@ Ltac deriv_proof trm pt := | sqrt => match goal with | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id) - | _ => constr:False + | _ => constr:(False) end | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt) | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with - | id:(derivable_pt aux pt) |- _ => constr:id + | id:(derivable_pt aux pt) |- _ => constr:(id) | id:(derivable aux) |- _ => constr:(id pt) - | _ => constr:False + | _ => constr:(False) end end. (**********) Ltac simplify_derive trm pt := - match constr:trm with + match constr:(trm) with | (?X1 + ?X2)%F => try rewrite derive_pt_plus; simplify_derive X1 pt; simplify_derive X2 pt @@ -753,7 +762,7 @@ Ltac simplify_derive trm pt := | Rsqr => try rewrite derive_pt_Rsqr | sqrt => try rewrite derive_pt_sqrt | ?X1 => - let aux := constr:X1 in + let aux := constr:(X1) in match goal with | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ => try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2); diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 9d55e4e6..9fbda92a 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -32,7 +32,7 @@ Hint Resolve Rplus_assoc: real. (**********) Axiom Rplus_opp_r : forall r:R, r + - r = 0. -Hint Resolve Rplus_opp_r: real v62. +Hint Resolve Rplus_opp_r: real. (**********) Axiom Rplus_0_l : forall r:R, 0 + r = r. @@ -44,11 +44,11 @@ Hint Resolve Rplus_0_l: real. (**********) Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1. -Hint Resolve Rmult_comm: real v62. +Hint Resolve Rmult_comm: real. (**********) Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3). -Hint Resolve Rmult_assoc: real v62. +Hint Resolve Rmult_assoc: real. (**********) Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1. @@ -69,7 +69,7 @@ Hint Resolve R1_neq_R0: real. (**********) Axiom Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3. -Hint Resolve Rmult_plus_distr_l: real v62. +Hint Resolve Rmult_plus_distr_l: real. (*********************************************************) (** * Order axioms *) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442..d43baee8 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 220cebea..fe8a96ac 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -36,7 +36,7 @@ Section Properties. Section Clos_Refl_Trans. Local Notation "R *" := (clos_refl_trans R) - (at level 8, left associativity, format "R *"). + (at level 8, no associativity, format "R *"). (** Correctness of the reflexive-transitive closure operator *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index b6005b9d..9c98879c 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -66,10 +66,10 @@ Section Relation_Definition. End Relation_Definition. -Hint Unfold reflexive transitive antisymmetric symmetric: sets v62. +Hint Unfold reflexive transitive antisymmetric symmetric: sets. Hint Resolve Build_preorder Build_order Build_equivalence Build_PER preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl - equiv_trans equiv_sym per_sym per_trans: sets v62. + equiv_trans equiv_sym per_sym per_trans: sets. -Hint Unfold inclusion same_relation commut: sets v62. +Hint Unfold inclusion same_relation commut: sets. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index ffd682d6..88239475 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -226,9 +226,9 @@ Section Lexicographic_Exponentiation. End Lexicographic_Exponentiation. -Hint Unfold transp union: sets v62. -Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62. -Hint Immediate rst_sym: sets v62. +Hint Unfold transp union: sets. +Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets. +Hint Immediate rst_sym: sets. (* begin hide *) (* Compatibility *) diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 8a4bb9f4..837437a2 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -122,4 +122,4 @@ Section Ensembles_classical. End Ensembles_classical. Hint Resolve Strict_super_set_contains_new_element Subtract_intro - not_SIncl_empty: sets v62. + not_SIncl_empty: sets. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 8d2344f9..6291248e 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -141,4 +141,4 @@ End Ensembles_facts. Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 Intersection_inv Couple_inv Setminus_intro Strict_Included_intro Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty - not_Empty_Add Inhabited_add Included_Empty: sets v62. + not_Empty_Add Inhabited_add Included_Empty: sets. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index 8f579214..0fefb354 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -90,9 +90,8 @@ Section Ensembles. End Ensembles. -Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets - v62. +Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets. Hint Resolve Union_introl Union_intror Intersection_intro In_singleton Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro - Extensionality_Ensembles: sets v62. + Extensionality_Ensembles: sets. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index f38dd6fd..edbc1efe 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -43,8 +43,8 @@ Section Ensembles_finis. End Ensembles_finis. -Hint Resolve Empty_is_finite Union_is_finite: sets v62. -Hint Resolve card_empty card_add: sets v62. +Hint Resolve Empty_is_finite Union_is_finite: sets. +Hint Resolve card_empty card_add: sets. Require Import Constructive_sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 34ea857d..e74ef41e 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -200,4 +200,4 @@ Section Image. End Image. -Hint Resolve Im_def image_empty finite_image: sets v62. +Hint Resolve Im_def image_empty finite_image: sets. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index ec38b892..42d0c76d 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -187,7 +187,7 @@ End multiset_defs. Unset Implicit Arguments. -Hint Unfold meq multiplicity: v62 datatypes. +Hint Unfold meq multiplicity: datatypes. Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right - munion_empty_left: v62 datatypes. -Hint Immediate meq_sym: v62 datatypes. + munion_empty_left: datatypes. +Hint Immediate meq_sym: datatypes. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 3610ebce..335fec5b 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -51,8 +51,8 @@ Section Partial_orders. End Partial_orders. -Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62. -Hint Resolve Definition_of_covers: sets v62. +Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets. +Hint Resolve Definition_of_covers: sets. Section Partial_order_facts. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index d636e046..7c2435da 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -175,14 +175,14 @@ Qed. End The_power_set_partial_order. -Hint Resolve Empty_set_minimal: sets v62. -Hint Resolve Power_set_Inhabited: sets v62. -Hint Resolve Inclusion_is_an_order: sets v62. -Hint Resolve Inclusion_is_transitive: sets v62. -Hint Resolve Union_minimal: sets v62. -Hint Resolve Union_increases_l: sets v62. -Hint Resolve Union_increases_r: sets v62. -Hint Resolve Intersection_decreases_l: sets v62. -Hint Resolve Intersection_decreases_r: sets v62. -Hint Resolve Empty_set_is_Bottom: sets v62. -Hint Resolve Strict_inclusion_is_transitive: sets v62. +Hint Resolve Empty_set_minimal: sets. +Hint Resolve Power_set_Inhabited: sets. +Hint Resolve Inclusion_is_an_order: sets. +Hint Resolve Inclusion_is_transitive: sets. +Hint Resolve Union_minimal: sets. +Hint Resolve Union_increases_l: sets. +Hint Resolve Union_increases_r: sets. +Hint Resolve Intersection_decreases_l: sets. +Hint Resolve Intersection_decreases_r: sets. +Hint Resolve Empty_set_is_Bottom: sets. +Hint Resolve Strict_inclusion_is_transitive: sets. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 09c90506..e802beac 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -90,7 +90,7 @@ Section Sets_as_an_algebra. apply Subtract_intro; auto with sets. red; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. - Hint Resolve incl_soustr_add_r: sets v62. + Hint Resolve incl_soustr_add_r: sets. Lemma add_soustr_2 : forall (X:Ensemble U) (x:U), @@ -328,9 +328,9 @@ Section Sets_as_an_algebra. End Sets_as_an_algebra. -Hint Resolve incl_soustr_in: sets v62. -Hint Resolve incl_soustr: sets v62. -Hint Resolve incl_soustr_add_l: sets v62. -Hint Resolve incl_soustr_add_r: sets v62. -Hint Resolve add_soustr_1 add_soustr_2: sets v62. -Hint Resolve add_soustr_xy: sets v62. +Hint Resolve incl_soustr_in: sets. +Hint Resolve incl_soustr: sets. +Hint Resolve incl_soustr_add_l: sets. +Hint Resolve incl_soustr_add_r: sets. +Hint Resolve add_soustr_1 add_soustr_2: sets. +Hint Resolve add_soustr_xy: sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 63e84199..e9696a1c 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -254,5 +254,5 @@ Section Sets_as_an_algebra. End Sets_as_an_algebra. Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add - singlx incl_add: sets v62. + singlx incl_add: sets. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index de96fa56..45fb8134 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -60,6 +60,6 @@ Section Relations_1. End Relations_1. Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains - same_relation: sets v62. + same_relation: sets. Hint Resolve Definition_of_preorder Definition_of_order - Definition_of_equivalence Definition_of_PER: sets v62. + Definition_of_equivalence Definition_of_PER: sets. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index f1026e31..1e0b83fe 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -48,7 +48,7 @@ Definition Strongly_confluent : Prop := End Relations_2. -Hint Resolve Rstar_0: sets v62. -Hint Resolve Rstar1_0: sets v62. -Hint Resolve Rstar1_1: sets v62. -Hint Resolve Rplus_0: sets v62. +Hint Resolve Rstar_0: sets. +Hint Resolve Rstar1_0: sets. +Hint Resolve Rstar1_1: sets. +Hint Resolve Rplus_0: sets. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 92b29988..c05b5ee7 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -51,10 +51,10 @@ Section Relations_3. Definition Noetherian : Prop := forall x:U, noetherian x. End Relations_3. -Hint Unfold coherent: sets v62. -Hint Unfold locally_confluent: sets v62. -Hint Unfold confluent: sets v62. -Hint Unfold Confluent: sets v62. -Hint Resolve definition_of_noetherian: sets v62. -Hint Unfold Noetherian: sets v62. +Hint Unfold coherent: sets. +Hint Unfold locally_confluent: sets. +Hint Unfold confluent: sets. +Hint Unfold Confluent: sets. +Hint Resolve definition_of_noetherian: sets. +Hint Unfold Noetherian: sets. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index e159efa8..44f8ff6a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -318,10 +318,10 @@ Lemma Permutation_length_2_inv : Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. - induction H; intros; try (injection Heqm; intros; subst; clear Heqm); + induction H; intros; try (injection Heqm as ? ?; subst); discriminate || (try tauto). apply Permutation_length_1_inv in H as ->; left; auto. - apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as (); + apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; auto. Qed. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 97cb746f..55a533c5 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -40,7 +40,7 @@ Defined. (** * Conversion between natural numbers modulo 256 and ascii characters *) -(** Auxillary function that turns a positive into an ascii by +(** Auxiliary function that turns a positive into an ascii by looking at the last 8 bits, ie z mod 2^8 *) Definition ascii_of_pos : positive -> ascii := diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 943bb48e..451b65cb 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -83,7 +83,7 @@ intros H; generalize (H 0); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). -intros H; injection H; intros H1 H2 n; case n; auto. +intros H; injection H as H1 H2. rewrite H2; trivial. rewrite H1; auto. Qed. @@ -238,14 +238,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H; intros H1; rewrite <- H1; auto. +intros H; injection H as <-; auto. intros; discriminate. intros; discriminate. intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H; intros H1; rewrite <- H1; auto. +intros H0 H; injection H as <-; auto. case H0; simpl; auto. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. @@ -271,7 +271,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H; intros H1; rewrite <- H1. +intros H; injection H as <-. intros p H0 H2; inversion H2. intros; discriminate. intros; discriminate. @@ -279,7 +279,7 @@ intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H; intros H1; rewrite <- H1; auto. +intros H0 H; injection H as <-; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 954d3df2..0115d8a5 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -434,21 +434,21 @@ Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma ltb_compare x y : (x true | _ => false end. Proof. apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma leb_compare x y : (x <=? y) = match compare x y with Gt => false | _ => true end. Proof. apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. -destruct compare; split; try easy. now destruct 1. +now destruct compare. Qed. End BoolOrderFacts. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 45c13e5c..1f8b76cb 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -30,7 +30,7 @@ Inductive t A : nat -> Type := |nil : t A 0 |cons : forall (h:A) (n:nat), t A n -> t A (S n). -Local Notation "[]" := (nil _). +Local Notation "[ ]" := (nil _) (format "[ ]"). Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity). Section SCHEMES. @@ -102,7 +102,7 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x). Computational behavior of this function should be the same as ocaml function. *) -Definition nth {A} := +Definition nth {A} := fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A := match p in Fin.t m' return t A m' -> A with |Fin.F1 => caseS (fun n v' => A) (fun h n t => h) @@ -293,12 +293,14 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni End VECTORLIST. Module VectorNotations. -Notation "[]" := [] : vector_scope. +Delimit Scope vector_scope with vector. +Notation "[ ]" := [] (format "[ ]") : vector_scope. +Notation "[]" := [] (compat "8.5") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) : vector_scope. -Notation " [ x ] " := (x :: []) : vector_scope. -Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _)) ..) : vector_scope -. +Notation "[ x ]" := (x :: []) : vector_scope. +Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. +Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. Open Scope vector_scope. End VectorNotations. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 992263cb..d90f9956 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -75,7 +75,7 @@ Section Wf_Lexicographic_Exponentiation. Proof. intros. inversion H. - - apply app_cons_not_nil in H1 as (). + - apply app_cons_not_nil in H1 as []. - assert (x ++ [a] = [x0]) by auto with sets. apply app_eq_unit in H0 as [(->, _)| (_, [=])]. auto using d_nil. @@ -98,7 +98,7 @@ Section Wf_Lexicographic_Exponentiation. destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-). inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ]. - inversion H0. - + apply app_cons_not_nil in H3 as (). + + apply app_cons_not_nil in H3 as []. + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0. pose proof (H x0 b H0). apply rt_trans with (y := x0); auto with sets. @@ -145,7 +145,7 @@ Section Wf_Lexicographic_Exponentiation. pose proof H0 as H0'. apply app_inj_tail in H0' as (_, ->). rewrite app_assoc_reverse in H0. - apply Hind in H0 as (). + apply Hind in H0 as []. split. assumption. apply d_conc; auto with sets. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 4b8447f4..b2ada2f9 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -44,14 +44,11 @@ Section WfLexicographic_Product. apply H2. auto with sets. - injection H1. - destruct 2. - injection H3. - destruct 2; auto with sets. + injection H1 as <- _. + injection H3 as <- _; auto with sets. rewrite <- H1. - injection H3; intros _ Hx1. - subst x1. + injection H3 as -> H3. apply IHAcc0. elim inj_pair2 with A B x y' x0; assumption. Defined. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index d210792f..72021f2e 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -225,11 +225,11 @@ Module MoreInt (Import I:Int). (** [int] to [ExprI] *) Ltac i2ei trm := - match constr:trm with - | 0 => constr:EI0 - | 1 => constr:EI1 - | 2 => constr:EI2 - | 3 => constr:EI3 + match constr:(trm) with + | 0 => constr:(EI0) + | 1 => constr:(EI1) + | 2 => constr:(EI2) + | 3 => constr:(EI3) | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey) | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey) | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey) @@ -241,7 +241,7 @@ Module MoreInt (Import I:Int). (** [Z] to [ExprZ] *) with z2ez trm := - match constr:trm with + match constr:(trm) with | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey) | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey) | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey) @@ -254,7 +254,7 @@ Module MoreInt (Import I:Int). (** [Prop] to [ExprP] *) Ltac p2ep trm := - match constr:trm with + match constr:(trm) with | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey) | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey) | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey) @@ -451,4 +451,8 @@ Module Z_as_Int <: Int. Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p). Proof. reflexivity. Qed. + (** Compatibility notations for Coq v8.4 *) + Notation plus := add (compat "8.4"). + Notation minus := sub (compat "8.4"). + Notation mult := mul (compat "8.4"). End Z_as_Int. diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index b80eb445..f4baba19 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -30,12 +30,12 @@ Local Open Scope Z_scope. Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xI X1) end | |- context [(Zpos (xO ?X1))] => - match constr:X1 with + match constr:(X1) with | context [1%positive] => fail 1 | _ => rewrite (Pos2Z.inj_xO X1) end diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 1ac00bdd..90754af3 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -56,7 +56,7 @@ Section wf_proof. End wf_proof. -Hint Resolve Zwf_well_founded: datatypes v62. +Hint Resolve Zwf_well_founded: datatypes. (** We also define the other family of relations: @@ -88,4 +88,4 @@ Section wf_proof_up. End wf_proof_up. -Hint Resolve Zwf_up_well_founded: datatypes v62. +Hint Resolve Zwf_up_well_founded: datatypes. diff --git a/theories/theories.itarget b/theories/theories.itarget deleted file mode 100644 index aacab2d9..00000000 --- a/theories/theories.itarget +++ /dev/null @@ -1,25 +0,0 @@ -Arith/vo.otarget -Bool/vo.otarget -Classes/vo.otarget -Compat/vo.otarget -FSets/vo.otarget -MSets/vo.otarget -Structures/vo.otarget -Init/vo.otarget -Lists/vo.otarget -Vectors/vo.otarget -Logic/vo.otarget -PArith/vo.otarget -NArith/vo.otarget -Numbers/vo.otarget -Program/vo.otarget -QArith/vo.otarget -Reals/vo.otarget -Relations/vo.otarget -Setoids/vo.otarget -Sets/vo.otarget -Sorting/vo.otarget -Strings/vo.otarget -Unicode/vo.otarget -Wellfounded/vo.otarget -ZArith/vo.otarget -- cgit v1.2.3