aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Classes/EquivDec.v2
-rw-r--r--theories/Classes/RelationClasses.v2
-rw-r--r--theories/FSets/FMapFacts.v14
-rw-r--r--theories/FSets/FSetProperties.v2
-rw-r--r--theories/Reals/RIneq.v10
-rw-r--r--theories/Reals/ROrderedType.v2
-rw-r--r--theories/Structures/OrderedType.v4
-rw-r--r--theories/Structures/OrdersLists.v2
-rw-r--r--theories/ZArith/Znumtheory.v46
9 files changed, 38 insertions, 46 deletions
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index 9f44d4fefa..87f86e0d36 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -139,7 +139,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
| _, _ => in_right
end }.
- Next Obligation. destruct y ; intuition eauto. Defined.
+ Next Obligation. destruct y ; unfold not in *; eauto. Defined.
Solve Obligations with unfold equiv, complement in * ;
program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index a8de1ba081..3717e1cb46 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -130,7 +130,7 @@ Tactic Notation "apply" "*" constr(t) :=
Ltac simpl_relation :=
unfold flip, impl, arrow ; try reduce ; program_simpl ;
- try ( solve [ intuition ]).
+ try ( solve [ dintuition ]).
Local Obligation Tactic := simpl_relation.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 0c1448c9bb..9fef1dc638 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -519,7 +519,7 @@ Proof.
intros. rewrite eq_option_alt. intro e.
rewrite <- find_mapsto_iff, elements_mapsto_iff.
unfold eqb.
-rewrite <- findA_NoDupA; intuition; try apply elements_3w; eauto.
+rewrite <- findA_NoDupA; dintuition; try apply elements_3w; eauto.
Qed.
Lemma elements_b : forall m x,
@@ -679,8 +679,8 @@ Add Parametric Morphism elt : (@Empty elt)
with signature Equal ==> iff as Empty_m.
Proof.
unfold Empty; intros m m' Hm; intuition.
-rewrite <-Hm in H0; eauto.
-rewrite Hm in H0; eauto.
+rewrite <-Hm in H0; eapply H, H0.
+rewrite Hm in H0; eapply H, H0.
Qed.
Add Parametric Morphism elt : (@is_empty elt)
@@ -1872,13 +1872,7 @@ Module OrdProperties (M:S).
add_mapsto_iff by (auto with *).
unfold O.eqke, O.ltk; simpl.
destruct (E.compare t0 x); intuition.
- right; split; auto; ME.order.
- ME.order.
- elim H.
- exists e0; apply MapsTo_1 with t0; auto.
- right; right; split; auto; ME.order.
- ME.order.
- right; split; auto; ME.order.
+ elim H; exists e0; apply MapsTo_1 with t0; auto.
Qed.
Lemma elements_Add_Above : forall m m' x e,
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 1bad806152..eec7196b78 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -995,8 +995,6 @@ Module OrdProperties (M:S).
leb_1, gtb_1, (H0 a) by auto with *.
intuition.
destruct (E.compare a x); intuition.
- right; right; split; auto with *.
- ME.order.
Qed.
Definition Above x s := forall y, In y s -> E.lt y x.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 70f4ff0d9b..944e7da210 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -43,7 +43,7 @@ Hint Immediate Rge_refl: rorders.
Lemma Rlt_irrefl : forall r, ~ r < r.
Proof.
- generalize Rlt_asym. intuition eauto.
+ intros r H; eapply Rlt_asym; eauto.
Qed.
Hint Resolve Rlt_irrefl: real.
@@ -64,7 +64,9 @@ Qed.
(**********)
Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
Proof.
- generalize Rlt_not_eq Rgt_not_eq. intuition eauto.
+ intuition.
+ - apply Rlt_not_eq in H1. eauto.
+ - apply Rgt_not_eq in H1. eauto.
Qed.
Hint Resolve Rlt_dichotomy_converse: real.
@@ -74,7 +76,7 @@ Hint Resolve Rlt_dichotomy_converse: real.
Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
Proof.
intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
- intuition eauto 3.
+ unfold not; intuition eauto 3.
Qed.
Hint Resolve Req_dec: real.
@@ -175,7 +177,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed.
Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
Proof.
generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
- intuition eauto 3.
+ unfold not; intuition eauto 3.
Qed.
Hint Immediate Rlt_not_le: real.
diff --git a/theories/Reals/ROrderedType.v b/theories/Reals/ROrderedType.v
index 0a8d89c77f..eeafbde9b9 100644
--- a/theories/Reals/ROrderedType.v
+++ b/theories/Reals/ROrderedType.v
@@ -15,7 +15,7 @@ Local Open Scope R_scope.
Lemma Req_dec : forall r1 r2:R, {r1 = r2} + {r1 <> r2}.
Proof.
intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
- intuition eauto 3.
+ intuition eauto.
Qed.
Definition Reqb r1 r2 := if Req_dec r1 r2 then true else false.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f84cdf32cf..beb10a8335 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -223,7 +223,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
Proof. exact (InfA_ltA lt_strorder). Qed.
Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
@@ -396,7 +396,7 @@ Module KeyOrderedType(O:OrderedType).
Qed.
Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l.
- Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed.
+ Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed.
Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
Proof. exact (InfA_ltA ltk_strorder). Qed.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index f83b637798..059992f5b0 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -32,7 +32,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l.
Proof. exact (InfA_ltA lt_strorder). Qed.
Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l.
-Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed.
+Proof. exact (InfA_eqA eq_equiv lt_compat). Qed.
Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x.
Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 6eb1a70939..2d4bfb2e3d 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -575,30 +575,29 @@ Lemma prime_divisors :
forall p:Z,
prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
Proof.
- simple induction 1; intros.
+ destruct 1; intros.
assert
(a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p).
- assert (Zabs a <= Zabs p). apply Zdivide_bounds; [ assumption | omega ].
- generalize H3.
- pattern (Zabs a) in |- *; apply Zabs_ind; pattern (Zabs p) in |- *;
- apply Zabs_ind; intros; omega.
+ { assert (Zabs a <= Zabs p) as H2.
+ apply Zdivide_bounds; [ assumption | omega ].
+ revert H2.
+ pattern (Zabs a); apply Zabs_ind; pattern (Zabs p); apply Zabs_ind;
+ intros; omega. }
intuition idtac.
(* -p < a < -1 *)
- absurd (rel_prime (- a) p); intuition.
- inversion H3.
- assert (- a | - a); auto with zarith.
- assert (- a | p); auto with zarith.
- generalize (H8 (- a) H9 H10); intuition idtac.
- generalize (Zdivide_1 (- a) H11); intuition.
+ - absurd (rel_prime (- a) p); intuition.
+ inversion H2.
+ assert (- a | - a) by auto with zarith.
+ assert (- a | p) by auto with zarith.
+ apply H7, Zdivide_1 in H8; intuition.
(* a = 0 *)
- inversion H2. subst a; omega.
+ - inversion H1. subst a; omega.
(* 1 < a < p *)
- absurd (rel_prime a p); intuition.
- inversion H3.
- assert (a | a); auto with zarith.
- assert (a | p); auto with zarith.
- generalize (H8 a H9 H10); intuition idtac.
- generalize (Zdivide_1 a H11); intuition.
+ - absurd (rel_prime a p); intuition.
+ inversion H2.
+ assert (a | a) by auto with zarith.
+ assert (a | p) by auto with zarith.
+ apply H7, Zdivide_1 in H8; intuition.
Qed.
(** A prime number is relatively prime with any number it does not divide *)
@@ -606,11 +605,10 @@ Qed.
Lemma prime_rel_prime :
forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
Proof.
- simple induction 1; intros.
- constructor; intuition.
- elim (prime_divisors p H x H3); intuition; subst; auto with zarith.
- absurd (p | a); auto with zarith.
- absurd (p | a); intuition.
+ intros; constructor; intros; auto with zarith.
+ apply prime_divisors in H1; intuition; subst; auto with zarith.
+ - absurd (p | a); auto with zarith.
+ - absurd (p | a); intuition.
Qed.
Hint Resolve prime_rel_prime: zarith.
@@ -635,7 +633,7 @@ Lemma prime_mult :
forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
Proof.
intro p; simple induction 1; intros.
- case (Zdivide_dec p a); intuition.
+ case (Zdivide_dec p a); nintuition.
right; apply Gauss with a; auto with zarith.
Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-18 17:46:02 +0000