...
 
Commits (2)
......@@ -6,6 +6,7 @@
Q : iProp Σ
l : loc
v : val
IPM_INTERNAL : IPM_STATE 3
============================
"Hl" : l ↦ v
--------------------------------------∗
......@@ -36,6 +37,7 @@
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
......@@ -68,6 +70,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
......@@ -99,6 +102,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
......@@ -131,6 +135,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
......@@ -196,6 +201,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 1
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
......
......@@ -6,6 +6,7 @@
Q : iProp Σ
l : loc
v : val
IPM_INTERNAL : IPM_STATE 3
============================
"Hl" : l ↦ v
--------------------------------------∗
......@@ -36,6 +37,7 @@
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, P x
ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
......@@ -68,6 +70,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << ∀ x : val, l ↦ x
ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >>
......@@ -99,6 +102,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅
......@@ -131,6 +135,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
_ : AACC << l ↦ #()
ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >>
......@@ -196,6 +201,7 @@
heapG0 : heapG Σ
l : loc
Φ : language.val heap_lang → iProp Σ
IPM_INTERNAL : IPM_STATE 1
============================
_ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
<< ∃ yyyy : val, l ↦ yyyy
......
......@@ -12,6 +12,7 @@
Σ : gFunctors
heapG0 : heapG Σ
E : coPset
IPM_INTERNAL : IPM_STATE 1
l : loc
============================
_ : l ↦ #1
......@@ -23,6 +24,7 @@
Σ : gFunctors
heapG0 : heapG Σ
E : coPset
IPM_INTERNAL : IPM_STATE 1
l : loc
============================
"Hl" : l ↦ #1
......@@ -37,6 +39,7 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
IPM_INTERNAL : IPM_STATE 1
============================
_ : ▷ l ↦ #0
--------------------------------------∗
......@@ -47,6 +50,7 @@
Σ : gFunctors
heapG0 : heapG Σ
l : loc
IPM_INTERNAL : IPM_STATE 1
============================
_ : l ↦ #1
--------------------------------------∗
......@@ -56,6 +60,7 @@
Σ : gFunctors
heapG0 : heapG Σ
IPM_INTERNAL : IPM_STATE 2
l : loc
============================
"Hl1" : l ↦{1 / 2} #0
......@@ -67,6 +72,7 @@
Σ : gFunctors
heapG0 : heapG Σ
IPM_INTERNAL : IPM_STATE 1
l : loc
============================
--------------------------------------∗
......
......@@ -6,6 +6,7 @@
A : Type
P, R : iProp
Ψ : A → iProp
IPM_INTERNAL : IPM_STATE 3
x : A
============================
"HP" : P
......@@ -20,6 +21,7 @@
A : Type
P, R : iProp
Ψ : A → iProp
IPM_INTERNAL : IPM_STATE 3
x : A
============================
"HΨ" : Ψ x
......@@ -39,6 +41,7 @@ P
A : Type
P, R : iProp
Ψ : A → iProp
IPM_INTERNAL : IPM_STATE 3
x : A
============================
"HP" : P
......@@ -54,6 +57,7 @@ P
A : Type
P, R : iProp
Ψ : A → iProp
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
"HΨ" : ∃ a : A, Ψ a
......@@ -72,6 +76,7 @@ P
n : nat
N : namespace
γ : gname
IPM_INTERNAL : IPM_STATE 2
============================
"Hinv" : inv N (I γ l)
--------------------------------------□
......@@ -88,6 +93,7 @@ P
n : nat
N : namespace
γ : gname
IPM_INTERNAL : IPM_STATE 5
c : nat
============================
"Hinv" : inv N (I γ l)
......
......@@ -5,6 +5,7 @@
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
IPM_INTERNAL : IPM_STATE 2
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
......@@ -16,6 +17,7 @@
Σ : gFunctors
heapG0 : heapG Σ
IPM_INTERNAL : IPM_STATE 2
acc : val
ys : list val
Φ : val → iPropI Σ
......
......@@ -5,6 +5,7 @@
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
IPM_INTERNAL : IPM_STATE 2
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
......@@ -16,6 +17,7 @@
Σ : gFunctors
heapG0 : heapG Σ
IPM_INTERNAL : IPM_STATE 2
acc : val
ys : list val
Φ : val → iPropI Σ
......
......@@ -4,6 +4,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : P
"H" : ∃ a : A, Φ a ∨ Ψ a
......@@ -16,6 +17,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
x : A
============================
"HP" : P
......@@ -29,6 +31,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
x : A
============================
"HP" : P
......@@ -42,6 +45,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : P
"H" : ∃ a : A, Φ a ∨ Ψ a
......@@ -54,6 +58,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
============================
"H" : ∃ a : A, Φ a ∨ Ψ a
--------------------------------------∗
......@@ -65,6 +70,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
x : A
============================
"HP" : <affine> P
......@@ -78,6 +84,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
x : A
============================
"HP" : <affine> P
......@@ -91,6 +98,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : P
--------------------------------------□
......@@ -104,6 +112,7 @@
A : Type
P : PROP
Φ, Ψ : A → PROP
IPM_INTERNAL : IPM_STATE 2
x : A
============================
"HP" : P
......@@ -117,6 +126,7 @@
PROP : bi
A : Type
P, Q : PROP
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : P
"HQ" : Q
......@@ -128,6 +138,7 @@
I : biIndex
PROP : bi
Φ, Ψ : monPred I PROP
IPM_INTERNAL : IPM_STATE 2
============================
"H1" : Φ
"H2" : Φ -∗ Ψ
......
......@@ -5,6 +5,7 @@
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
IPM_INTERNAL : IPM_STATE 10
l : loc
γ : gname
============================
......@@ -24,6 +25,7 @@
one_shotG0 : one_shotG Σ
Φ : val → iProp Σ
N : namespace
IPM_INTERNAL : IPM_STATE 13
l : loc
γ : gname
m, m' : Z
......
......@@ -15,6 +15,7 @@
PROP : sbi
P, Q : PROP
IPM_INTERNAL : IPM_STATE 2
============================
"H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
_ : P
......@@ -29,6 +30,7 @@
P, Q : PROP
Persistent0 : Persistent P
Persistent1 : Persistent Q
IPM_INTERNAL : IPM_STATE 2
============================
_ : P
_ : Q
......@@ -82,6 +84,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
φ : Prop
P, P2, Q, R1, R2 : PROP
H : φ
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
"HQ" : P -∗ Q
......@@ -161,6 +164,7 @@ Tactic failure: iFrame: cannot frame Q.
PROP : sbi
BiAffine0 : BiAffine PROP
P, Q : PROP
IPM_INTERNAL : IPM_STATE 2
============================
_ : □ P
_ : Q
......@@ -175,6 +179,7 @@ Tactic failure: iFrame: cannot frame Q.
x : nat
l : list nat
P : PROP
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
_ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
......@@ -188,6 +193,7 @@ Tactic failure: iFrame: cannot frame Q.
x : nat
l : list nat
P : PROP
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
_ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
......@@ -203,6 +209,7 @@ Tactic failure: iFrame: cannot frame Q.
x1, x2 : nat
l1, l2 : list nat
P : PROP
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
_ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
......@@ -216,6 +223,7 @@ Tactic failure: iFrame: cannot frame Q.
x1, x2 : nat
l1, l2 : list nat
P : PROP
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : P
_ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
......@@ -232,6 +240,7 @@ Tactic failure: iFrame: cannot frame Q.
Φ : nat → nat → PROP
x1, x2 : nat
l1, l2 : list nat
IPM_INTERNAL : IPM_STATE 2
============================
_ : Φ x1 x2
_ : [∗ list] y1;y2 ∈ l1;l2, Φ y1 y2
......@@ -243,6 +252,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
IPM_INTERNAL : IPM_STATE 2
============================
"H" : □ True
--------------------------------------∗
......@@ -253,6 +263,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
IPM_INTERNAL : IPM_STATE 2
============================
"H" : emp
--------------------------------------□
......@@ -263,6 +274,7 @@ Tactic failure: iFrame: cannot frame Q.
1 subgoal
PROP : sbi
IPM_INTERNAL : IPM_STATE 2
============================
"H" : emp
--------------------------------------□
......@@ -287,6 +299,7 @@ Tactic failure: iFrame: cannot frame Q.
PROP : sbi
mP : option PROP
Q, R : PROP
IPM_INTERNAL : IPM_STATE 3
============================
"HP" : default emp mP
--------------------------------------∗
......@@ -303,6 +316,7 @@ Tactic failure: iFrame: cannot frame Q.
α : X → PROP
β : X → PROP
γ : X → option PROP
IPM_INTERNAL : IPM_STATE 1
============================
"Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
--------------------------------------∗
......@@ -326,6 +340,7 @@ Tactic failure: iFrame: cannot frame Q.
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
IPM_INTERNAL : IPM_STATE 1
============================
_ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
......@@ -350,6 +365,7 @@ Tactic failure: iFrame: cannot frame Q.
PROP : sbi
BiFUpd0 : BiFUpd PROP
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P : PROP
IPM_INTERNAL : IPM_STATE 1
============================
_ : TESTNOTATION {{ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P |
P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P }}
......
......@@ -6,6 +6,7 @@
na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
"H" : inv N (<pers> P)
"H2" : ▷ <pers> P
......@@ -20,6 +21,7 @@
na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
IPM_INTERNAL : IPM_STATE 2
============================
"H" : inv N (<pers> P)
"H2" : ▷ <pers> P
......@@ -38,6 +40,7 @@
p : Qp
N : namespace
P : iProp Σ
IPM_INTERNAL : IPM_STATE 4
============================
_ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P
......@@ -56,6 +59,7 @@
p : Qp
N : namespace
P : iProp Σ
IPM_INTERNAL : IPM_STATE 4
============================
_ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P
......@@ -76,6 +80,7 @@
E1, E2 : coPset
P : iProp Σ
H : ↑N ⊆ E2
IPM_INTERNAL : IPM_STATE 5
============================
_ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P
......@@ -97,6 +102,7 @@
E1, E2 : coPset
P : iProp Σ
H : ↑N ⊆ E2
IPM_INTERNAL : IPM_STATE 5
============================
_ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P
......@@ -138,6 +144,7 @@ Tactic failure: iInv: invariant "H2" not found.
E : coPset
𝓟 : iProp Σ
H : ↑N ⊆ E
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : ⎡ ▷ 𝓟 ⎤
--------------------------------------∗
......@@ -154,6 +161,7 @@ Tactic failure: iInv: invariant "H2" not found.
E : coPset
𝓟 : iProp Σ
H : ↑N ⊆ E
IPM_INTERNAL : IPM_STATE 2
============================
"HP" : ⎡ ▷ 𝓟 ⎤
"Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
......
......@@ -42,6 +42,7 @@
FU0 : BiFUpd PROP * ()
P, Q : monpred.monPred I PROP
i : I
IPM_INTERNAL : IPM_STATE 1
============================
--------------------------------------∗
(Q -∗ emp) i
......@@ -53,6 +54,7 @@
FU0 : BiFUpd PROP * ()
P : monpred.monPred I PROP
i : I
IPM_INTERNAL : IPM_STATE 1
============================
--------------------------------------∗
∀ _ : (), ∃ _ : (), emp
......
......@@ -5,6 +5,7 @@
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
IPM_INTERNAL : IPM_STATE 3
x' : X
============================
"Hγ12" : ∀.. x : X, γ1 x -∗ γ2 x
......@@ -29,6 +30,7 @@
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
IPM_INTERNAL : IPM_STATE 1
x : X
============================
"Hγ1" : γ1 x
......@@ -42,6 +44,7 @@
X : tele
E1, E2 : coPset
α, β, γ1, γ2 : X → PROP
IPM_INTERNAL : IPM_STATE 1
x : X
============================
"Hγ1" : γ1 x
......@@ -53,6 +56,7 @@
PROP : sbi
BiFUpd0 : BiFUpd PROP
E1, E2 : coPset
IPM_INTERNAL : IPM_STATE 1
============================
"H" : ∃ x x0 : nat, <affine> ⌜x = x0⌝ ∗ (True ={E2,E1}=∗ <affine> ⌜x ≠ x0⌝)
--------------------------------------∗
......
......@@ -91,22 +91,44 @@ Tactic Notation "iStartProof" uconstr(PROP) :=
end.
(** * Generate a fresh identifier *)
Inductive IPM_STATE (n: positive) : Set := state_dummy.
Definition ipm_init : IPM_STATE 1 := state_dummy 1.
Lemma ipm_state_incr n : IPM_STATE n IPM_STATE (Pos.succ n).
Proof. intros; constructor. Qed.
(* Tactic Notation tactics cannot return terms *)
Ltac iFresh :=
(* We need to increment the environment counter using [tac_fresh].
(* We need to increment the environment counter using [ipm_state_incr].
But because [iFresh] returns a value, we have to let bind
[tac_fresh] wrapped under a match to force evaluation of this
[ipm_state_incr] wrapped under a match to force evaluation of this
side-effect. See https://stackoverflow.com/a/46178884 *)
let start_proof :=
lazymatch goal with
| _ => iStartProof
end in
let do_incr :=
lazymatch goal with
| _ => iStartProof; eapply tac_fresh; first by (pm_reflexivity)
| [ H : IPM_STATE _ |- _ ] =>
eapply ipm_state_incr in H; simpl in H
| [ |- envs_entails ?Δ _ ] =>
(* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
first use [cbv] to compute the domain of [Δ] *)
let Hs := eval cbv in (envs_dom Δ) in
let n' := eval vm_compute in
(match Hs with
| [] => 1
| _ => 1 + foldr Pos.max 1 (omap (maybe IAnon) Hs)
end)%positive in
let H := fresh "IPM_INTERNAL" in
pose proof (state_dummy n') as H
end in
lazymatch goal with
|- envs_entails ?Δ _ =>
let n := pm_eval (env_counter Δ) in
| [ H : IPM_STATE ?n |- _ ] =>
constr:(IAnon n)
end.
(** * Context manipulation *)
Tactic Notation "iRename" constr(H1) "into" constr(H2) :=
eapply tac_rename with _ H1 H2 _ _; (* (i:=H1) (j:=H2) *)
......