1 files changed, 53 insertions, 1 deletions

diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index b58ebd4..84c272b 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -57,6 +57,19 @@ Ltac learn_tac fact name :=
 Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name.
 Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name.
 
+Ltac auto_apply fact :=
+  let H' := fresh "H" in
+  match goal with
+  | H : _ |- _ => pose proof H as H'; apply fact in H'
+  end.
+
+(** Specialize all hypotheses with a forall to a specific term *)
+Tactic Notation "specialize_all" constr(v) :=
+  let t := type of v in
+  repeat match goal with
+         | [H : (forall (x: t), _) |- _ ] => learn H; destruct H with v
+         end.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
@@ -71,12 +84,30 @@ Ltac solve_by_invert := solve_by_inverts 1.
 
 Ltac invert x := inversion x; subst; clear x.
 
+(** For a hypothesis of a forall-type, instantiate every variable to a fresh existential *)
+Ltac insterU1 H :=
+  match type of H with
+  | forall x : ?T, _ =>
+    let x := fresh "x" in
+    evar (x : T);
+    let x' := eval unfold x in x in
+        clear x; specialize (H x')
+  end.
+
+Ltac insterU H :=
+  repeat (insterU1 H).
+
 Ltac destruct_match :=
   match goal with
   | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:?
   | [ 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 :=
@@ -187,9 +218,21 @@ Ltac liapp :=
          | _ => idtac
          end.
 
-Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
+Ltac plia := solve [ unfold Ple in *; lia ].
+
+Ltac crush := simplify; try discriminate; try congruence; try plia; 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.
+
+Ltac maybe t := t + idtac.
+
 Global Opaque Nat.div.
 Global Opaque Z.mul.
 
@@ -229,6 +272,15 @@ Definition join {A : Type} (a : option (option A)) : option A :=
   | Some a' => a'
   end.
 
+Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B :=
+  match l with
+  | nil => nil
+  | x::xs => match f x with
+           | None => map_option f xs
+           | Some x' => x'::map_option f xs
+           end
+  end.
+
 Module Notation.
 Notation "'do' X <- A ; B" := (bind A (fun X => B))
    (at level 200, X ident, A at level 100, B at level 200).