From 8fa89c3e400fff4e9a4ec28eba6393cdca48362b Mon Sep 17 00:00:00 2001 From: Michalis Pardalos Date: Fri, 7 May 2021 19:16:55 +0100 Subject: Fully clean up the iter_expand_instr_spec proof --- src/common/Vericertlib.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/common') 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. -- cgit