From 3c6f213c1adc03a8b1a4543ef9bf80bd6b5d4be9 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva <lord@crocodile.org>
Date: Wed, 1 Nov 2023 16:21:19 -0700
Subject: [PATCH] moving tactics to separate .v

---
 coq/Proofs/Revocation.v | 47 ++---------------------------------------
 coq/Proofs/Tactics.v    | 43 +++++++++++++++++++++++++++++++++++++
 coq/Proofs/dune         |  2 +-
 3 files changed, 46 insertions(+), 46 deletions(-)
 create mode 100644 coq/Proofs/Tactics.v

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
index 44723d07c..5da4e5e53 100644
--- a/coq/Proofs/Revocation.v
+++ b/coq/Proofs/Revocation.v
@@ -29,6 +29,8 @@ From Morello Require Import CapabilitiesGS MorelloCapsGS.
 
 From CheriMemory Require Import CheriMorelloMemory Memory_model CoqMem_common ErrorWithState CoqUndefined ErrorWithState CoqLocation CoqSymbol CoqImplementation CoqTags CoqSwitches CerbSwitches CoqAilTypesAux.
 
+Require Import Tactics.
+
 Local Open Scope string_scope.
 Local Open Scope type_scope.
 Local Open Scope list_scope.
@@ -54,18 +56,6 @@ Module AbstTagDefs: TagDefs.
   Definition tagDefs := abst_tagDefs.
 End AbstTagDefs.
 
-(* This (seemingly) prevents slow `Qed` problem.
-   Usage: replace `cbn in H` with `cbn_hyp H`.
-
-   See aslo:
-     - discussion: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Coq.20hangs.20on.20Qed
-     - FAQ: https://github.com/coq/coq/wiki/Troubleshooting#what-can-i-do-when-qed-is-slow
-
-   TODO: move to separate file with other tactics we define
- *)
-Ltac cbn_hyp H :=
-  let T := type of H in let T' := eval cbn in T in replace T with T' in H by (cbn;reflexivity).
-
 Module RevocationProofs.
 
   (* --- Memory models instantiated with and without PNVI --- *)
@@ -1140,39 +1130,6 @@ Module RevocationProofs.
 
   End allocate_region_proofs.
 
-  (* TODO : move *)
-  Ltac inl_inr :=
-    match goal with
-    | [H1: inl _ = inr _ |- _] => inversion H1
-    | [H1: inr _ = inl _ |- _] => inversion H1
-
-    | [H1: inl _ = Monad.ret _ |- _] => inversion H1
-    | [H1: Monad.ret _ = inl _ |- _] => inversion H1
-
-    | [H1: raise _ = inr _ |- _] => inversion H1
-    | [H1: inr _ = raise _ |- _] => inversion H1
-
-    | [ |- inl ?x = inl ?x ] => reflexivity
-    | [ |- inr ?x = inr ?x ] => reflexivity
-
-    | [H1: ?a = inr _,
-          H2: ?a = inl _ |- _] => rewrite H1 in H2;
-                                inversion H2
-
-    end.
-
-  (* TODO : move *)
-  Ltac inl_inr_inv :=
-    match goal with
-    | [H1: inl _ = inl _ |- _] => inversion H1; clear H1
-    | [H1: inr _ = inr _ |- _] => inversion H1; clear H1
-
-    | [H1: inr _ = Monad.ret _ |- _] => inversion H1; clear H1
-    | [H1: Monad.ret _ = inr _ |- _] => inversion H1; clear H1
-    | [H1: raise _ = inl _ |- _] => inversion H1; clear H1
-    | [H1: inl _ = raise _ |- _] => inversion H1; clear H1
-    end.
-
   Lemma bind_Same_eq {T1 T2 T:Type}
     {R: T1 -> T2 -> Prop} (* relation between values *)
     {M1: CheriMemoryWithPNVI.memM T}
diff --git a/coq/Proofs/Tactics.v b/coq/Proofs/Tactics.v
new file mode 100644
index 000000000..0baffa117
--- /dev/null
+++ b/coq/Proofs/Tactics.v
@@ -0,0 +1,43 @@
+From ExtLib.Structures Require Import Monad Monads MonadExc MonadState Traversable.
+From ExtLib.Data.Monads Require Import EitherMonad OptionMonad.
+
+(* This (seemingly) prevents slow `Qed` problem.
+   Usage: replace `cbn in H` with `cbn_hyp H`.
+
+   See aslo:
+     - discussion: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Coq.20hangs.20on.20Qed
+     - FAQ: https://github.com/coq/coq/wiki/Troubleshooting#what-can-i-do-when-qed-is-slow
+ *)
+Ltac cbn_hyp H :=
+  let T := type of H in let T' := eval cbn in T in replace T with T' in H by (cbn;reflexivity).
+
+Ltac inl_inr :=
+  match goal with
+  | [H1: inl _ = inr _ |- _] => inversion H1
+  | [H1: inr _ = inl _ |- _] => inversion H1
+
+  | [H1: inl _ = Monad.ret _ |- _] => inversion H1
+  | [H1: Monad.ret _ = inl _ |- _] => inversion H1
+
+  | [H1: raise _ = inr _ |- _] => inversion H1
+  | [H1: inr _ = raise _ |- _] => inversion H1
+
+  | [ |- inl ?x = inl ?x ] => reflexivity
+  | [ |- inr ?x = inr ?x ] => reflexivity
+
+  | [H1: ?a = inr _,
+        H2: ?a = inl _ |- _] => rewrite H1 in H2;
+                              inversion H2
+
+  end.
+
+Ltac inl_inr_inv :=
+  match goal with
+  | [H1: inl _ = inl _ |- _] => inversion H1; clear H1
+  | [H1: inr _ = inr _ |- _] => inversion H1; clear H1
+
+  | [H1: inr _ = Monad.ret _ |- _] => inversion H1; clear H1
+  | [H1: Monad.ret _ = inr _ |- _] => inversion H1; clear H1
+  | [H1: raise _ = inl _ |- _] => inversion H1; clear H1
+  | [H1: inl _ = raise _ |- _] => inversion H1; clear H1
+  end.
diff --git a/coq/Proofs/dune b/coq/Proofs/dune
index 2d1572579..3b300b502 100644
--- a/coq/Proofs/dune
+++ b/coq/Proofs/dune
@@ -2,6 +2,6 @@
  (mode vo)
  (name Proofs)
  (package cerberus-cheri)
- (modules Revocation)
+ (modules Tactics Revocation)
  (theories CheriMemory Common Morello)
 )