From 39278439ad26cb5eb22b496066c0f044c33ef28b Mon Sep 17 00:00:00 2001 From: "xavier.leroy" Date: Sat, 25 Jan 2020 18:59:33 -0600 Subject: Reduce the checking time for the "decidable_equality_from" tactic Just moved a frequent failure case ahead of a costly "simpl". --- lib/BoolEqual.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'lib/BoolEqual.v') diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index c9e7bad5..e8c1d831 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -106,8 +106,8 @@ Ltac bool_eq_refl_case := end. Ltac bool_eq_refl := - let H := fresh "Hrec" in let x := fresh "x" in - fix H 1; intros x; destruct x; simpl; bool_eq_refl_case. + let Hrec := fresh "Hrec" in let x := fresh "x" in + fix Hrec 1; intros x; destruct x; simpl; bool_eq_refl_case. Lemma false_not_true: forall (P: Prop), false = true -> P. @@ -124,7 +124,6 @@ Qed. Ltac bool_eq_sound_case := match goal with - | [ H: false = true |- _ ] => exact (false_not_true _ H) | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto @@ -137,7 +136,9 @@ Ltac bool_eq_sound_case := Ltac bool_eq_sound := let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in - fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case. + let H := fresh "EQ" in + fix Hrec 1; intros x y; destruct x, y; intro H; + try (apply (false_not_true _ H)); simpl in H; bool_eq_sound_case. Lemma dec_eq_from_bool_eq: forall (A: Type) (f: A -> A -> bool) -- cgit