1 files changed, 54 insertions, 6 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index c9361c2..469eddc 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -32,6 +32,29 @@ From coqup Require Import Show.
 From compcert.lib Require Export Coqlib.
 From compcert Require Import Integers.
 
+Local Open Scope Z_scope.
+
+(* 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 :=
@@ -49,10 +72,11 @@ Ltac invert x := inversion x; subst; clear x.
 Ltac destruct_match :=
   match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
 
-Ltac clear_obvious :=
+Ltac nicify_hypotheses :=
   repeat match goal with
          | [ H : ex _ |- _ ] => invert H
          | [ H : Some _ = Some _ |- _ ] => invert H
+         | [ H : ?x = ?x |- _ ] => clear H
          | [ H : _ /\ _ |- _ ] => invert H
          end.
 
@@ -129,16 +153,38 @@ Ltac unfold_constants :=
            end
          end.
 
-Ltac crush := intros; unfold_constants; simpl in *;
-              repeat (clear_obvious; nicify_goals; kill_bools);
-              simpl in *; try discriminate; try congruence; try lia; try assumption.
+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.
 
-Global Opaque Nat.div.
-Global Opaque Z.mul.
+Ltac simplify := intros; unfold_constants; simpl in *;
+                 repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp);
+                 simpl in *.
 
 Infix "==nat" := eq_nat_dec (no associativity, at level 50).
 Infix "==Z" := Z.eq_dec (no associativity, at level 50).
 
+Ltac liapp :=
+  repeat match goal with
+         | [ |- (?x | ?y) ] =>
+           match (eval compute in (Z.rem y x ==Z 0)) with
+           | left _ =>
+             let q := (eval compute in (Z.div y x))
+             in exists q; reflexivity
+           | _ => idtac
+          end
+         | _ => idtac
+         end.
+
+Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
+
+Global Opaque Nat.div.
+Global Opaque Z.mul.
+
 (* Definition const (A B : Type) (a : A) (b : B) : A := a.
 
 Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
@@ -189,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B :=
 
 Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B :=
   let unused := debug_print (s ++ show a) in b.
+
+Notation "f $ x" := (f x) (at level 60, right associativity, only parsing).