diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-07 19:16:55 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-07 19:16:55 +0100 |
| commit | 8fa89c3e400fff4e9a4ec28eba6393cdca48362b (patch) | |
| tree | 0d46970b3c4cb8f5ca46f26eb05ec5f1b67bc806 /src/common | |
| parent | 8a6cee2918b73b97026dc4010f85e2cf52297470 (diff) | |
| download | vericert-8fa89c3e400fff4e9a4ec28eba6393cdca48362b.tar.gz vericert-8fa89c3e400fff4e9a4ec28eba6393cdca48362b.zip | |
Fully clean up the iter_expand_instr_spec proof
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. |