Commit 6bca8573 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode

parents ba5a4f8e 119fdac5
Pipeline #7032 passed with stage
in 10 minutes and 44 seconds
......@@ -170,8 +170,11 @@ Rewriting / simplification
Iris
----
- `iInv N as (x1 ... xn) "ipat" "Hclose"` : open the invariant `N`, the update
for closing the invariant is put in a hypothesis named `Hclose`.
- `iInv S with "selpat" as (x1 ... xn) "ipat" "Hclose"` : where `S` is either
a namespace N or an identifier "H". Open the invariant indicated by S. The
selection pattern `selpat` is used for any auxiliary assertions needed to
open the invariant (e.g. for cancelable or non-atomic invariants). The update
for closing the invariant is put in a hypothesis named `Hclose`.
Miscellaneous
-------------
......
......@@ -11,5 +11,5 @@ install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
depends: [
"coq" { >= "8.7.1" & < "8.8~" | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-21.0") | (= "dev") }
"coq-stdpp" { (= "dev.2018-02-23.0") | (= "dev") }
]
......@@ -90,6 +90,18 @@ Section proofs.
+ 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 p γ E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (cinv N γ P) (cinv_own γ p)
( P cinv_own γ p) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&Hown&H2)".
iApply (Helim with "[- $H2]"); first done.
iMod (cinv_open E N γ p P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
End proofs.
Typeclasses Opaque cinv_own cinv.
From iris.base_logic.lib Require Export fancy_updates.
From stdpp Require Export namespaces.
From stdpp Require Export namespaces.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type".
Import uPred.
......@@ -94,6 +94,17 @@ Proof.
iApply "HP'". iFrame.
Qed.
Global Instance into_inv_inv N P : IntoInv (inv N P) N.
Global Instance elim_inv_inv E N P Q Q' :
( R, ElimModal True (|={E,E∖↑N}=> R) R Q Q')
ElimInv (N E) (inv N P) True ( P) ( P ={E∖↑N,E}= True) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim ?) "(#H1&_&H2)".
iApply (Helim with "[$H2]"); first done.
iMod (inv_open _ N with "[#]") as "(HP&Hclose)"; auto with iFrame.
Qed.
Lemma inv_open_timeless E N P `{!Timeless P} :
N E inv N P ={E,E∖↑N}= P (P ={E∖↑N,E}= True).
Proof.
......@@ -101,29 +112,3 @@ Proof.
iIntros "!> {$HP} HP". iApply "Hclose"; auto.
Qed.
End inv.
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
let pat := constr:(IList [[IIdent Htmp; patback]]) in
iMod (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
|tac Htmp].
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1) pat) 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) 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) 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) Hclose.
......@@ -110,4 +110,16 @@ Section proofs.
+ iFrame. iApply "Hclose". iNext. iLeft. by iFrame.
- iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
Qed.
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':
( R, ElimModal True (|={E}=> R)%I R Q Q')
ElimInv (N E N F) (na_inv p N P) (na_own p F)
( P na_own p (F∖↑N)) ( P na_own p (F∖↑N) ={E}= na_own p F) Q Q'.
Proof.
rewrite /ElimInv /ElimModal. iIntros (Helim (?&?)) "(#H1&Hown&H2)".
iApply (Helim with "[- $H2]"); first done.
iMod (na_inv_open p E F N P with "[#] [Hown]") as "(HP&Hown&Hclose)"; auto.
by iFrame.
Qed.
End proofs.
......@@ -394,7 +394,7 @@ Canonical Structure monPredSI : sbi :=
End canonical_sbi.
Class Absolute {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
absolute_at V1 V2 : P V1 - P V2.
absolute_at i j : P i - P j.
Arguments Absolute {_ _} _%I.
Arguments absolute_at {_ _} _%I {_}.
Hint Mode Absolute + + ! : typeclass_instances.
......@@ -452,11 +452,11 @@ Proof. move => [] /(_ i). unfold Affine. by unseal. Qed.
(* Note that monPred_in is *not* Plain, because it does depend on the
index. *)
Global Instance monPred_in_persistent V :
Persistent (@monPred_in I PROP V).
Global Instance monPred_in_persistent i :
Persistent (@monPred_in I PROP i).
Proof. unfold Persistent. unseal; split => ?. by apply bi.pure_persistent. Qed.
Global Instance monPred_in_absorbing V :
Absorbing (@monPred_in I PROP V).
Global Instance monPred_in_absorbing i :
Absorbing (@monPred_in I PROP i).
Proof. unfold Absorbing. unseal. split=> ? /=. apply absorbing, _. Qed.
......@@ -657,35 +657,35 @@ Global Instance relatively_absolute P : Absolute (∃ᵢ P).
Proof. apply emb_absolute. Qed.
Global Instance and_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P Q).
Proof. intros ??. unseal. by rewrite !(absolute_at _ V1 V2). Qed.
Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
Global Instance or_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P Q).
Proof. intros ??. by rewrite !monPred_at_or !(absolute_at _ V1 V2). Qed.
Proof. intros i j. by rewrite !monPred_at_or !(absolute_at _ i j). Qed.
Global Instance impl_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P Q).
Proof.
intros ??. unseal. rewrite (bi.forall_elim V1) bi.pure_impl_forall.
rewrite bi.forall_elim //. apply bi.forall_intro=>V'.
intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
rewrite bi.forall_elim //. apply bi.forall_intro=> k.
rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
rewrite (absolute_at Q V1). by rewrite (absolute_at P V').
rewrite (absolute_at Q i). by rewrite (absolute_at P k).
Qed.
Global Instance forall_absolute {A} Φ {H : x : A, Absolute (Φ x)} :
@Absolute I PROP ( x, Φ x)%I.
Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Global Instance exists_absolute {A} Φ {H : x : A, Absolute (Φ x)} :
@Absolute I PROP ( x, Φ x)%I.
Proof. intros ??. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Proof. intros i j. unseal. do 2 f_equiv. by apply absolute_at. Qed.
Global Instance sep_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P Q).
Proof. intros ??. unseal. by rewrite !(absolute_at _ V1 V2). Qed.
Proof. intros i j. unseal. by rewrite !(absolute_at _ i j). Qed.
Global Instance wand_absolute P Q `{!Absolute P, !Absolute Q} : Absolute (P - Q).
Proof.
intros ??. unseal. rewrite (bi.forall_elim V1) bi.pure_impl_forall.
rewrite bi.forall_elim //. apply bi.forall_intro=>V'.
intros i j. unseal. rewrite (bi.forall_elim i) bi.pure_impl_forall.
rewrite bi.forall_elim //. apply bi.forall_intro=> k.
rewrite bi.pure_impl_forall. apply bi.forall_intro=>_.
rewrite (absolute_at Q V1). by rewrite (absolute_at P V').
rewrite (absolute_at Q i). by rewrite (absolute_at P k).
Qed.
Global Instance persistently_absolute P `{!Absolute P} :
Absolute (bi_persistently P).
Proof. intros ??. unseal. by rewrite absolute_at. Qed.
Proof. intros i j. unseal. by rewrite absolute_at. Qed.
Global Instance affinely_absolute P `{!Absolute P} : Absolute (bi_affinely P).
Proof. rewrite /bi_affinely. apply _. Qed.
......
From iris.bi Require Export bi.
From stdpp Require Import namespaces.
Set Default Proof Using "Type".
Import bi.
......@@ -478,6 +479,32 @@ Proof. by apply as_valid. Qed.
Lemma as_valid_2 (φ : Prop) {PROP : bi} (P : PROP) `{!AsValid φ P} : P φ.
Proof. by apply as_valid. Qed.
(* Input: [P]; Outputs: [N],
Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
Arguments IntoInv {_} _%I _.
Hint Mode IntoInv + ! - : typeclass_instances.
(* Input: [Pinv]
Arguments:
- [Pinv] is an invariant assertion
- [Pin] is an additional assertion needed for opening an invariant
- [Pout] is the assertion obtained by opening the invariant
- [Pclose] is the assertion which contains an update modality to close the invariant
- [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).
*)
Class ElimInv {PROP : bi} (φ : Prop) (Pinv Pin Pout Pclose Q Q' : PROP) :=
elim_inv : φ Pinv Pin (Pout Pclose - Q') Q.
Arguments ElimInv {_} _ _ _%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
definitions opaque for type class search. For example, when using `iDestruct`,
......@@ -523,3 +550,8 @@ Instance from_modal_tc_opaque {PROP : bi} (P Q : PROP) :
FromModal P Q FromModal (tc_opaque P) Q := id.
Instance elim_modal_tc_opaque {PROP : bi} φ (P P' Q Q' : PROP) :
ElimModal φ P P' Q Q' ElimModal φ (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 Pclose Q Q' : PROP) :
ElimInv φ Pinv Pin Pout Pclose Q Q'
ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
......@@ -209,6 +209,16 @@ Proof.
repeat apply sep_mono=>//; apply affinely_persistently_if_flag_mono; by destruct q1.
Qed.
Lemma envs_lookup_delete_list_cons Δ Δ' Δ'' rp j js p1 p2 P Ps :
envs_lookup_delete rp j Δ = Some (p1, P, Δ')
envs_lookup_delete_list rp js Δ' = Some (p2, Ps, Δ'')
envs_lookup_delete_list rp (j :: js) Δ = Some (p1 && p2, (P :: Ps), Δ'').
Proof. rewrite //= => -> //= -> //=. Qed.
Lemma envs_lookup_delete_list_nil Δ rp :
envs_lookup_delete_list rp [] Δ = Some (true, [], Δ).
Proof. done. Qed.
Lemma envs_lookup_snoc Δ i p P :
envs_lookup i Δ = None envs_lookup i (envs_snoc Δ p i P) = Some (p, P).
Proof.
......@@ -1159,6 +1169,22 @@ Proof.
rewrite envs_entails_eq => ???? HΔ. rewrite envs_replace_singleton_sound //=.
rewrite HΔ affinely_persistently_if_elim. by eapply elim_modal.
Qed.
(** * Invariants *)
Lemma tac_inv_elim Δ Δ' i j φ p P Pin Pout Pclose Q Q' :
envs_lookup_delete false i Δ = Some (p, P, Δ')
ElimInv φ P Pin Pout Pclose Q Q'
φ
( R, Δ'',
envs_app false (Esnoc Enil j (Pin - (Pout - 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 affinely_persistently_if_elim -assoc wand_curry. auto.
Qed.
End bi_tactics.
Section sbi_tactics.
......
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
From iris.bi Require Export bi big_op.
From stdpp Require Import namespaces.
From iris.proofmode Require Export classes notation.
From iris.proofmode Require Import class_instances.
From stdpp Require Import hlist pretty.
......@@ -1864,6 +1865,92 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
(** * Invariant *)
(* Finds a hypothesis in the context that is an invariant with
namespace [N]. To do so, we check whether for each hypothesis
["H":P] we can find an instance of [IntoInv P N] *)
Tactic Notation "iAssumptionInv" constr(N) :=
let rec find Γ i :=
lazymatch Γ with
| Esnoc ?Γ ?j ?P' =>
first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
end in
lazymatch goal with
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs) = Some _ =>
first [find Γp i|find Γs i]; env_reflexivity
end.
(* 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) constr(Hclose) :=
iStartProof;
let pats := spec_pat.parse pats in
lazymatch pats with
| [_] => idtac
| _ => fail "iInv: exactly one specialization pattern should be given"
end;
let H := iFresh in
lazymatch type of select with
| string =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| ident =>
eapply tac_inv_elim with _ select H _ _ _ _ _ _ _;
first by (iAssumptionCore || fail "iInv: invariant" select "not found")
| namespace =>
eapply tac_inv_elim with _ _ H _ _ _ _ _ _ _;
first by (iAssumptionInv select || fail "iInv: invariant" select "not found")
| _ => fail "iInv: selector" select "is not of the right type "
end;
[apply _ ||
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;
iIntros H; (* H was spatial, so it's gone due to the apply and we can reuse the name *)
iIntros Hclose;
tac H
)].
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
iInvCore N with "[$]" as ltac:(tac) Hclose.
Tactic Notation "iInv" constr(N) "as" constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as pat) Hclose.
Tactic Notation "iInv" constr(N) "as" "(" simple_intropattern(x1) ")"
constr(pat) constr(Hclose) :=
iInvCore N as (fun H => iDestructHyp H as (x1) pat) 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) 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) 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) Hclose.
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as pat) 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) 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) Hclose.
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3) pat) Hclose.
Tactic Notation "iInv" constr(N) "with" constr(Hs) "as" "(" simple_intropattern(x1)
simple_intropattern(x2) simple_intropattern(x3) simple_intropattern(x4) ")"
constr(pat) constr(Hclose) :=
iInvCore N with Hs as (fun H => iDestructHyp H as (x1 x2 x3 x4) pat) Hclose.
Hint Extern 0 (_ _) => iStartProof.
(* Make sure that by and done solve trivial things in proof mode *)
......
From iris.proofmode Require Import tactics.
From iris.base_logic Require Import base_logic lib.invariants.
From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
Section base_logic_tests.
Context {M : ucmraT}.
......@@ -48,7 +49,7 @@ Section base_logic_tests.
End base_logic_tests.
Section iris_tests.
Context `{invG Σ}.
Context `{invG Σ, cinvG Σ, na_invG Σ}.
Lemma test_masks N E P Q R :
N E
......@@ -58,4 +59,152 @@ Section iris_tests.
iApply ("H" with "[% //] [$] [> HQ] [> //]").
by iApply inv_alloc.
Qed.
Lemma test_iInv_0 N P: inv N (bi_persistently 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 (bi_persistently P) ={E}= P.
Proof.
iIntros (?) "#H".
iInv N as "#H2" "Hclose".
iMod ("Hclose" with "H2").
iModIntro. by iNext.
Qed.
Lemma test_iInv_2 γ p N P:
cinv N γ (bi_persistently 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 γ (bi_persistently P) cinv_own γ p1 cinv_own γ p2
={}= cinv_own γ p1 cinv_own γ p2 P.
Proof.
iIntros "(#?&Hown1&Hown2)".
iInv N with "[Hown2 //]" as "(#HP&Hown2)" "Hclose".
iMod ("Hclose" with "HP").
iModIntro. iFrame. by iNext.
Qed.
Lemma test_iInv_4 t N E1 E2 P:
N E2
na_inv t N (bi_persistently 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
na_inv t N (bi_persistently P) na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&Hown1&Hown2)".
iInv N with "Hown2" as "(#HP&Hown2)" "Hclose".
iMod ("Hclose" with "[HP Hown2]").
{ iFrame. done. }
iModIntro. iFrame. by iNext.
Qed.
Lemma test_iInv_6 t N E1 E2 P:
N E1
na_inv t N (bi_persistently P) na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&Hown1&Hown2)".
iInv N with "Hown1" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[HP Hown1]").
{ iFrame. done. }
iModIntro. iFrame. by iNext.
Qed.
(* test robustness in presence of other invariants *)
Lemma test_iInv_7 t N1 N2 N3 E1 E2 P:
N3 E1
inv N1 P na_inv t N3 (bi_persistently P) inv N2 P na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&#?&#?&Hown1&Hown2)".
iInv N3 with "Hown1" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[HP Hown1]").
{ iFrame. done. }
iModIntro. iFrame. by iNext.
Qed.
(* iInv should work even where we have "inv N P" in which P contains an evar *)
Lemma test_iInv_8 N : P, inv N P ={}= P True inv N P.
Proof.
eexists. iIntros "#H".
iInv N as "HP" "Hclose".
iMod ("Hclose" with "[$HP]"). auto.
Qed.
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_9 t N1 N2 N3 E1 E2 P:
N3 E1
inv N1 P na_inv t N3 (bi_persistently P) inv N2 P na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
iInv "HInv" with "Hown1" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[$HP $Hown1]").
iModIntro. iFrame. by iNext.
Qed.
(* test selection by hypothesis name instead of namespace *)
Lemma test_iInv_10 t N1 N2 N3 E1 E2 P:
N3 E1
inv N1 P na_inv t N3 (bi_persistently P) inv N2 P na_own t E1 na_own t E2
={}= na_own t E1 na_own t E2 P.
Proof.
iIntros (?) "(#?&#HInv&#?&Hown1&Hown2)".
iInv "HInv" as "(#HP&Hown1)" "Hclose".
iMod ("Hclose" with "[$HP $Hown1]").
iModIntro. iFrame. by iNext.
Qed.
(* test selection by ident name *)
Lemma test_iInv_11 N P: inv N (bi_persistently P) ={}= P.
Proof.
let H := iFresh in
(iIntros H; iInv H as "#H2" "Hclose").
iMod ("Hclose" with "H2").
iModIntro. by iNext.
Qed.
(* error messages *)
Lemma test_iInv_12 N P: inv N (bi_persistently P) ={}= True.
Proof.
iIntros "H".
Fail iInv 34 as "#H2" "Hclose".
Fail iInv nroot as "#H2" "Hclose".
Fail iInv "H2" as "#H2" "Hclose".
done.
Qed.
(* test destruction of existentials when opening an invariant *)
Lemma test_iInv_13 N:
inv N ( (v1 v2 v3 : nat), emp emp emp) ={}= emp.
Proof.
iIntros "H"; iInv "H" as (v1 v2 v3) "(?&?&_)" "Hclose".
iMod ("Hclose" with "[]").
{ iNext; iExists O; done. }
iModIntro. by iNext.
Qed.
End iris_tests.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment