From 3627c45fd81275ae6c97f87cdceb58074c606cc3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Apr 2018 23:05:53 +0200
Subject: [PATCH] New IntoAcc typeclass to decouple creating and elliminating
accessors; ElimInv supports both with and without Hclose
---
theories/base_logic/lib/auth.v | 3 +-
.../base_logic/lib/cancelable_invariants.v | 15 +--
theories/base_logic/lib/invariants.v | 11 ++-
theories/base_logic/lib/na_invariants.v | 16 +--
theories/base_logic/lib/sts.v | 3 +-
theories/base_logic/lib/viewshifts.v | 3 +-
theories/bi/derived_laws_bi.v | 14 +++
theories/heap_lang/lib/increment.v | 5 +-
theories/program_logic/weakestpre.v | 25 ++---
theories/proofmode/class_instances_sbi.v | 47 +++++++--
theories/proofmode/classes.v | 94 ++++++++++++------
theories/proofmode/coq_tactics.v | 33 ++++---
theories/proofmode/ltac_tactics.v | 99 ++++++++++++++-----
theories/proofmode/monpred.v | 18 ++--
theories/tests/proofmode_iris.v | 29 ++++++
15 files changed, 292 insertions(+), 123 deletions(-)
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index f0a8c87e0..bd849ac1f 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -144,8 +144,7 @@ Section auth.
⌜a ≼ f t⌠∗ ▷ φ t ∗ ∀ u b,
⌜(f t, a) ~l~> (f u, b)⌠∗ ▷ φ u ={E∖↑N,E}=∗ auth_own γ b.
Proof using Type*.
- iIntros (?) "[Hinv Hγf]". rewrite /auth_ctx.
- iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
+ iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index f3fff6412..f960d5ebe 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -83,21 +83,22 @@ Section proofs.
cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
Proof.
iIntros (?) "#Hinv Hγ". iDestruct "Hinv" as (P') "[#HP' Hinv]".
- iMod (inv_open with "Hinv") as "[[HP | >Hγ'] Hclose]"; first done.
+ iInv N as "[HP | >Hγ']" "Hclose".
- iIntros "!> {$Hγ}". iSplitL "HP".
- + iApply "HP'". done.
+ + iNext. iApply "HP'". done.
+ iIntros "HP". iApply "Hclose". iLeft. iNext. by iApply "HP'".
- iDestruct (cinv_own_1_l with "Hγ' Hγ") as %[].
Qed.
Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
- Global Instance elim_inv_cinv E N γ P p Q Q' :
- AccElim E (E∖↑N) (▷ P ∗ cinv_own γ p) (▷ P) None Q Q' →
- ElimInv (↑N ⊆ E) (cinv N γ P) (cinv_own γ p) (▷ P ∗ cinv_own γ p) Q Q'.
+ Global Instance elim_inv_cinv E N γ P p :
+ IntoAcc (X:=unit) (cinv N γ P)
+ (↑N ⊆ E) (cinv_own γ p) E (E∖↑N)
+ (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
Proof.
- rewrite /ElimInv /AccElim. iIntros (Helim ?) "(#Hinv & Hown & Hcont)".
- iApply (Helim with "Hcont"). clear Helim. rewrite -assoc.
+ rewrite /IntoAcc /accessor. iIntros (?) "#Hinv Hown".
+ rewrite exist_unit -assoc.
iApply (cinv_open with "Hinv"); done.
Qed.
End proofs.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 785558bfc..3aae8621c 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -109,12 +109,12 @@ Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
-Global Instance elim_inv_inv E N P Q Q' :
- AccElim E (E∖↑N) (▷ P) (▷ P) None Q Q' →
- ElimInv (↑N ⊆ E) (inv N P) True (▷ P) Q Q'.
+Global Instance elim_inv_inv E N P :
+ IntoAcc (X:=unit) (inv N P)
+ (↑N ⊆ E) True E (E∖↑N) (λ _, ▷ P)%I (λ _, ▷ P)%I (λ _, None)%I.
Proof.
- rewrite /ElimInv /AccElim. iIntros (Hopener ?) "(#Hinv & _ & Hcont)".
- iApply (Hopener with "Hcont"). iApply inv_open; done.
+ rewrite /IntoAcc /accessor exist_unit.
+ iIntros (?) "#Hinv _". iApply inv_open; done.
Qed.
Lemma inv_open_timeless E N P `{!Timeless P} :
@@ -123,4 +123,5 @@ Proof.
iIntros (?) "Hinv". iMod (inv_open with "Hinv") as "[>HP Hclose]"; auto.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed.
+
End inv.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 810fe5cb3..9b3fe13ca 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -101,7 +101,7 @@ Section proofs.
rewrite [F as X in na_own p X](union_difference_L (↑N) F) //.
rewrite [X in (X ∪ _)](union_difference_L {[i]} (↑N)) ?na_own_union; [|set_solver..].
iDestruct "Htoks" as "[[Htoki $] $]".
- iMod (inv_open with "Hinv") as "[[[$ >Hdis]|>Htoki2] Hclose]"; first done.
+ iInv "Hinv" as "[[$ >Hdis]|>Htoki2]" "Hclose".
- iMod ("Hclose" with "[Htoki]") as "_"; first auto.
iIntros "!> [HP $]".
iInv N as "[[_ >Hdis2]|>Hitok]".
@@ -113,14 +113,14 @@ Section proofs.
Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
- Global Instance elim_inv_na p F E N P Q Q':
- AccElim E E (▷ P ∗ na_own p (F ∖ ↑ N)) (▷ P ∗ na_own p (F ∖ ↑ N))
- (Some (na_own p F)) Q Q' →
- ElimInv (↑N ⊆ E ∧ ↑N ⊆ F) (na_inv p N P) (na_own p F)
- (▷ P ∗ na_own p (F∖↑N)) Q Q'.
+ Global Instance elim_inv_na p F E N P :
+ IntoAcc (X:=unit) (na_inv p N P)
+ (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) E E
+ (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
+ (λ _, Some (na_own p F))%I.
Proof.
- rewrite /ElimInv /AccElim. iIntros (Helim (?&?)) "(#Hinv & Hown & Hcont)".
- iApply (Helim with "Hcont"). clear Helim. rewrite -assoc /=.
+ rewrite /IntoAcc /accessor. iIntros ((?&?)) "#Hinv Hown".
+ rewrite exist_unit -assoc /=.
iApply (na_inv_open with "Hinv"); done.
Qed.
End proofs.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index ecf58f3aa..0d8e8ced6 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -156,8 +156,7 @@ Section sts.
⌜s ∈ S⌠∗ ▷ φ s ∗ ∀ s' T',
⌜sts.steps (s, T) (s', T')⌠∗ ▷ φ s' ={E∖↑N,E}=∗ sts_own γ s' T'.
Proof.
- iIntros (?) "[Hinv Hγf]". rewrite /sts_ctx.
- iMod (inv_open with "Hinv") as "[Hinv Hclose]"; first done.
+ iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[sts_acc] and [inv_open] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 6f418757b..e45a87c0c 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -72,8 +72,7 @@ Qed.
Lemma vs_inv N E P Q R :
↑N ⊆ E → inv N R ∗ (▷ R ∗ P ={E∖↑N}=> ▷ R ∗ Q) ⊢ P ={E}=> Q.
Proof.
- iIntros (?) "#[Hinv Hvs] !# HP".
- iMod (inv_open with "Hinv") as "[HR Hclose]"; first done.
+ iIntros (?) "#[? Hvs] !# HP". iInv N as "HR" "Hclose".
iMod ("Hvs" with "[HR HP]") as "[? $]"; first by iFrame.
by iApply "Hclose".
Qed.
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index 0143774a7..183386e3e 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -219,6 +219,20 @@ Proof.
- apply impl_intro_r, impl_elim_r', exist_elim=>x.
apply impl_intro_r. by rewrite (forall_elim x) impl_elim_r.
Qed.
+Lemma forall_unit (Ψ : unit → PROP) :
+ (∀ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+ apply (anti_symm (⊢)).
+ - rewrite (forall_elim ()) //.
+ - apply forall_intro=>[[]]. done.
+Qed.
+Lemma exist_unit (Ψ : unit → PROP) :
+ (∃ x, Ψ x) ⊣⊢ Ψ ().
+Proof.
+ apply (anti_symm (⊢)).
+ - apply exist_elim=>[[]]. done.
+ - rewrite -(exist_intro ()). done.
+Qed.
Lemma or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
Proof.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index f4d2d8803..331ba1db0 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -68,7 +68,7 @@ Section increment_client.
WP incr_client #x {{ _, True }}%I.
Proof using Type*.
wp_let. wp_alloc l as "Hl". wp_let.
- iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#Hinv"; first eauto.
+ iMod (inv_alloc nroot _ (∃x':Z, l ↦ #x')%I with "[Hl]") as "#?"; first eauto.
(* FIXME: I am only usign persistent stuff, so I should be allowed
to move this to the persisten context even without the additional â–¡. *)
iAssert (□ atomic_update (λ (v: Z), l ↦ #v)
@@ -78,8 +78,7 @@ Section increment_client.
{ iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
iIntros "!#" (E) "% _".
assert (E = ⊤) as -> by set_solver.
- iMod (inv_open with "Hinv") as "[>H↦ Hclose]"; first done.
- iDestruct "H↦" as (x) "H↦".
+ iInv nroot as (x) ">H↦" "Hclose".
iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
iExists _. iFrame. iSplit.
{ iIntros "H↦". iMod "Hclose2" as "_". iMod ("Hclose" with "[-]"); last done.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index c847355b1..22026e94a 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -405,25 +405,26 @@ Section proofmode_classes.
AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
- Global Instance acc_elim_wp E1 E2 P P' (P'' : option _) e s Φ :
+ Global Instance acc_elim_wp {X} E1 E2 α β γ e s Φ :
Atomic (stuckness_to_atomicity s) e →
- AccElim E1 E2 P P' P'' (WP e @ s; E1 {{ Φ }})
- (WP e @ s; E2 {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+ AccElim (X:=X) E1 E2 α β γ (WP e @ s; E1 {{ Φ }})
+ (λ x, WP e @ s; E2 {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Proof.
intros ?. rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
- iIntros "Hinner >[HP Hclose]".
- iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
- iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
+ iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+ iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+ iIntros (v) "[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
- Global Instance acc_elim_wp_nonatomic E P P' (P'' : option _) e s Φ :
- AccElim E E P P' P'' (WP e @ s; E {{ Φ }})
- (WP e @ s; E {{ v, P' ∗ coq_tactics.maybe_wand P'' (Φ v) }})%I.
+ Global Instance acc_elim_wp_nonatomic {X} E α β γ e s Φ :
+ AccElim (X:=X) E E α β γ (WP e @ s; E {{ Φ }})
+ (λ x, WP e @ s; E {{ v, β x ∗ coq_tactics.maybe_wand (γ x) (Φ v) }})%I.
Proof.
rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
- iIntros "Hinner >[HP Hclose]". iApply wp_fupd.
- iApply (wp_wand with "[Hinner HP]"); first by iApply "Hinner".
- iIntros (v) "[HP HΦ]". iApply "HΦ". by iApply "Hclose".
+ iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+ iApply wp_fupd.
+ iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
+ iIntros (v) "[Hβ HΦ]". iApply "HΦ". by iApply "Hclose".
Qed.
End proofmode_classes.
diff --git a/theories/proofmode/class_instances_sbi.v b/theories/proofmode/class_instances_sbi.v
index 79b177e77..1a31b4a64 100644
--- a/theories/proofmode/class_instances_sbi.v
+++ b/theories/proofmode/class_instances_sbi.v
@@ -552,15 +552,46 @@ Global Instance add_modal_embed_fupd_goal `{BiEmbedFUpd PROP PROP'}
Proof. by rewrite /AddModal !embed_fupd. Qed.
(* AccElim *)
-Global Instance acc_elim_vs `{BiFUpd PROP} E1 E2 E P P' (P'' : option PROP) Q :
+Global Instance acc_elim_vs `{BiFUpd PROP} {X} E1 E2 E α β γ Q :
(* FIXME: Why %I? AccElim sets the right scopes! *)
- AccElim E1 E2 P P' P''
- (|={E1,E}=> Q) (|={E2}=> (P' ∗ (coq_tactics.maybe_wand P'' (|={E1,E}=> Q))))%I.
-Proof.
- rewrite /AccElim coq_tactics.maybe_wand_sound.
- iIntros "Hinner >[HP Hclose]".
- iMod ("Hinner" with "HP") as "[HP Hfin]".
- iMod ("Hclose" with "HP") as "HP''". by iApply "Hfin".
+ AccElim (X:=X) E1 E2 α β γ
+ (|={E1,E}=> Q)
+ (λ x, |={E2}=> (β x ∗ (coq_tactics.maybe_wand (γ x) (|={E1,E}=> Q))))%I.
+Proof.
+ rewrite /AccElim. setoid_rewrite coq_tactics.maybe_wand_sound.
+ iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
+ iMod ("Hinner" with "Hα") as "[Hβ Hfin]".
+ iMod ("Hclose" with "Hβ") as "Hγ". by iApply "Hfin".
+Qed.
+
+(* IntoAcc *)
+(* TODO: We could have instances from "unfolded" accessors with or without
+ the first binder. *)
+
+(* ElimInv *)
+Global Instance elim_inv_acc_without_close `{BiFUpd PROP} φ Pinv Pin
+ E1 E2 α β γ Q (Q' : () → PROP) :
+ IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ →
+ AccElim (X:=unit) E1 E2 α β γ Q Q' →
+ ElimInv φ Pinv Pin (α ()) None Q (Q' ()).
+Proof.
+ rewrite /AccElim /IntoAcc /ElimInv.
+ iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+ iApply (Helim with "[Hcont]").
+ - rewrite right_id. iIntros ([]). done.
+ - iApply (Hacc with "Hinv Hin"). done.
+Qed.
+
+Global Instance elim_inv_acc_with_close `{BiFUpd PROP} φ Pinv Pin
+ E1 E2 α β γ Q Q' :
+ IntoAcc (X:=unit) Pinv φ Pin E1 E2 α β γ →
+ (∀ R, ElimModal True false false (|={E1,E2}=> R) R Q Q') →
+ ElimInv φ Pinv Pin (α ()) (Some (β () ={E2,E1}=∗ default emp (γ ()) id))%I Q Q'.
+Proof.
+ rewrite /AccElim /IntoAcc /ElimInv.
+ iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
+ iMod (Hacc with "Hinv Hin") as ([]) "[Hα Hclose]"; first done.
+ iApply "Hcont". simpl. iSplitL "Hα"; done.
Qed.
(* IntoLater *)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 2ab4f51e9..6a811bf6c 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -513,40 +513,74 @@ Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.
-(** Typeclass for assertions around which accessors can be elliminated.
- Inputs: [Q], [P], [P'], [P'']
- Outputs: [Q']
- In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
-
- Elliminates an accessor [|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ P'')] in goal [Q'],
- turning the goal into [Q'] with a new assumption [P]. If [P''] is None,
- that signifies [emp] and will be used to make the goal shown to the user
- nicer (i.e., no unnecessary hypothesis is added). [φ] is a Coq-level
- side-condition that will be attempted to be discharged by solve_ndisj. *)
-Class AccElim `{BiFUpd PROP} E1 E2 (P P' : PROP) (P'' : option PROP) (Q Q' : PROP) :=
- acc_elim : ((P -∗ Q') -∗ (|={E1,E2}=> P ∗ (P' ={E2,E1}=∗ default emp P'' id)) -∗ Q).
-Arguments AccElim {_} {_} _ _ _%I _%I _%I _%I : simpl never.
-Arguments acc_elim {_} {_} _ _ _%I _%I _%I _%I {_}.
-Hint Mode AccElim + + - - ! ! ! ! - : typeclass_instances.
-
-(* Input: [Pinv]
+(** Accessors.
+ This definition only exists for the purpose of the proof mode; a truly
+ usable and general form would use telescopes and also allow binders for the
+ closing view shift. [γ] is an [option] to make it easy for AccElim
+ instances to recognize the [emp] case and make it look nicer. *)
+Definition accessor `{BiFUpd PROP} {X : Type} (E1 E2 : coPset)
+ (α β : X → PROP) (γ : X → option PROP) : PROP :=
+ (|={E1,E2}=> ∃ x, α x ∗ (β x ={E2,E1}=∗ default emp (γ x) id))%I.
+
+(* Typeclass for assertions around which accessors can be elliminated.
+ Inputs: [Q], [α], [β], [γ]
+ Outputs: [Q']
+ In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+
+ Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
+ into [Q'] with a new assumption [α x]. *)
+Class AccElim `{BiFUpd PROP} {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP)
+ (Q : PROP) (Q' : X → PROP) :=
+ acc_elim : ((∀ x, α x -∗ Q' x) -∗ accessor E1 E2 α β γ -∗ Q).
+Arguments AccElim {_} {_} {_} _ _ _%I _%I _%I _%I : simpl never.
+Arguments acc_elim {_} {_} {_} _ _ _%I _%I _%I _%I {_}.
+Hint Mode AccElim + + ! - - ! ! ! ! - : typeclass_instances.
+
+(* Turn [P] into an accessor.
+ Inputs:
+ - [Pacc]: the assertion to be turned into an accessor (e.g. an invariant)
+ Outputs:
+ - [Pin]: additional logic assertion needed for starting the accessor.
+ - [φ]: additional Coq assertion needed for starting the accessor.
+ - [X] [α], [β], [γ]: the accessor parameters.
+ In/Out (can be an evar and will not usually be instantiated): [E1], [E2]
+*)
+Class IntoAcc `{BiFUpd PROP} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+ {X : Type} E1 E2 (α β : X → PROP) (γ : X → option PROP) :=
+ into_acc : φ → Pacc -∗ Pin -∗ accessor E1 E2 α β γ.
+Arguments IntoAcc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I : simpl never.
+Arguments into_acc {_} {_} _%I _ _%I {_} _ _ _%I _%I _%I {_} : simpl never.
+Hint Mode IntoAcc + - ! - - - - - - - - : typeclass_instances.
+
+(* The typeclass used for the [iInv] tactic.
+ Input: [Pinv]
Arguments:
- [Pinv] is an invariant assertion
- - [Pin] is an additional assertion needed for opening an invariant
+ - [Pin] is an additional logic assertion needed for opening an invariant
+ - [φ] is an additional Coq assertion needed for opening an invariant
- [Pout] is the assertion obtained by opening the invariant
+ - [Pclose] is the closing view shift. It must be (Some _) or None
+ when doing typeclass search as instances are allowed to make a
+ case distinction on whether the user wants a closing view-shift or not.
- [Q] is a goal on which iInv may be invoked
- [Q'] is the transformed goal that must be proved after opening the invariant.
- There are similarities to the definition of ElimModal, however we
- want to be general enough to support uses in settings where there
- is not a clearly associated instance of ElimModal of the right form
- (e.g. to handle Iris 2.0 usage of iInv).
+ Most users will never want to instantiate this; there is a general instance
+ based on [AccElim] and [IntoAcc]. However, logics like Iris 2 that support
+ invariants but not mask-changing fancy updates can use this class directly to
+ still benefit from [iInv].
+
+ TODO: Add support for a binder (like accessors have it).
+
+ This is defined on sbi instead of bi as typeclass search otherwise
+ fails (e.g. in the iInv as used in cancelable_invariants.v)
*)
-Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Q Q' : PROP) :=
- elim_inv : φ → Pinv ∗ Pin ∗ (Pout -∗ Q') ⊢ Q.
-Arguments ElimInv {_} _ _%I _%I _%I _%I _%I : simpl never.
-Arguments elim_inv {_} _ _ _%I _%I _%I _%I _%I.
-Hint Mode ElimInv + - ! - - ! - : typeclass_instances.
+Class ElimInv {PROP : sbi} (φ : Prop)
+ (Pinv Pin : PROP) (Pout : PROP) (Pclose : option PROP) (Q Q' : PROP) :=
+ elim_inv : φ → Pinv ∗ Pin ∗ (Pout ∗ default emp Pclose id -∗ Q') ⊢ Q.
+Arguments ElimInv {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
+Arguments elim_inv {_} _ _%I _%I _%I _%I _%I _%I {_}.
+Hint Mode ElimInv + - ! - - ! ! - : typeclass_instances.
(* We make sure that tactics that perform actions on *specific* hypotheses or
parts of the goal look through the [tc_opaque] connective, which is used to make
@@ -594,6 +628,6 @@ Instance elim_modal_tc_opaque {PROP : bi} φ p p' (P P' Q Q' : PROP) :
ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
Instance into_inv_tc_opaque {PROP : bi} (P : PROP) N :
IntoInv P N → IntoInv (tc_opaque P) N := id.
-Instance elim_inv_tc_opaque {PROP : bi} φ (Pinv Pin Pout Q Q' : PROP) :
- ElimInv φ Pinv Pin Pout Q Q' →
- ElimInv φ (tc_opaque Pinv) Pin Pout Q Q' := id.
+Instance elim_inv_tc_opaque {PROP : sbi} φ Pinv Pin Pout Pclose Q Q' :
+ ElimInv (PROP:=PROP) φ Pinv Pin Pout Pclose Q Q' →
+ ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index f5c42b628..d2d3c526d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -746,6 +746,7 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_singleton_sound Δ2) //; simpl.
rewrite HP1 into_wand /= -(add_modal P1' P1 Q). cancel [P1'].
+
apply wand_intro_l. by rewrite assoc !wand_elim_r.
Qed.
@@ -1075,22 +1076,6 @@ Proof.
rewrite HΔ. by eapply elim_modal.
Qed.
-(** * Invariants *)
-Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Q Q' :
- envs_lookup_delete false i Δ = Some (p, P, Δ') →
- ElimInv φ P Pin Pout Q Q' →
- φ →
- (∀ R, ∃ Δ'',
- envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ Q') -∗ R)%I) Δ' = Some Δ'' ∧
- envs_entails Δ'' R) →
- envs_entails Δ Q.
-Proof.
- rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
- rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
- apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
- rewrite intuitionistically_if_elim -assoc. auto.
-Qed.
-
(** * Accumulate hypotheses *)
Lemma tac_accu Δ P :
prop_of_env (env_spatial Δ) = P →
@@ -1339,6 +1324,22 @@ Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.
+(** * Invariants *)
+Lemma tac_inv_elim Δ Δ' i j φ p Pinv Pin Pout (Pclose : option PROP) Q Q' :
+ envs_lookup_delete false i Δ = Some (p, Pinv, Δ') →
+ ElimInv φ Pinv Pin Pout Pclose Q Q' →
+ φ →
+ (∀ R, ∃ Δ'',
+ envs_app false (Esnoc Enil j (Pin -∗ (Pout -∗ maybe_wand Pclose Q') -∗ R)%I) Δ' = Some Δ'' ∧
+ envs_entails Δ'' R) →
+ envs_entails Δ Q.
+Proof.
+ rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] ?? /(_ Q) [Δ'' [? <-]].
+ rewrite (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
+ apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
+ rewrite intuitionistically_if_elim maybe_wand_sound -assoc wand_curry. auto.
+Qed.
+
(** * Rewriting *)
Lemma tac_rewrite Δ i p Pxy d Q :
envs_lookup i Δ = Some (p, Pxy) →
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 2f2230a2a..476dee490 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
Export ident.
Declare Reduction env_cbv := cbv [
- option_bind
+ option_bind from_option (* TODO: Can we make these (and maybe_wand) reduce only if applied to a constructor? *)
beq ascii_beq string_beq positive_beq Pos.succ ident_beq
env_lookup env_lookup_delete env_delete env_app env_replace env_dom
env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
@@ -1887,7 +1887,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
(* The argument [select] is the namespace [N] or hypothesis name ["H"] of the
invariant. *)
-Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) :=
+Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) open_constr(Hclose) :=
iStartProof;
let pats := spec_pat.parse pats in
lazymatch pats with
@@ -1895,48 +1895,67 @@ Tactic Notation "iInvCore" constr(select) "with" constr(pats) "as" tactic(tac) :
| _ => fail "iInv: exactly one specialization pattern should be given"
end;
let H := iFresh in
+ let Pclose_pat :=
+ match Hclose with
+ | Some _ => open_constr:(Some _)
+ | None => open_constr:(None)
+ end in
lazymatch type of select with
| string =>
- eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+ eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| ident =>
- eapply tac_inv_elim with _ select H _ _ _ _ _ _;
+ eapply @tac_inv_elim with (i:=select) (j:=H) (Pclose:=Pclose_pat);
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| namespace =>
- eapply tac_inv_elim with _ _ H _ _ _ _ _ _;
+ eapply @tac_inv_elim with (j:=H) (Pclose:=Pclose_pat);
first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
| _ => fail "iInv: selector" select "is not of the right type "
end;
[iSolveTC ||
- let I := match goal with |- ElimInv _ ?I _ _ _ _ => I end in
+ let I := match goal with |- ElimInv _ ?I _ _ _ _ _ => I end in
fail "iInv: cannot eliminate invariant " I
|try (split_and?; solve [ fast_done | solve_ndisj ])
|let R := fresh in intros R; eexists; split; [env_reflexivity|];
iSpecializePat H pats; last (
iApplyHyp H; clear R; env_cbv;
iIntro H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
+ match Hclose with
+ | Some ?Hcl => iIntros Hcl
+ | None => idtac
+ end;
tac H
)].
+(* Without closing view shift *)
+Tactic Notation "iInvCore" constr(N) "with" constr(pats) "as" tactic(tac) :=
+ iInvCore N with pats as ltac:(tac) (@None string).
+(* Without pattern *)
+Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
+ iInvCore N with "[$]" as ltac:(tac) Hclose.
+(* Without both *)
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) :=
- iInvCore N with "[$]" as ltac:(tac).
+ iInvCore N with "[$]" as ltac:(tac) (@None string).
-Tactic Notation "iInv" constr(N) "as" constr(pat) :=
- iInvCore N as (fun H => iDestructHyp H as pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
- constr(pat) :=
- iInvCore N as (fun H => iDestructHyp H as (x1) pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
- simple_intropattern(x2) ")" constr(pat) :=
- iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+(* With everything *)
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
+ iInvCore N with Hs as (fun H => iDestructHyp H as pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
+ constr(pat) constr(Hclose) :=
+ iInvCore N with Hs as (fun H => iDestructHyp H as (x1) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+ iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
- constr(pat) :=
- iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat).
-Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ constr(pat) constr(Hclose) :=
+ iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
- constr(pat) :=
- iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
+ constr(pat) constr(Hclose) :=
+ iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) (Some Hclose).
+
+(* Without closing view shift *)
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as pat).
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1) ")"
@@ -1954,7 +1973,43 @@ Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(
constr(pat) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
-(* Miscellaneous *)
+(* Without pattern *)
+Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
+ iInvCore N as (fun H => iDestructHyp H as pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+ constr(pat) constr(Hclose) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) constr(Hclose) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")"
+ constr(pat) constr(Hclose) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat) (Some Hclose).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+ constr(pat) constr(Hclose) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) (Some Hclose).
+
+(* Without both *)
+Tactic Notation "iInv" constr(N) "as" constr(pat) :=
+ iInvCore N as (fun H => iDestructHyp H as pat).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
+ constr(pat) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1) pat).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) ")" constr(pat) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2) pat).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) ")"
+ constr(pat) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3) pat).
+Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1)
+ simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
+ constr(pat) :=
+ iInvCore N as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat).
+
+(** Miscellaneous *)
Tactic Notation "iAccu" :=
iStartProof; eapply tac_accu; [env_reflexivity || fail "iAccu: not an evar"].
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 31cbbb4bf..6820522f6 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -486,12 +486,18 @@ Global Instance add_modal_at_fupd_goal `{BiFUpd PROP} E1 E2 ð“Ÿ ð“Ÿ' Q i :
AddModal ð“Ÿ ð“Ÿ' (|={E1,E2}=> Q i) → AddModal ð“Ÿ ð“Ÿ' ((|={E1,E2}=> Q) i).
Proof. by rewrite /AddModal !monPred_at_fupd. Qed.
-Global Instance elim_inv_embed φ ð“Ÿinv ð“Ÿin ð“Ÿout Pin Pout Q Q' :
- (∀ i, ElimInv φ ð“Ÿinv ð“Ÿin ð“Ÿout (Q i) (Q' i)) →
+Global Instance elim_inv_embed φ ð“Ÿinv ð“Ÿin ð“Ÿout ð“Ÿclose Pin Pout Pclose Q Q' :
+ (∀ i, ElimInv φ ð“Ÿinv ð“Ÿin ð“Ÿout ð“Ÿclose (Q i) (Q' i)) →
MakeEmbed ð“Ÿin Pin → MakeEmbed ð“Ÿout Pout →
- ElimInv φ ⎡ð“Ÿinv⎤ Pin Pout Q Q'.
-Proof.
- rewrite /MakeEmbed /ElimInv=>H <- <- ?. iStartProof PROP.
- iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
+ match ð“Ÿclose, Pclose with
+ | Some ð“Ÿclose, Some Pclose => MakeEmbed ð“Ÿclose Pclose
+ | None, None => True
+ | _, _ => False
+ end →
+ ElimInv φ ⎡ð“Ÿinv⎤ Pin Pout Pclose Q Q'.
+Proof.
+ rewrite /MakeEmbed /ElimInv=>H <- <- Hclose ?. iStartProof PROP.
+ iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?".
+ destruct ð“Ÿclose; destruct Pclose; try rewrite -Hclose; iApply "HQ'"; done.
Qed.
End sbi.
diff --git a/theories/tests/proofmode_iris.v b/theories/tests/proofmode_iris.v
index dd793e037..df20ac3d1 100644
--- a/theories/tests/proofmode_iris.v
+++ b/theories/tests/proofmode_iris.v
@@ -67,6 +67,14 @@ Section iris_tests.
iModIntro. iSplit; auto.
Qed.
+ Lemma test_iInv_0_with_close N P: inv N (<pers> P) ={⊤}=∗ ▷ P.
+ Proof.
+ iIntros "#H".
+ iInv N as "#H2" "Hclose".
+ iMod ("Hclose" with "H2").
+ iModIntro. by iNext.
+ Qed.
+
Lemma test_iInv_1 N E P:
↑N ⊆ E →
inv N (<pers> P) ={E}=∗ ▷ P.
@@ -84,6 +92,15 @@ Section iris_tests.
iModIntro. iSplit; auto with iFrame.
Qed.
+ Lemma test_iInv_2_with_close γ p N P:
+ cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P.
+ Proof.
+ iIntros "(#?&?)".
+ iInv N as "(#HP&Hown)" "Hclose".
+ iMod ("Hclose" with "HP").
+ iModIntro. iFrame. by iNext.
+ Qed.
+
Lemma test_iInv_3 γ p1 p2 N P:
cinv N γ (<pers> P) ∗ cinv_own γ p1 ∗ cinv_own γ p2
={⊤}=∗ cinv_own γ p1 ∗ cinv_own γ p2 ∗ ▷ P.
@@ -103,6 +120,18 @@ Section iris_tests.
iModIntro. iSplitL "Hown2"; auto with iFrame.
Qed.
+ Lemma test_iInv_4_with_close t N E1 E2 P:
+ ↑N ⊆ E2 →
+ na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
+ ⊢ |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P.
+ Proof.
+ iIntros (?) "(#?&Hown1&Hown2)".
+ iInv N as "(#HP&Hown2)" "Hclose".
+ iMod ("Hclose" with "[HP Hown2]").
+ { iFrame. done. }
+ iModIntro. iFrame. by iNext.
+ Qed.
+
(* test named selection of which na_own to use *)
Lemma test_iInv_5 t N E1 E2 P:
↑N ⊆ E2 →
--
GitLab