From d1c9de736aa576ab31a114d65d67db6e10ef8bec Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 7 Oct 2011 11:29:50 +0000 Subject: Improved handling of element equalities in fsetdec (fix #2467) - We now handle things like (H : E.eq x x -> ...) by rewriting E.eq x x into True. - There was also a confusion between E.t and its various equivalent (but syntactically different) forms. This should be solved by preventing inlining during an inner functor application. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14520 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/FSets/FSetDecide.v | 26 +++++++++++++++----------- 1 file changed, 15 insertions(+), 11 deletions(-) (limited to 'theories/FSets') 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. -- cgit v1.2.3