summaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 18:33:25 +0100
commit1b92c226e563643da187b8614d5888dc4855eb43 (patch)
treec4c3d204b36468b58cb71050ba95f06b8dd7bc2e /theories
parent7c9b0a702976078b813e6493c1284af62a3f093c (diff)
Imported Upstream version 8.6
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Between.v24
-rw-r--r--theories/Arith/EqNat.v4
-rw-r--r--theories/Arith/Gt.v16
-rw-r--r--theories/Arith/Le.v12
-rw-r--r--theories/Arith/Lt.v26
-rw-r--r--theories/Arith/Max.v4
-rw-r--r--theories/Arith/Minus.v20
-rw-r--r--theories/Arith/Mult.v16
-rw-r--r--theories/Arith/Peano_dec.v5
-rw-r--r--theories/Arith/Plus.v12
-rw-r--r--theories/Bool/Bool.v30
-rw-r--r--theories/Bool/IfProp.v2
-rw-r--r--theories/Classes/CMorphisms.v4
-rw-r--r--theories/Classes/Equivalence.v8
-rw-r--r--theories/Classes/Morphisms.v6
-rw-r--r--theories/Classes/RelationPairs.v5
-rw-r--r--theories/Classes/SetoidTactics.v16
-rw-r--r--theories/Compat/Coq84.v54
-rw-r--r--theories/Compat/Coq85.v27
-rw-r--r--theories/Compat/Coq86.v9
-rw-r--r--theories/Compat/vo.itarget1
-rw-r--r--theories/FSets/FMapFacts.v10
-rw-r--r--theories/FSets/FMapList.v2
-rw-r--r--theories/FSets/FMapPositive.v10
-rw-r--r--theories/FSets/FMapWeakList.v2
-rw-r--r--theories/FSets/FSetDecide.v19
-rw-r--r--theories/FSets/FSetList.v2
-rw-r--r--theories/FSets/FSetPositive.v28
-rw-r--r--theories/FSets/FSetWeakList.v2
-rw-r--r--theories/Init/Datatypes.v2
-rw-r--r--theories/Init/Logic_Type.v2
-rw-r--r--theories/Init/Notations.v8
-rw-r--r--theories/Init/Peano.v3
-rw-r--r--theories/Init/Prelude.v1
-rw-r--r--theories/Init/Specif.v3
-rw-r--r--theories/Init/Tactics.v8
-rw-r--r--theories/Init/Tauto.v101
-rw-r--r--theories/Init/Wf.v2
-rw-r--r--theories/Init/vo.itarget3
-rw-r--r--theories/Lists/List.v117
-rw-r--r--theories/Lists/ListSet.v109
-rw-r--r--theories/Lists/Streams.v2
-rw-r--r--theories/Logic/ClassicalFacts.v78
-rw-r--r--theories/Logic/Decidable.v2
-rw-r--r--theories/Logic/Eqdep.v2
-rw-r--r--theories/Logic/EqdepFacts.v2
-rw-r--r--theories/Logic/Hurkens.v3
-rw-r--r--theories/Logic/PropFacts.v50
-rw-r--r--theories/MSets/MSetAVL.v1
-rw-r--r--theories/MSets/MSetDecide.v19
-rw-r--r--theories/MSets/MSetInterface.v3
-rw-r--r--theories/MSets/MSetList.v2
-rw-r--r--theories/MSets/MSetPositive.v28
-rw-r--r--theories/MSets/MSetRBT.v4
-rw-r--r--theories/MSets/MSetWeakList.v2
-rw-r--r--theories/Numbers/BigNumPrelude.v4
-rw-r--r--theories/Numbers/Cyclic/Int31/Ring31.v20
-rw-r--r--theories/Numbers/Cyclic/ZModulo/ZModulo.v6
-rw-r--r--theories/Numbers/Integer/Abstract/ZDivEucl.v14
-rw-r--r--theories/Numbers/Integer/BigZ/BigZ.v24
-rw-r--r--theories/Numbers/Integer/BigZ/ZMake.v12
-rw-r--r--theories/Numbers/NatInt/NZGcd.v2
-rw-r--r--theories/Numbers/Natural/BigN/BigN.v26
-rw-r--r--theories/Numbers/Natural/BigN/NMake.v2
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml2
-rw-r--r--theories/Numbers/Natural/Peano/NPeano.v84
-rw-r--r--theories/Numbers/Rational/BigQ/BigQ.v14
-rw-r--r--theories/Numbers/Rational/BigQ/QMake.v37
-rw-r--r--theories/Numbers/Rational/SpecViaQ/QSig.v10
-rw-r--r--theories/PArith/BinPos.v3
-rw-r--r--theories/Program/Equality.v11
-rw-r--r--theories/Program/Subset.v1
-rw-r--r--theories/Program/Tactics.v4
-rw-r--r--theories/Program/Wf.v4
-rw-r--r--theories/QArith/Qcabs.v129
-rw-r--r--theories/QArith/Qcanon.v120
-rw-r--r--theories/QArith/Qreduction.v22
-rw-r--r--theories/QArith/vo.itarget1
-rw-r--r--theories/Reals/RIneq.v12
-rw-r--r--theories/Reals/Ranalysis_reg.v109
-rw-r--r--theories/Reals/Raxioms.v8
-rw-r--r--theories/Reals/Sqrt_reg.v2
-rw-r--r--theories/Relations/Operators_Properties.v2
-rw-r--r--theories/Relations/Relation_Definitions.v6
-rw-r--r--theories/Relations/Relation_Operators.v6
-rw-r--r--theories/Sets/Classical_sets.v2
-rw-r--r--theories/Sets/Constructive_sets.v2
-rw-r--r--theories/Sets/Ensembles.v5
-rw-r--r--theories/Sets/Finite_sets.v4
-rw-r--r--theories/Sets/Image.v2
-rw-r--r--theories/Sets/Multiset.v6
-rw-r--r--theories/Sets/Partial_Order.v4
-rw-r--r--theories/Sets/Powerset.v22
-rw-r--r--theories/Sets/Powerset_Classical_facts.v14
-rw-r--r--theories/Sets/Powerset_facts.v2
-rw-r--r--theories/Sets/Relations_1.v4
-rw-r--r--theories/Sets/Relations_2.v8
-rw-r--r--theories/Sets/Relations_3.v12
-rw-r--r--theories/Sorting/Permutation.v4
-rw-r--r--theories/Strings/Ascii.v2
-rw-r--r--theories/Strings/String.v10
-rw-r--r--theories/Structures/OrdersFacts.v6
-rw-r--r--theories/Vectors/VectorDef.v14
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v6
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v9
-rw-r--r--theories/ZArith/Int.v18
-rw-r--r--theories/ZArith/Zsqrt_compat.v4
-rw-r--r--theories/ZArith/Zwf.v4
-rw-r--r--theories/theories.itarget25
109 files changed, 1239 insertions, 580 deletions
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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.6 *) \ No newline at end of file
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
index 43b19700..7ffb86eb 100644
--- a/theories/Compat/vo.itarget
+++ b/theories/Compat/vo.itarget
@@ -1,3 +1,4 @@
AdmitAxiom.vo
Coq84.vo
Coq85.vo
+Coq86.vo
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index eaeb2914..3c5690a7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** * Basic facts about Prop as a type *)
+
+(** An intuitionistic theorem from topos theory [[LambekScott]]
+
+References:
+
+[[LambekScott]] Jim Lambek, Phil J. Scott, Introduction to higher
+order categorical logic, Cambridge Studies in Advanced Mathematics
+(Book 7), 1988.
+
+*)
+
+Theorem injection_is_involution_in_Prop
+ (f : Prop -> 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) <? lh) eqn:LT;
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791..9c622fd7 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.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 (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 "<?" := Nat.ltb (at level 70) : nat_scope.
+Infix "^" := Nat.pow : nat_scope.
+Infix "/" := Nat.div : nat_scope.
+Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
+Notation "( x | y )" := (Nat.divide x y) (at level 0) : nat_scope.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f..850afe53 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -104,18 +104,18 @@ Ltac isBigQcst t :=
| BigQ.Qz ?t => 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<y \/ x==y.
Proof. intros. qify. apply Qle_lteq. Qed.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 0ccfad7b..7baf102a 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -201,7 +201,6 @@ Proof.
Qed.
(** ** No neutral elements for addition *)
-
Lemma add_no_neutral p q : q + p <> 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 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** * An absolute value for normalized rational numbers. *)
+
+(** Contributed by Cédric Auger *)
+
+Require Import Qabs Qcanon.
+
+Lemma Qred_abs (x : Q) : Qred (Qabs x) = Qabs (Qred x).
+Proof.
+ destruct x as [[|a|a] d]; simpl; auto;
+ destruct (Pos.ggcd a d) as [x [y z]]; simpl; auto.
+Qed.
+
+Lemma Qcabs_canon (x : Q) : Qred x = x -> 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<q) <-> (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<y \/ x==y.
+Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y.
Proof.
- unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto.
+ unfold Qcle, Qclt; intros x y H.
+ destruct (Qle_lt_or_eq _ _ H); [left|right]; trivial.
+ now apply Qc_is_canon.
Qed.
(** Some decidability results about orders. *)
@@ -459,13 +474,13 @@ Proof.
induction n; simpl; auto with qarith.
rewrite IHn; auto with qarith.
Qed.
-Transparent Qred.
+
Lemma Qcpower_0 : forall n, n<>O -> 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 <? y) = match compare x y with Lt => 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