diff options
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/Vericertlib.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 1c5c37f..48edd08 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -90,6 +90,11 @@ Ltac destruct_match := | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? end. +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := @@ -203,6 +208,14 @@ Ltac liapp := Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption; try (solve [auto]). +Ltac crush_trans := + match goal with + | [ H : ?g = ?inter |- ?g = _ ] => transitivity inter; crush + | [ H : ?inter = ?g |- ?g = _ ] => transitivity inter; crush + | [ H : ?g = ?inter |- _ = ?g ] => transitivity inter; crush + | [ H : ?inter = ?g |- _ = ?g ] => transitivity inter; crush + end. + Global Opaque Nat.div. Global Opaque Z.mul. |