Working on determinacy proof.

1 files changed, 42 insertions, 10 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 8ad557b..2295ff6 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -34,6 +34,27 @@ 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 :=
@@ -51,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.
 
@@ -131,22 +153,32 @@ Ltac unfold_constants :=
            end
          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; unfold_constants; simpl in *;
-                 repeat (clear_obvious; nicify_goals; kill_bools);
+                 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 :=
-  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.
+  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.