From 2bf052b6cc1f369cafb43f30704dea06f54ca9c3 Mon Sep 17 00:00:00 2001
From: Nicolas Nardino <nicolas.nardino@club-internet.fr>
Date: Wed, 28 Feb 2024 15:49:30 +0100
Subject: [PATCH] Separate tactics file + cleanup

---
 theories/examples/delim_lang/example.v | 26 +--------------------
 theories/examples/delim_lang/tactics.v | 32 ++++++++++++++++++++++++++
 2 files changed, 33 insertions(+), 25 deletions(-)
 create mode 100644 theories/examples/delim_lang/tactics.v

diff --git a/theories/examples/delim_lang/example.v b/theories/examples/delim_lang/example.v
index 3d8c808..4f03814 100644
--- a/theories/examples/delim_lang/example.v
+++ b/theories/examples/delim_lang/example.v
@@ -1,5 +1,5 @@
 From gitrees Require Import gitree lang_generic.
-From gitrees.examples.delim_lang Require Import lang interp.
+From gitrees.examples.delim_lang Require Import lang interp tactics.
 From iris.proofmode Require Import base classes tactics environments.
 From iris.base_logic Require Import algebra.
 
@@ -9,8 +9,6 @@ Example p : expr Empty_set :=
   ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))).
 
 Local Definition rs : gReifiers _ _ := gReifiers_cons reify_delim gReifiers_nil.
-(* Local Definition Hrs : subReifier reify_delim rs. *)
-(* Proof. unfold rs. apply subReifier_here. Qed. *)
 
 Notation F := (gReifiers_ops rs).
 Context {R} `{!Cofe R}.
@@ -28,28 +26,6 @@ Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}.
 Notation iProp := (iProp Σ).
 
 
-Ltac wp_ctx :=
-  match goal with
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x)
-                               (ofe_mor_car _ _ (?k2 ?t) ?e)) _ _ _) =>
-      assert (AsVal e) by apply _;
-      assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t e)) ≡ (λne x, k1 (k2 x e)) t) as -> by done
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) =>
-      assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ (?k ?t) ?e) _ _ _) =>
-      assert (AsVal e) by apply _;
-      assert (k t e ≡ (λne x, k x e) t) as -> by done
-  | |- envs_entails _ (wp _ (?k ?t) _ _ _) =>
-      assert (k t ≡ (λne x, k x) t) as -> by done
-  end.
-
-Ltac name_ctx k :=
-  match goal with
-  | |- envs_entails _ (wp _ (ofe_mor_car _ _ ?k1 _) _ _ _) =>
-      remember k1 as k
-  end.
-
-
 Lemma wp_t (s : gitree.weakestpre.stuckness) :
   has_substate σ -∗
   WP@{rs} t @ s {{βv, βv ≡ RetV 18}}.
diff --git a/theories/examples/delim_lang/tactics.v b/theories/examples/delim_lang/tactics.v
new file mode 100644
index 0000000..b1cfd09
--- /dev/null
+++ b/theories/examples/delim_lang/tactics.v
@@ -0,0 +1,32 @@
+From gitrees Require Import gitree lang_generic.
+From iris.proofmode Require Import base classes tactics environments.
+From iris.base_logic Require Import algebra.
+
+(* TODO: doc *)
+Ltac reshape_term α tac :=
+  match α with
+  | (ofe_mor_car _ _ (λne x, ?k1 x) (ofe_mor_car _ _ (?k2 ?t) ?e)) =>
+      assert (AsVal e) by apply _;
+      tac ((λne x, k1 (k2 x e)) t)
+  | (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) =>
+      tac ((λne x, k1 (k2 x)) t)
+  | (ofe_mor_car _ _ (?k ?t) ?e) =>
+      assert (AsVal e) by apply _;
+      tac ((λne x, k x e) t)
+  | (?k ?t) =>
+      tac ((λne x, k x) t)
+  end.
+
+(* TODO: doc *)
+Ltac wp_ctx :=
+  match goal with
+    |- envs_entails _ (wp _ ?e _ _ _) =>
+      reshape_term e ltac:(fun x => assert (e ≡ x) as -> by done)
+  end.
+
+(* TODO: doc *)
+Ltac name_ctx k :=
+  match goal with
+    |- envs_entails _ (wp _ (ofe_mor_car _ _ ?k1 _) _ _ _) =>
+      remember k1 as k
+  end.