Skip to content

C
cpdt
Commit f889978a authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

crush' pursues trivial inversions

parent 2cadc205
Hide whitespace changes
Inline Side-by-side
Showing with 8 additions and 5 deletions
src/Tactics.v
View file @ f889978a
......@@ -42,6 +42,9 @@ Ltac all f ls :=
end.
Ltac simplHyp invOne :=
let invert H F :=
inList F invOne; (inversion H; fail)
|| (inversion H; [idtac]; clear H; try subst) in
match goal with
| [ H : ex _ |- _ ] => destruct H
......@@ -54,11 +57,11 @@ Ltac simplHyp invOne :=
| [ |- _ = _ -> _ = _ -> _ ] => try clear H; intros; try subst
end
| [ H : ?F _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
| [ H : ?F _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
| [ H : ?F _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
| [ H : ?F _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
| [ H : ?F _ _ _ _ _ |- _ ] => inList F invOne; inversion H; [idtac]; clear H; try subst
| [ H : ?F _ |- _ ] => invert H F
| [ H : ?F _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ |- _ ] => invert H F
| [ H : ?F _ _ _ _ _ |- _ ] => invert H F
end.
Ltac rewriteHyp :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment