Merge branch 'robbert/intuitionistic_inv' into 'master'

Add introduction pattern `-# pat` to move a hypothesis to the spatial context

Closes #213

See merge request iris/iris!370

CHANGELOG.md

@@ -65,6 +65,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   lemmas is through `iInv`, and that does not change.)
 * Added a construction `bi_rtc` to create reflexive transitive closures of
   PROP-level binary relations.
+* Add new introduction pattern `-# pat` that moves a hypothesis from the
+  intuitionistic context to the spatial context.
 
 ## Iris 3.2.0 (released 2019-08-29)
 

docs/proof_mode.md

@@ -227,7 +227,16 @@ _introduction patterns_:
 - `[]` : false elimination.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
 - `->` and `<-` : rewrite using a pure Coq equality
-- `# ipat` : move the hypothesis into the intuitionistic context.
+- `# ipat` : move the hypothesis into the intuitionistic context. The tactic
+  will fail if the hypothesis is not intuitionistic. On success, the tactic will
+  strip any number of intuitionistic and persistence modalities. If the
+  hypothesis is already in the intuitionistic context, the tactic will still
+  strip intuitionistic and persistence modalities (it is a no-op if the
+  hypothesis does not contain such modalities).
+- `-# ipat` : move the hypothesis from the intuitionistic context into the
+  spatial context. If the hypothesis is already in the spatial context, the
+  tactic is a no-op. If the hypothesis is not affine, an `<affine>` modality is
+  added to the hypothesis.
 - `> ipat` : eliminate a modality (if the goal permits).
 
 Apart from this, there are the following introduction patterns that can only

tests/proofmode.ref

@@ -54,6 +54,29 @@
   --------------------------------------□
   <affine> (P ∗ Q)
   
+"test_iDestruct_spatial"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  ============================
+  "HQ" : <affine> Q
+  --------------------------------------∗
+  Q
+  
+"test_iDestruct_spatial_affine"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  Affine0 : Affine Q
+  ============================
+  "HQ" : Q
+  --------------------------------------∗
+  Q
+  
 The command has indeed failed with message:
 Ltac call to "done" failed.
 No applicable tactic.

tests/proofmode.v

@@ -90,6 +90,21 @@ Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persisten
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
 
+Check "test_iDestruct_spatial".
+Lemma test_iDestruct_spatial Q : □ Q -∗ Q.
+Proof. iIntros "#HQ". iDestruct "HQ" as "-#HQ". Show. done. Qed.
+
+Check "test_iDestruct_spatial_affine".
+Lemma test_iDestruct_spatial_affine Q `{!Affine Q} : □ Q -∗ Q.
+Proof.
+  iIntros "#-#HQ".
+  (* Since [Q] is affine, it should not add an <affine> modality *)
+  Show. done.
+Qed.
+
+Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
+Proof. iIntros "-#HQ". done. Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.
 

theories/proofmode/coq_tactics.v

@@ -182,6 +182,22 @@ Proof.
         absorbingly_sep_l wand_elim_r HQ.
 Qed.
 
+Lemma tac_spatial Δ i p P P' Q :
+  envs_lookup i Δ = Some (p, P) →
+  (if p then FromAffinely P' P else TCEq P' P) →
+  match envs_replace i p false (Esnoc Enil i P') Δ with
+  | None => False
+  | Some Δ' => envs_entails Δ' Q
+  end →
+  envs_entails Δ Q.
+Proof.
+  intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
+  rewrite envs_entails_eq=> <-. rewrite envs_replace_singleton_sound //; simpl.
+  destruct p; simpl; last destruct HP.
+  - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
+  - by rewrite wand_elim_r.
+Qed.
+
 (** * Implication and wand *)
 Lemma tac_impl_intro Δ i P P' Q R :
   FromImpl R P Q →

theories/proofmode/intro_patterns.v

@@ -10,6 +10,7 @@ Inductive intro_pat :=
   | IList : list (list intro_pat) → intro_pat
   | IPure : intro_pat
   | IIntuitionistic : intro_pat → intro_pat
+  | ISpatial : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
   | IRewrite : direction → intro_pat
   | IPureIntro : intro_pat
@@ -29,6 +30,7 @@ Inductive stack_item :=
   | StBar : stack_item
   | StAmp : stack_item
   | StIntuitionistic : stack_item
+  | StSpatial : stack_item
   | StModalElim : stack_item.
 Notation stack := (list stack_item).
 
@@ -63,6 +65,7 @@ Fixpoint close_conj_list (k : stack)
      Some (StPat (big_conj ps) :: k)
   | StPat pat :: k => guard (cur = None); close_conj_list k (Some pat) ps
   | StIntuitionistic :: k => p ← cur; close_conj_list k (Some (IIntuitionistic p)) ps
+  | StSpatial :: k => p ← cur; close_conj_list k (Some (ISpatial p)) ps
   | StModalElim :: k => p ← cur; close_conj_list k (Some (IModalElim p)) ps
   | StAmp :: k => p ← cur; close_conj_list k None (p :: ps)
   | _ => None
@@ -83,6 +86,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TParenR :: ts => close_conj_list k None [] ≫= parse_go ts
   | TPure :: ts => parse_go ts (StPat IPure :: k)
   | TIntuitionistic :: ts => parse_go ts (StIntuitionistic :: k)
+  | TMinus :: TIntuitionistic :: ts => parse_go ts (StSpatial :: k)
   | TModal :: ts => parse_go ts (StModalElim :: k)
   | TArrow d :: ts => parse_go ts (StPat (IRewrite d) :: k)
   | TPureIntro :: ts => parse_go ts (StPat IPureIntro :: k)
@@ -113,6 +117,7 @@ Fixpoint close (k : stack) (ps : list intro_pat) : option (list intro_pat) :=
   | [] => Some ps
   | StPat pat :: k => close k (pat :: ps)
   | StIntuitionistic :: k => ''(p,ps) ← maybe2 (::) ps; close k (IIntuitionistic p :: ps)
+  | StSpatial :: k => ''(p,ps) ← maybe2 (::) ps; close k (ISpatial p :: ps)
   | StModalElim :: k => ''(p,ps) ← maybe2 (::) ps; close k (IModalElim p :: ps)
   | _ => None
   end.

theories/proofmode/ltac_tactics.v

@@ -301,6 +301,14 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
      fail "iIntuitionistic:" P "not affine and the goal not absorbing"
     |pm_reduce].
 
+Local Tactic Notation "iSpatial" constr(H) :=
+  eapply tac_spatial with H _ _ _;
+    [pm_reflexivity ||
+     let H := pretty_ident H in
+     fail "iSpatial:" H "not found"
+    |pm_reduce; iSolveTC
+    |pm_reduce].
+
 Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
   eapply tac_pure with H _ _ _; (* (i:=H1) *)
     [pm_reflexivity ||
@@ -1381,6 +1389,7 @@ Local Ltac iDestructHypGo Hz pat :=
   | IRewrite Right => iPure Hz as ->
   | IRewrite Left => iPure Hz as <-
   | IIntuitionistic ?pat => iIntuitionistic Hz; iDestructHypGo Hz pat
+  | ISpatial ?pat => iSpatial Hz; iDestructHypGo Hz pat
   | IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
   | _ => fail "iDestruct:" pat "invalid"
   end.