1 files changed, 115 insertions, 0 deletions
diff --git a/src/Common.v b/src/Common.v
new file mode 100644
index 0000000..2e5523b
--- /dev/null
+++ b/src/Common.v
@@ -0,0 +1,115 @@
+Require Export Coq.Bool.Bool.
+Require Export Coq.Lists.List.
+Require Export Coq.Strings.String.
+Require Export Coq.ZArith.ZArith.
+Require Export Coq.ZArith.Znumtheory.
+Require Import Coq.micromega.Lia.
+
+Require Export TVSMT.Coqlib.
+(* Require Import compcert.lib.Integers. *)
+Require Export TVSMT.Errors.
+
+(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to
+   allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *)
+Inductive Learnt {A: Type} (a: A) :=
+  | AlreadyKnown : Learnt a.
+
+Ltac learn_tac fact name :=
+  lazymatch goal with
+  | [ H: Learnt fact |- _ ] =>
+    fail 0 "fact" fact "has already been learnt"
+  | _ => let type := type of fact in
+        lazymatch goal with
+        | [ H: @Learnt type _ |- _ ] =>
+          fail 0 "fact" fact "of type" type "was already learnt through" H
+        | _ => let learnt := fresh "Learn" in
+              pose proof (AlreadyKnown fact) as learnt; pose proof fact as name
+        end
+  end.
+
+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 unfold_rec c := unfold c; fold c.
+
+Ltac solve_by_inverts n :=
+  match goal with | H : ?T |- _ =>
+    match type of T with Prop =>
+      inversion H;
+      match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end
+    end
+  end.
+
+Ltac solve_by_invert := solve_by_inverts 1.
+
+Ltac invert x := inversion x; subst; clear x.
+
+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 auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence.
+
+Ltac nicify_hypotheses :=
+  repeat match goal with
+         | [ H : ex _ |- _ ] => invert H
+         | [ H : Some _ = Some _ |- _ ] => invert H
+         | [ H : OK _ = OK _ |- _ ] => invert H
+         | [ H : ?x = ?x |- _ ] => clear H
+         | [ H : _ /\ _ |- _ ] => invert H
+         | [ H : (_, _) = (_, _) |- _ ] => invert H
+         end.
+
+Ltac nicify_goals :=
+  repeat match goal with
+         | [ |- _ /\ _ ] => split
+         | [ |- Some _ = Some _ ] => f_equal
+         | [ |- OK _ = OK _ ] => f_equal
+         | [ |- S _ = S _ ] => f_equal
+         end.
+
+Ltac kill_bools :=
+  repeat match goal with
+         | [ H : _ && _ = true |- _ ] => apply andb_prop in H
+         | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H
+         | [ H : negb _ = true |- _ ] => apply negb_true_iff in H
+         | [ H : negb _ = false |- _ ] => apply negb_false_iff in H
+
+         | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H
+         | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H
+         | [ H : _ <? _ = true |- _ ] => apply Z.ltb_lt in H
+         | [ H : _ <? _ = false |- _ ] => apply Z.ltb_ge in H
+         | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H
+         | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H
+
+         | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H
+         | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H
+
+         | [ H : (_ <=? _)%positive = true |- _ ] => apply Pos.leb_le in H
+         | [ H : (_ <=? _)%positive = false |- _ ] => apply Pos.leb_gt in H
+         | [ H : (_ <? _)%positive = true |- _ ] => apply Pos.ltb_lt in H
+         | [ H : (_ <? _)%positive = false |- _ ] => apply Pos.ltb_ge in H
+
+         | [ H : (_ =? _)%positive = true |- _ ] => apply Pos.eqb_eq in H
+         | [ H : (_ =? _)%positive = false |- _ ] => apply Pos.eqb_neq in H
+         end.
+
+Ltac substpp :=
+  repeat match goal with
+         | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] =>
+           let EQ := fresh "EQ" in
+           learn H1 as EQ; rewrite H2 in EQ; invert EQ
+         | _ => idtac
+         end.
+
+Ltac simplify := intros; simpl in *;
+                 repeat progress (try nicify_hypotheses; try nicify_goals; try kill_bools; substpp);
+                 simpl in *.
+
+Ltac crush := simplify; try discriminate; try congruence; try (zify; lia);
+              try assumption; try (solve [auto]).
+
+Ltac ecrush m := simplify; try discriminate; try congruence; try (zify; lia);
+                 try assumption; try (solve [eauto with m]).