From 153fa59cafff3dd0a8acf34df1ca1aafb4234ddf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 18 Sep 2017 14:18:59 +0200
Subject: [PATCH] Allow to move non-affine stuff to the persistent/pure context
 if the goal is absorbing.

---
 theories/bi/derived.v            |  6 +++++
 theories/proofmode/coq_tactics.v | 44 +++++++++++++++++++++-----------
 theories/proofmode/tactics.v     | 16 ++++++------
 3 files changed, 43 insertions(+), 23 deletions(-)

diff --git a/theories/bi/derived.v b/theories/bi/derived.v
index 653323888..f350f0599 100644
--- a/theories/bi/derived.v
+++ b/theories/bi/derived.v
@@ -1345,6 +1345,12 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 Lemma persistent_entails_r P Q `{!Persistent Q} : (P ⊢ Q) → P ⊢ P ∗ Q.
 Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
 
+Lemma persistent_sink_bare P `{!Persistent P} : P ⊢ ▲ ■ P.
+Proof.
+  by rewrite {1}(persistent_persistently_2 P) -persistently_bare
+             persistently_elim_sink.
+Qed.
+
 Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
   P ∧ (Q ∗ R) ⊣⊢ (P ∧ Q) ∗ R.
 Proof. by rewrite -(persistent_persistently P) persistently_and_sep_assoc. Qed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index a555a196b..2c65ec850 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -506,14 +506,17 @@ Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
   IntoPure P φ →
-  (if p then TCTrue else Affine P) →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
   (φ → Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ??? HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
+  intros ?? HPQ HQ. rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl.
   - rewrite (into_pure P) -persistently_and_bare_sep_l persistently_pure.
     by apply pure_elim_l.
-  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
-    by apply pure_elim_l.
+  - destruct HPQ.
+    + rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
+      by apply pure_elim_l.
+    + rewrite (into_pure P) (persistent_sink_bare ⌜ _ ⌝%I) sink_sep_lr.
+      rewrite -persistent_and_bare_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
 Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
@@ -535,14 +538,18 @@ Qed.
 Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
-  (if p then TCTrue else Affine P) →
+  (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
-  intros ???? <-. rewrite envs_replace_singleton_sound //; simpl.
-  apply wand_elim_r', wand_mono=> //. destruct p; simpl.
-  - by rewrite -(into_persistent _ P).
-  - by rewrite -(into_persistent _ P) /= affine_bare.
+  intros ?? HPQ ? HQ. rewrite envs_replace_singleton_sound //; simpl.
+  destruct p; simpl.
+  - by rewrite -(into_persistent _ P) /= wand_elim_r.
+  - destruct HPQ.
+    + rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
+      by rewrite wand_elim_r.
+    + rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
+      by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
 Qed.
 
 (** * Implication and wand *)
@@ -591,20 +598,27 @@ Proof.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
-  Affine P →
+  TCOr (Affine P) (Absorbing Q) →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
-  intros ??? <-. rewrite envs_app_singleton_sound //; simpl.
-  apply wand_mono=>//. by rewrite -(into_persistent _ P) /= affine_bare.
+  intros ? HPQ ? HQ. rewrite envs_app_singleton_sound //; simpl.
+  apply wand_intro_l. destruct HPQ.
+  - rewrite -(affine_bare P) (_ : P = â–¡?false P)%I // (into_persistent _ P).
+    by rewrite wand_elim_r.
+  - rewrite (_ : P = â–¡?false P)%I // (into_persistent _ P).
+    by rewrite {1}(persistent_sink_bare (â–¡ _)%I) sink_sep_l wand_elim_r HQ.
 Qed.
 Lemma tac_wand_intro_pure Δ P φ Q :
   IntoPure P φ →
-  Affine P →
+  TCOr (Affine P) (Absorbing Q) →
   (φ → Δ ⊢ Q) → Δ ⊢ P -∗ Q.
 Proof.
-  intros. apply wand_intro_l. rewrite -(affine_bare P) (into_pure P).
-  rewrite -persistent_and_bare_sep_l. by apply pure_elim_l.
+  intros ? HPQ HQ. apply wand_intro_l. destruct HPQ.
+  - rewrite -(affine_bare P) (into_pure P) -persistent_and_bare_sep_l.
+    by apply pure_elim_l.
+  - rewrite (into_pure P) (persistent_sink_bare ⌜ _ ⌝%I) sink_sep_lr.
+    rewrite -persistent_and_bare_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 Lemma tac_wand_intro_drop Δ P Q :
   TCOr (Affine P) (Absorbing Q) →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index c6c174b99..ad1b54ad7 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -184,8 +184,8 @@ Local Tactic Notation "iPersistent" constr(H) :=
      let P := match goal with |- IntoPersistent _ ?P _ => P end in
      fail "iPersistent:" P "not persistent"
     |env_cbv; apply _ ||
-     let P := match goal with |- Affine ?P => P end in
-     fail "iPersistent:" P "not affine"
+     let P := match goal with |- TCOr (Affine ?P) _ => P end in
+     fail "iPersistent:" P "not affine and the goal not absorbing"
     |env_reflexivity|].
 
 Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
@@ -195,8 +195,8 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
      let P := match goal with |- IntoPure ?P _ => P end in
      fail "iPure:" P "not pure"
     |env_cbv; apply _ ||
-     let P := match goal with |- Affine ?P => P end in
-     fail "iPure:" P "not affine"
+     let P := match goal with |- TCOr (Affine ?P) _ => P end in
+     fail "iPure:" P "not affine and the goal not absorbing"
     |intros pat].
 
 Tactic Notation "iEmpIntro" :=
@@ -338,7 +338,7 @@ Local Tactic Notation "iIntro" constr(H) :=
     eapply tac_wand_intro with _ H; (* (i:=H) *)
       [env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
-  | fail 1 "iIntro: nothing to introduce" ].
+  | fail "iIntro: nothing to introduce" ].
 
 Local Tactic Notation "iIntro" "#" constr(H) :=
   iStartProof;
@@ -356,11 +356,11 @@ Local Tactic Notation "iIntro" "#" constr(H) :=
        let P := match goal with |- IntoPersistent _ ?P _ => P end in
        fail 1 "iIntro:" P "not persistent"
       |apply _ ||
-       let P := match goal with |- Affine ?P => P end in
-       fail 1 "iIntro:" P "not affine"
+       let P := match goal with |- TCOr (Affine ?P) _ => P end in
+       fail 1 "iIntro:" P "not affine and the goal not absorbing"
       |env_reflexivity || fail 1 "iIntro:" H "not fresh"
       |]
-  | fail 1 "iIntro: nothing to introduce" ].
+  | fail "iIntro: nothing to introduce" ].
 
 Local Tactic Notation "iIntro" "_" :=
   try iStartProof;
-- 
GitLab