Merge branch 'robbert/istopproof' into 'master'

Add `iStopProof` tactic

Closes #265

See merge request iris/iris!311

CHANGELOG.md

@@ -3,6 +3,13 @@ way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
 `[#]` still need to be ported to the Iris Documentation LaTeX file(s).
 
+## Iris master
+
+**Changes in Coq:**
+
+* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
+  Coq goal `big star of context ⊢ proof mode goal`.
+
 ## Iris 3.2.0 (released 2019-08-29)
 
 The highlight of this release is the completely re-engineered interactive proof

ProofMode.md

@@ -8,6 +8,18 @@ of the tactics can be applied when the connective to be introduced or to be elim
 appears under a later, an update modality, or in the conclusion of a
 weakest precondition.
 
+Starting and stopping the proof mode
+------------------------------------
+
+- `iStartProof PROP` : start the proof mode by turning a Coq goal into a proof
+  mode entailment. This tactic is performed implicitly by all proof mode tactics
+  described in this file, and thus should generally not be used by hand. The
+  optional argument `PROP` can be used to explicitly specify which BI logic
+  `PROP : bi` should be used. This is useful to drop down in a layered logic,
+  e.g. to drop down from `monPred PROP` to `PROP`.
+- `iStopProof` to turn the proof mode entailment into an ordinary Coq goal
+  `big star of context ⊢ proof mode goal`.
+
 Applying hypotheses and lemmas
 ------------------------------
 

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

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.

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 *)

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
 ].