diff options
| author | Jerome Hugues <50238921+jjhugues@users.noreply.github.com> | 2022-06-25 10:44:02 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-06-25 10:44:02 +0200 |
| commit | 59c40033462c08095b068e490ab3ef246ddb67f5 (patch) | |
| tree | 31c021bacd96648acac85904cee66245afdeefd4 | |
| parent | 971c8ea8397b74aabfe0245d3f1c0645f3f77554 (diff) | |
| download | compcert-59c40033462c08095b068e490ab3ef246ddb67f5.tar.gz compcert-59c40033462c08095b068e490ab3ef246ddb67f5.zip | |
Extend the boolean_equality tactic (#429)
Handle constructors with 5, 6 and 7 arguments.
Handle lists.
| -rw-r--r-- | lib/BoolEqual.v | 16 |
1 files changed, 15 insertions, 1 deletions
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) => |