From 59c40033462c08095b068e490ab3ef246ddb67f5 Mon Sep 17 00:00:00 2001 From: Jerome Hugues <50238921+jjhugues@users.noreply.github.com> Date: Sat, 25 Jun 2022 10:44:02 +0200 Subject: Extend the boolean_equality tactic (#429) Handle constructors with 5, 6 and 7 arguments. Handle lists. --- lib/BoolEqual.v | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index 6479c1ee..ee9a9226 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -65,12 +65,26 @@ Ltac bool_eq_base x y := change (bool_eq x y); match goal with | [ H: forall (x y: ?A), bool |- @bool_eq ?A x y ] => exact (H x y) - | [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq ?A x y ] => exact (proj_sumbool (H x y)) + | [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq ?A x y ] => exact (proj_sumbool (H x y)) + | [ H: forall (x y: ?A), {x=y} + {x<>y} |- @bool_eq (list ?A) x y ] => exact (proj_sumbool (list_eq_dec H x y)) | _ => idtac end. Ltac bool_eq_case := match goal with + | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4 ?x5 ?x6 ?x7) (?C ?y1 ?y2 ?y3 ?y4 ?y5 ?y6 ?y7) => + refine (_ && _ && _ && _ && _ && _ && _); + [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3| + bool_eq_base x4 y4|bool_eq_base x5 y5|bool_eq_base x6 y6| + bool_eq_base x7 y7] + | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4 ?x5 ?x6) (?C ?y1 ?y2 ?y3 ?y4 ?y5 ?y6) => + refine (_ && _ && _ && _ && _ && _); + [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3| + bool_eq_base x4 y4|bool_eq_base x5 y5|bool_eq_base x6 y6] + | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4 ?x5) (?C ?y1 ?y2 ?y3 ?y4 ?y5) => + refine (_ && _ && _ && _ && _); + [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3| + bool_eq_base x4 y4|bool_eq_base x5 y5] | |- bool_eq (?C ?x1 ?x2 ?x3 ?x4) (?C ?y1 ?y2 ?y3 ?y4) => refine (_ && _ && _ && _); [bool_eq_base x1 y1|bool_eq_base x2 y2|bool_eq_base x3 y3|bool_eq_base x4 y4] | |- bool_eq (?C ?x1 ?x2 ?x3) (?C ?y1 ?y2 ?y3) => -- cgit