From 589e1fedf62e25d939c0b7d91bc6c80917f42ec1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 7 Sep 2019 20:44:58 +0200
Subject: [PATCH] Add `iStopProof` tactic.

This commit closes issue #265.
---
 theories/proofmode/coq_tactics.v  | 18 ++++++++++++++++--
 theories/proofmode/environments.v | 22 +++++++++++++++++-----
 theories/proofmode/ltac_tactics.v | 10 ++++++++--
 theories/proofmode/reduction.v    |  3 ++-
 4 files changed, 43 insertions(+), 10 deletions(-)

diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index fbfb2a7ce..72164546d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -12,14 +12,28 @@ Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
 
-(** * Adequacy *)
-Lemma tac_adequate P : envs_entails (Envs Enil Enil 1) P → P.
+(** * Starting and stopping the proof mode *)
+Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → bi_emp_valid P.
 Proof.
   rewrite envs_entails_eq !of_envs_eq /=.
   rewrite intuitionistically_True_emp left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
 
+Lemma tac_stop Δ P :
+  (match env_intuitionistic Δ, env_spatial Δ with
+   | Enil, Γs => env_to_prop Γs
+   | Γp, Enil => □ env_to_prop_and Γp
+   | Γp, Γs => □ env_to_prop_and Γp ∗ env_to_prop Γs
+   end%I ⊢ P) →
+  envs_entails Δ P.
+Proof.
+  rewrite envs_entails_eq !of_envs_eq. intros <-.
+  rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
+  destruct (env_intuitionistic Δ), (env_spatial Δ);
+    by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
+Qed.
+
 (** * Basic rules *)
 Lemma tac_eval Δ Q Q' :
   (∀ (Q'':=Q'), Q'' ⊢ Q) → (* We introduce [Q''] as a let binding so that
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index a0e04eb0e..f3e8e93f7 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -364,11 +364,15 @@ Definition envs_split {PROP} (d : direction)
   ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
+Fixpoint env_to_prop_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
+  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P ∗ acc)%I Γ end.
 Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
-  let fix aux Γ acc :=
-    match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
-  in
-  match Γ with Enil => emp%I | Esnoc Γ _ P => aux Γ P end.
+  match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.
+
+Fixpoint env_to_prop_and_go {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
+  match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P ∧ acc)%I Γ end.
+Definition env_to_prop_and {PROP : bi} (Γ : env PROP) : PROP :=
+  match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
 
 Section envs.
 Context {PROP : bi}.
@@ -767,7 +771,15 @@ Qed.
 
 Lemma env_to_prop_sound Γ : env_to_prop Γ ⊣⊢ [∗] Γ.
 Proof.
-  destruct Γ as [|Γ ? P]; simpl; first done.
+  destruct Γ as [|Γ i P]; simpl; first done.
+  revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
+  - by rewrite right_id.
+  - rewrite /= IH (comm _ Q _) assoc. done.
+Qed.
+
+Lemma env_to_prop_and_sound Γ : env_to_prop_and Γ ⊣⊢ [∧] Γ.
+Proof.
+  destruct Γ as [|Γ i P]; simpl; first done.
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
   - by rewrite right_id.
   - rewrite /= IH (comm _ Q _) assoc. done.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 72ceda801..b63077368 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -71,7 +71,7 @@ Tactic Notation "iStartProof" :=
   | |- envs_entails _ _ => idtac
   | |- ?φ => notypeclasses refine (as_emp_valid_2 φ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_adequate]
+               |apply tac_start]
   end.
 
 (* Same as above, with 2 differences :
@@ -92,7 +92,13 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
      to find the corresponding bi. *)
   | |- ?φ => notypeclasses refine ((λ P : PROP, @as_emp_valid_2 φ _ P) _ _ _);
                [iSolveTC || fail "iStartProof: not a BI assertion"
-               |apply tac_adequate]
+               |apply tac_start]
+  end.
+
+Tactic Notation "iStopProof" :=
+  lazymatch goal with
+  | |- envs_entails _ _ => apply tac_stop; pm_reduce
+  | |- _ => fail "iStopProof: proofmode not started"
   end.
 
 (** * Generate a fresh identifier *)
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index c126c9bab..ba3090367 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -13,7 +13,8 @@ Declare Reduction pm_eval := cbv [
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
-  envs_split_go envs_split env_to_prop
+  envs_split_go envs_split
+  env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
 ].
-- 
GitLab