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

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.