aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1912.v (renamed from test-suite/bugs/closed/shouldsucceed/bug1912.v)0
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2467.v49
-rw-r--r--theories/FSets/FSetDecide.v26
-rw-r--r--theories/MSets/MSetDecide.v26
4 files changed, 79 insertions, 22 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/bug1912.v b/test-suite/bugs/closed/shouldsucceed/1912.v
index 987a54177..987a54177 100644
--- a/test-suite/bugs/closed/shouldsucceed/bug1912.v
+++ b/test-suite/bugs/closed/shouldsucceed/1912.v
diff --git a/test-suite/bugs/closed/shouldsucceed/2467.v b/test-suite/bugs/closed/shouldsucceed/2467.v
new file mode 100644
index 000000000..ad17814a8
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2467.v
@@ -0,0 +1,49 @@
+(*
+In the code below, I would expect the
+ NameSetDec.fsetdec.
+to solve the Lemma, but I need to do it in steps instead.
+
+This is a regression relative to FSet,
+
+I have v8.3 (13702).
+*)
+
+Require Import Coq.MSets.MSets.
+
+Parameter Name : Set.
+Parameter Name_compare : Name -> Name -> comparison.
+Parameter Name_compare_sym : forall {x y : Name},
+ Name_compare y x = CompOpp (Name_compare x y).
+Parameter Name_compare_trans : forall {c : comparison}
+ {x y z : Name},
+ Name_compare x y = c
+ -> Name_compare y z = c
+ -> Name_compare x z = c.
+Parameter Name_eq_leibniz : forall {s s' : Name},
+ Name_compare s s' = Eq
+ -> s = s'.
+
+Module NameOrderedTypeAlt.
+Definition t := Name.
+Definition compare := Name_compare.
+Definition compare_sym := @Name_compare_sym.
+Definition compare_trans := @Name_compare_trans.
+End NameOrderedTypeAlt.
+
+Module NameOrderedType := OT_from_Alt(NameOrderedTypeAlt).
+
+Module NameOrderedTypeWithLeibniz.
+Include NameOrderedType.
+Definition eq_leibniz := @Name_eq_leibniz.
+End NameOrderedTypeWithLeibniz.
+
+Module NameSetMod := MSetList.MakeWithLeibniz(NameOrderedTypeWithLeibniz).
+Module NameSetDec := WDecide (NameSetMod).
+
+Lemma foo : forall (xs ys : NameSetMod.t)
+ (n : Name)
+ (H1 : NameSetMod.Equal xs (NameSetMod.add n ys)),
+ NameSetMod.In n xs.
+Proof.
+NameSetDec.fsetdec.
+Qed.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index cc78fdb4d..550a6900b 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -480,6 +480,13 @@ the above form:
F.union_iff F.inter_iff F.diff_iff
: set_simpl.
+ Lemma eq_refl_iff (x : E.t) : E.eq x x <-> True.
+ Proof.
+ now split.
+ Qed.
+
+ Hint Rewrite eq_refl_iff : set_eq_simpl.
+
(** ** Decidability of FSet Propositions *)
(** [In] is decidable. *)
@@ -556,8 +563,10 @@ the above form:
Ltac substFSet :=
repeat (
match goal with
+ | H: E.eq ?x ?x |- _ => clear H
| H: E.eq ?x ?y |- _ => rewrite H in *; clear H
- end).
+ end);
+ autorewrite with set_eq_simpl in *.
(** ** Considering Decidability of Base Propositions
This tactic adds assertions about the decidability of
@@ -637,13 +646,7 @@ the above form:
(** Here is the crux of the proof search. Recursion through
[intuition]! (This will terminate if I correctly
understand the behavior of [intuition].) *)
- Ltac fsetdec_rec :=
- try (match goal with
- | H: E.eq ?x ?x -> False |- _ => destruct H
- end);
- (reflexivity ||
- contradiction ||
- (progress substFSet; intuition fsetdec_rec)).
+ Ltac fsetdec_rec := progress substFSet; intuition fsetdec_rec.
(** If we add [unfold Empty, Subset, Equal in *; intros;] to
the beginning of this tactic, it will satisfy the same
@@ -651,12 +654,13 @@ the above form:
be much slower than necessary without the pre-processing
done by the wrapper tactic [fsetdec]. *)
Ltac fsetdec_body :=
+ autorewrite with set_eq_simpl in *;
inst_FSet_hypotheses;
- autorewrite with set_simpl in *;
+ autorewrite with set_simpl set_eq_simpl in *;
push not in * using FSet_decidability;
substFSet;
assert_decidability;
- auto using E.eq_refl;
+ auto;
(intuition fsetdec_rec) ||
fail 1
"because the goal is beyond the scope of this tactic".
@@ -874,5 +878,5 @@ Require Import FSetInterface.
the subtyping [WS<=S], the [Decide] functor which is meant to be
used on modules [(M:S)] can simply be an alias of [WDecide]. *)
-Module WDecide (M:WS) := WDecide_fun M.E M.
+Module WDecide (M:WS) := !WDecide_fun M.E M.
Module Decide := WDecide.
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index 1646ea7fa..6abd19111 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -480,6 +480,13 @@ the above form:
F.union_iff F.inter_iff F.diff_iff
: set_simpl.
+ Lemma eq_refl_iff (x : E.t) : E.eq x x <-> True.
+ Proof.
+ now split.
+ Qed.
+
+ Hint Rewrite eq_refl_iff : set_eq_simpl.
+
(** ** Decidability of MSet Propositions *)
(** [In] is decidable. *)
@@ -556,8 +563,10 @@ the above form:
Ltac substMSet :=
repeat (
match goal with
+ | H: E.eq ?x ?x |- _ => clear H
| H: E.eq ?x ?y |- _ => rewrite H in *; clear H
- end).
+ end);
+ autorewrite with set_eq_simpl in *.
(** ** Considering Decidability of Base Propositions
This tactic adds assertions about the decidability of
@@ -637,13 +646,7 @@ the above form:
(** Here is the crux of the proof search. Recursion through
[intuition]! (This will terminate if I correctly
understand the behavior of [intuition].) *)
- Ltac fsetdec_rec :=
- try (match goal with
- | H: E.eq ?x ?x -> False |- _ => destruct H
- end);
- (reflexivity ||
- contradiction ||
- (progress substMSet; intuition fsetdec_rec)).
+ Ltac fsetdec_rec := progress substMSet; intuition fsetdec_rec.
(** If we add [unfold Empty, Subset, Equal in *; intros;] to
the beginning of this tactic, it will satisfy the same
@@ -651,12 +654,13 @@ the above form:
be much slower than necessary without the pre-processing
done by the wrapper tactic [fsetdec]. *)
Ltac fsetdec_body :=
+ autorewrite with set_eq_simpl in *;
inst_MSet_hypotheses;
- autorewrite with set_simpl in *;
+ autorewrite with set_simpl set_eq_simpl in *;
push not in * using MSet_decidability;
substMSet;
assert_decidability;
- auto using (@Equivalence_Reflexive _ _ E.eq_equiv);
+ auto;
(intuition fsetdec_rec) ||
fail 1
"because the goal is beyond the scope of this tactic".
@@ -874,5 +878,5 @@ Require Import MSetInterface.
the subtyping [WS<=S], the [Decide] functor which is meant to be
used on modules [(M:S)] can simply be an alias of [WDecide]. *)
-Module WDecide (M:WSets) := WDecideOn M.E M.
+Module WDecide (M:WSets) := !WDecideOn M.E M.
Module Decide := WDecide.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 11:26:00 +0000