Commit 24656b41 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ci/ralf/telescopes' into 'gen_proofmode'

Telescope infrastructure

See merge request FP/iris-coq!161
parents 4c3f5b17 9690a7ee
......@@ -39,6 +39,7 @@ theories/bi/tactics.v
theories/bi/monpred.v
theories/bi/embedding.v
theories/bi/weakestpre.v
theories/bi/telescopes.v
theories/bi/lib/counter_examples.v
theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
......
"sep_exist"
: string
1 subgoal
M : ucmraT
......@@ -44,6 +46,8 @@ P
--------------------------------------∗
P
"sep_exist_short"
: string
1 subgoal
M : ucmraT
......@@ -57,6 +61,8 @@ P
--------------------------------------∗
∃ a : A, Ψ a ∗ P
"read_spec"
: string
1 subgoal
Σ : gFunctors
......
......@@ -25,6 +25,7 @@ Section demo.
Qed.
(* The version in IPM *)
Check "sep_exist".
Lemma sep_exist A (P R: iProp) (Ψ: A iProp) :
P ( a, Ψ a) R a, Ψ a P.
Proof.
......@@ -35,6 +36,7 @@ Section demo.
Qed.
(* The short version in IPM, as in the paper *)
Check "sep_exist_short".
Lemma sep_exist_short A (P R: iProp) (Ψ: A iProp) :
P ( a, Ψ a) R a, Ψ a P.
Proof. iIntros "[HP [HΨ HR]]". Show. iFrame "HP". iAssumption. Qed.
......@@ -235,6 +237,7 @@ Section counter_proof.
wp_if. iApply ("IH" with "[Hγf]"). rewrite {3}/C; eauto 10.
Qed.
Check "read_spec".
Lemma read_spec l n :
{{ C l n }} read #l {{ v, m : nat, v = #m n m C l m }}.
Proof.
......
......@@ -59,6 +59,31 @@ In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
1 subgoal
PROP : sbi
P, Q : PROP
n, m, k : nat
============================
--------------------------------------∗
▷^(S n + S m) emp
1 subgoal
PROP : sbi
P, Q : PROP
============================
--------------------------------------∗
▷ emp
1 subgoal
PROP : sbi
P, Q : PROP
============================
--------------------------------------∗
▷ emp
The command has indeed failed with message:
In nested Ltac calls to "iFrame (constr)",
"<iris.proofmode.ltac_tactics.iFrame_go>" and
......@@ -114,6 +139,52 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
<absorb> Φ x1 x2
1 subgoal
PROP : sbi
============================
"H" : □ True
--------------------------------------∗
True
1 subgoal
PROP : sbi
============================
"H" : emp
--------------------------------------□
□ emp
1 subgoal
PROP : sbi
============================
"H" : emp
--------------------------------------□
□ emp
1 subgoal
PROP : sbi
mP : option PROP
Q, R : PROP
============================
"HPQ" : mP -∗? Q
"HQR" : Q -∗ R
"HP" : pm_default emp mP
--------------------------------------∗
R
1 subgoal
PROP : sbi
mP : option PROP
Q, R : PROP
============================
"HP" : pm_default emp mP
--------------------------------------∗
pm_default emp mP
1 subgoal
PROP : sbi
......
......@@ -367,7 +367,7 @@ Lemma test_iNext_plus_2 P n m : ▷^n ▷^m P -∗ ▷^(n+m) P.
Proof. iIntros "H". iNext. done. Qed.
Lemma test_iNext_plus_3 P Q n m k :
^m ^(2 + S n + k) P - ^m ^(2 + S n) Q - ^k ^(S (S n + S m)) (P Q).
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Qed.
Proof. iIntros "H1 H2". iNext. iNext. iNext. iFrame. Show. iModIntro. done. Qed.
Lemma test_iNext_unfold P Q n m (R := (^n P)%I) :
R ^m True.
......@@ -409,10 +409,10 @@ Lemma test_iPureIntro_absorbing (φ : Prop) :
Proof. intros ?. iPureIntro. done. Qed.
Lemma test_iFrame_later_1 P Q : P Q - (P Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Lemma test_iFrame_later_2 P Q : P Q - ( P Q).
Proof. iIntros "H". iFrame "H". auto. Qed.
Proof. iIntros "H". iFrame "H". Show. auto. Qed.
Lemma test_with_ident P Q R : P - Q - (P - Q - R) - R.
Proof.
......@@ -490,7 +490,7 @@ Lemma test_big_sepL_simpl x (l : list nat) P :
([ list] ky l, <affine> y = y ) -
([ list] y x :: l, <affine> y = y ) -
P.
Proof. iIntros "HP ?? /=". Show. done. Qed.
Proof. iIntros "HP ??". Show. done. Qed.
Lemma test_big_sepL2_simpl x1 x2 (l1 l2 : list nat) P :
P -
......@@ -508,6 +508,42 @@ Lemma test_big_sepL2_iFrame (Φ : nat → nat → PROP) (l1 l2 : list nat) P :
Φ 0 10 - ([ list] y1;y2 l1;l2, Φ y1 y2) -
([ list] y1;y2 (0 :: l1);(10 :: l2), Φ y1 y2).
Proof. iIntros "$ ?". iFrame. Qed.
Lemma test_lemma_1 (b : bool) :
emp @{PROP} ?b True.
Proof. destruct b; simpl; eauto. Qed.
Lemma test_reducing_after_iDestruct : emp @{PROP} True.
Proof.
iIntros "H". iDestruct (test_lemma_1 true with "H") as "H". Show. done.
Qed.
Lemma test_lemma_2 (b : bool) :
?b emp @{PROP} emp.
Proof. destruct b; simpl; eauto. Qed.
Lemma test_reducing_after_iApply : emp @{PROP} emp.
Proof.
iIntros "#H". iApply (test_lemma_2 true). Show. auto.
Qed.
Lemma test_lemma_3 (b : bool) :
?b emp @{PROP} b = b.
Proof. destruct b; simpl; eauto. Qed.
Lemma test_reducing_after_iApply_late_evar : emp @{PROP} true = true.
Proof.
iIntros "#H". iApply (test_lemma_3). Show. auto.
Qed.
Section wandM.
Import proofmode.base.
Lemma test_wandM mP Q R :
(mP -? Q) - (Q - R) - (mP -? R).
Proof.
iIntros "HPQ HQR HP". Show.
iApply "HQR". iApply "HPQ". Show.
done.
Qed.
End wandM.
End tests.
(** Test specifically if certain things print correctly. *)
......
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
x' : X
============================
"Hγ12" : ∀.. x : X, γ1 x -∗ γ2 x
"Hα" : α x'
"Hclose" : β x' ={E2,E1}=∗ γ1 x'
--------------------------------------∗
|={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
1 subgoal
PROP : sbi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
--------------------------------------∗
|={E2,E1}=> False
"test1_test"
: string
1 subgoal
PROP : sbi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
▷ False
1 subgoal
PROP : sbi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
▷ False
"test2_test"
: string
1 subgoal
PROP : sbi
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
False
1 subgoal
PROP : sbi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
False
1 subgoal
PROP : sbi
x : nat
============================
"H" : ▷ (∃ x0 : nat, <affine> ⌜x = x0⌝)
--------------------------------------∗
▷ False
"test3_test"
: string
1 subgoal
PROP : sbi
x : nat
============================
"H" : ∃ x0 : nat, <affine> ⌜x = x0⌝
--------------------------------------∗
▷ False
1 subgoal
PROP : sbi
x : nat
============================
"H" : ◇ (∃ x0 : nat, <affine> ⌜x = x0⌝)
--------------------------------------∗
▷ False
From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Section accessor.
(* Just playing around a bit with a telescope version
of accessors with just one binder list. *)
Definition accessor `{!BiFUpd PROP} {X : tele} (E1 E2 : coPset)
(α β γ : X PROP) : PROP :=
(|={E1,E2}=> .. x, α x (β x - |={E2,E1}=> (γ x)))%I.
Notation "'ACC' @ E1 , E2 {{ ∃ x1 .. xn , α | β | γ } }" :=
(accessor (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
E1 E2
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => α%I) ..)
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => β%I) ..)
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => γ%I) ..))
(at level 20, α, β, γ at level 200, x1 binder, xn binder, only parsing).
(* Working with abstract telescopes. *)
Section tests.
Context `{!BiFUpd PROP} {X : tele}.
Implicit Types α β γ : X PROP.
Lemma acc_mono E1 E2 α β γ1 γ2 :
(.. x, γ1 x - γ2 x) -
accessor E1 E2 α β γ1 - accessor E1 E2 α β γ2.
Proof.
iIntros "Hγ12 >Hacc". iDestruct "Hacc" as (x') "[Hα Hclose]". Show.
iModIntro. iExists x'. iFrame. iIntros "Hβ".
iMod ("Hclose" with "Hβ") as "Hγ". iApply "Hγ12". auto.
Qed.
End tests.
Section printing_tests.
Context `{!BiFUpd PROP}.
(* Working with concrete telescopes: Testing the reduction into normal quantifiers. *)
Lemma acc_elim_test_1 E1 E2 :
ACC @ E1, E2 {{ a b : nat, <affine> a = b | True | <affine> a b }}
@{PROP} |={E1}=> False.
Proof.
iIntros ">H". Show.
iDestruct "H" as (a b) "[% Hclose]". iMod ("Hclose" with "[//]") as "%".
done.
Qed.
End printing_tests.
End accessor.
(* Robbert's tests *)
Section telescopes_and_tactics.
Definition test1 {PROP : sbi} {X : tele} (α : X PROP) : PROP :=
(.. x, α x)%I.
Notation "'TEST1' {{ ∃ x1 .. xn , α } }" :=
(test1 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => α%I) ..))
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
Definition test2 {PROP : sbi} {X : tele} (α : X PROP) : PROP :=
( .. x, α x)%I.
Notation "'TEST2' {{ ∃ x1 .. xn , α } }" :=
(test2 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => α%I) ..))
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
Definition test3 {PROP : sbi} {X : tele} (α : X PROP) : PROP :=
( .. x, α x)%I.
Notation "'TEST3' {{ ∃ x1 .. xn , α } }" :=
(test3 (X:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. ))
(tele_app (TT:=TeleS (fun x1 => .. (TeleS (fun xn => TeleO)) .. )) $
fun x1 => .. (fun xn => α%I) ..))
(at level 20, α at level 200, x1 binder, xn binder, only parsing).
Check "test1_test".
Lemma test1_test {PROP : sbi} :
TEST1 {{ a b : nat, <affine> a = b }} @{PROP} False.
Proof.
iIntros "H". iDestruct "H" as (x) "H". Show.
Restart.
iIntros "H". unfold test1. iDestruct "H" as (x) "H". Show.
Abort.
Check "test2_test".
Lemma test2_test {PROP : sbi} :
TEST2 {{ a b : nat, <affine> a = b }} @{PROP} False.
Proof.
iIntros "H". iModIntro. Show.
iDestruct "H" as (x) "H". Show.
Restart.
iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.
Check "test3_test".
Lemma test3_test {PROP : sbi} :
TEST3 {{ a b : nat, <affine> a = b }} @{PROP} False.
Proof.
iIntros "H". iMod "H".
iDestruct "H" as (x) "H".
Show.
Restart.
iIntros "H". iDestruct "H" as (x) "H". Show.
Abort.
End telescopes_and_tactics.
......@@ -206,7 +206,7 @@ Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i,
Proof. exact: uPred_primitive.ofe_fun_validI. Qed.
(** Consistency/soundness statement *)
Lemma soundness φ n : (^n φ : uPred M)%I φ.
Lemma soundness_iter φ n : Nat.iter n sbi_later ( φ : uPred M)%I φ.
Proof. exact: uPred_primitive.soundness. Qed.
End restate.
......
......@@ -91,8 +91,10 @@ Global Instance uPred_ownM_sep_homomorphism :
MonoidHomomorphism op uPred_sep () (@uPred_ownM M).
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
(** Consistency/soundness statement *)
Lemma soundness φ n : (^n φ : uPred M)%I φ.
Proof. rewrite laterN_iter. apply soundness_iter. Qed.
Corollary consistency_modal n : ¬ (^n False : uPred M)%I.
Proof. exact (soundness False n). Qed.
......
......@@ -88,8 +88,11 @@ Fixpoint bi_hforall {PROP : bi} {As} : himpl As PROP → PROP :=
| tcons A As => λ Φ, x, bi_hforall (Φ x)
end%I.
Definition sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
Nat.iter n sbi_later P.
Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
match n with
| O => P
| S n' => sbi_laterN n' P
end%I.
Arguments sbi_laterN {_} !_%nat_scope _%I.
Instance: Params (@sbi_laterN) 2.
Notation "▷^ n P" := (sbi_laterN n P) : bi_scope.
......@@ -106,3 +109,15 @@ Arguments Timeless {_} _%I : simpl never.
Arguments timeless {_} _%I {_}.
Hint Mode Timeless + ! : typeclass_instances.
Instance: Params (@Timeless) 1.
(** An optional precondition [mP] to [Q].
TODO: We may actually consider generalizing this to a list of preconditions,
and e.g. also using it for texan triples. *)
Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
match mP with
| None => Q
| Some P => (P - Q)%I
end.
Arguments bi_wandM {_} !_%I _%I /.
Notation "mP -∗? Q" := (bi_wandM mP Q)
(at level 99, Q at level 200, right associativity) : bi_scope.
......@@ -460,6 +460,10 @@ Proof.
- rewrite !and_elim_r wand_elim_r. done.
Qed.
Lemma wandM_sound (mP : option PROP) Q :
(mP -? Q) (default emp mP - Q).
Proof. destruct mP; simpl; first done. rewrite emp_wand //. Qed.
(* Pure stuff *)
Lemma pure_elim φ Q R : (Q ⌜φ⌝) (φ Q R) Q R.
Proof.
......
......@@ -247,6 +247,9 @@ Proof. induction n1; f_equiv/=; auto. Qed.
Lemma laterN_le n1 n2 P : n1 n2 ^n1 P ^n2 P.
Proof. induction 1; simpl; by rewrite -?later_intro. Qed.
Lemma laterN_iter n P : (^n P)%I = Nat.iter n sbi_later P.
Proof. induction n; f_equal/=; auto. Qed.
Lemma laterN_mono n P Q : (P Q) ^n P ^n Q.
Proof. induction n; simpl; auto. Qed.
Global Instance laterN_mono' n : Proper (() ==> ()) (@sbi_laterN PROP n).
......
......@@ -160,8 +160,8 @@ Section lemmas.
Global Instance elim_acc_aacc {X} E1 E2 Ei (α' β' : X PROP) γ' α β Pas Φ :
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1) α' β' γ'
(atomic_acc E1 Ei α Pas β Φ)
(λ x', atomic_acc E2 Ei α (β' x' pm_maybe_wand (γ' x') Pas)%I β
(λ x y, β' x' pm_maybe_wand (γ' x') (Φ x y)))%I.
(λ x', atomic_acc E2 Ei α (β' x' (γ' x' -? Pas))%I β
(λ x y, β' x' (γ' x' -? Φ x y)))%I.
Proof.
rewrite /ElimAcc.
(* FIXME: Is there any way to prevent maybe_wand from unfolding?
......
From stdpp Require Export telescopes.
From iris.bi Require Export bi.
Set Default Proof Using "Type*".
Import bi.
(* This cannot import the proofmode because it is imported by the proofmode! *)
(** Telescopic quantifiers *)
Definition bi_texist {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_exist PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_texist {_ !_} _ /.
Definition bi_tforall {PROP : bi} {TT : tele} (Ψ : TT PROP) : PROP :=
tele_fold (@bi_forall PROP) (λ x, x) (tele_bind Ψ).
Arguments bi_tforall {_ !_} _ /.
Notation "'∃..' x .. y , P" := (bi_texist (λ x, .. (bi_texist (λ y, P)) .. )%I)
(at level 200, x binder, y binder, right associativity,
format "∃.. x .. y , P") : bi_scope.
Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) .. )%I)
(at level 200, x binder, y binder, right associativity,
format "∀.. x .. y , P") : bi_scope.
Section telescope_quantifiers.
Context {PROP : bi} {TT : tele}.
Lemma bi_tforall_forall (Ψ : TT PROP) :
bi_tforall Ψ bi_forall Ψ.
Proof.
symmetry. unfold bi_tforall. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
+ by rewrite (forall_elim TargO).
+ rewrite -forall_intro; first done.
intros p. rewrite (tele_arg_O_inv p) /= //.
- simpl. apply (anti_symm _); apply forall_intro; intros a.
+ rewrite /= -IH. apply forall_intro; intros p.
by rewrite (forall_elim (TargS a p)).
+ move/tele_arg_inv : (a) => [x [pf ->]] {a} /=.
setoid_rewrite <- IH.
rewrite 2!forall_elim. done.
Qed.
Lemma bi_texist_exist (Ψ : TT PROP) :
bi_texist Ψ bi_exist Ψ.
Proof.
symmetry. unfold bi_texist. induction TT as [|X ft IH].
- simpl. apply (anti_symm _).
+ apply exist_elim; intros p.
rewrite (tele_arg_O_inv p) //.
+ by rewrite -(exist_intro TargO).
- simpl. apply (anti_symm _); apply exist_elim.
+ intros p. move/tele_arg_inv: (p) => [x [pf ->]] {p} /=.
by rewrite -exist_intro -IH -exist_intro.
+ intros x.
rewrite /= -IH. apply exist_elim; intros p.
by rewrite -(exist_intro (TargS x p)).
Qed.
Global Instance bi_tforall_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_tforall PROP TT).
Proof.
intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
Qed.
Global Instance bi_tforall_proper :
Proper (pointwise_relation _ () ==> ()) (@bi_tforall PROP TT).
Proof.
intros ?? EQ. rewrite !bi_tforall_forall. rewrite EQ //.
Qed.
Global Instance bi_texist_ne n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@bi_texist PROP TT).
Proof.
intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
Qed.
Global Instance bi_texist_proper :
Proper (pointwise_relation _ () ==> ()) (@bi_texist PROP TT).
Proof.
intros ?? EQ. rewrite !bi_texist_exist. rewrite EQ //.
Qed.
End telescope_quantifiers.
......@@ -27,8 +27,8 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
| _ => fail "wp_expr_eval: not a 'wp'"
end.
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
Ltac wp_expr_simpl := (wp_expr_eval simpl); pm_prettify.
Ltac wp_expr_simpl_subst := (wp_expr_eval simpl_subst); pm_prettify.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2
......
From iris.base_logic.lib Require Export fancy_updates.
From iris.program_logic Require Export language.
From iris.bi Require Export weakestpre.
From iris.proofmode Require Import tactics classes.
From iris.proofmode Require Import base tactics classes.
Set Default Proof Using "Type".
Import uPred.
......@@ -270,9 +270,9 @@ Section proofmode_classes.
Atomic (stuckness_to_atomicity s) e
ElimAcc (X:=X) (fupd E1 E2) (fupd E2 E1)
α β γ (WP e @ s; E1 {{ Φ }})
(λ x, WP e @ s; E2 {{ v, |={E2}=> β x coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
(λ x, WP e @ s; E2 {{ v, |={E2}=> β x (γ x -? Φ v) }})%I.
Proof.
intros ?. rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
intros ?. rewrite /ElimAcc.
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".
......@@ -281,9 +281,9 @@ Section proofmode_classes.
Global Instance elim_acc_wp_nonatomic {X} E α β γ e s Φ :
ElimAcc (X:=X) (fupd E E) (fupd E E)
α β γ (WP e @ s; E {{ Φ }})
(λ x, WP e @ s; E {{ v, |={E}=> β x coq_tactics.pm_maybe_wand (γ x) (Φ v) }})%I.
(λ x, WP e @ s; E {{ v, |={E}=> β x (γ x -? Φ v) }})%I.
Proof.
rewrite /ElimAcc. setoid_rewrite coq_tactics.pm_maybe_wand_sound.
rewrite /ElimAcc.
iIntros "Hinner >Hacc". iDestruct "Hacc" as (x) "[Hα Hclose]".
iApply wp_fupd.
iApply (wp_wand with "[Hinner Hα]"); first by iApply "Hinner".
......
From stdpp Require Import nat_cancel.
From iris.bi Require Import bi tactics.
From iris.bi Require Import bi tactics telescopes.
From iris.proofmode Require Import base modality_instances classes ltac_tactics.
Set Default Proof Using "Type".
Import bi.
......@@ -340,6 +340,16 @@ Global Instance from_modal_bupd `{BiBUpd PROP} P :
Proof. by rewrite /FromModal /= -bupd_intro. Qed.
(** IntoWand *)
Global Instance into_wand_wand' p q (P Q P' Q' : PROP) :
IntoWand' p q (P - Q) P' Q' IntoWand p q (P - Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_impl' p q (P Q P' Q' : PROP) :
IntoWand' p q (P Q) P' Q' IntoWand p q (P Q) P' Q' | 100.
Proof. done. Qed.
Global Instance into_wand_wandM' p q mP (Q P' Q' : PROP) :
IntoWand' p q (mP -? Q) P' Q' IntoWand p q (mP -? Q) P' Q' | 100.
Proof. done. Qed.