Commit 6415d82a authored by Ralf Jung's avatar Ralf Jung
Browse files

remove now stale .ref files

parent a092506c
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
============================
"H" : inv N (<pers> P)
"H2" : ▷ <pers> P
--------------------------------------□
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
N : namespace
P : iProp Σ
============================
"H" : inv N (<pers> P)
"H2" : ▷ <pers> P
--------------------------------------□
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ▷ P
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
γ : gname
p : Qp
N : namespace
P : iProp Σ
============================
_ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P
--------------------------------------□
"Hown" : cinv_own γ p
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
γ : gname
p : Qp
N : namespace
P : iProp Σ
============================
_ : cinv N γ (<pers> P)
"HP" : ▷ <pers> P
--------------------------------------□
"Hown" : cinv_own γ p
"Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : iProp Σ
H : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
--------------------------------------∗
|={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
1 goal
Σ : gFunctors
invG0 : invG Σ
cinvG0 : cinvG Σ
na_invG0 : na_invG Σ
t : na_inv_pool_name
N : namespace
E1, E2 : coPset
P : iProp Σ
H : ↑N ⊆ E2
============================
_ : na_inv t N (<pers> P)
"HP" : ▷ <pers> P
--------------------------------------□
"Hown1" : na_own t E1
"Hown2" : na_own t (E2 ∖ ↑N)
"Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
--------------------------------------∗
|={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
"test_iInv_12"
: string
The command has indeed failed with message:
Tactic failure: iInv: selector 34 is not of the right type .
The command has indeed failed with message:
Tactic failure: iInv: invariant nroot not found.
The command has indeed failed with message:
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
: string
1 goal
Σ : gFunctors
invG0 : invG Σ
I : biIndex
N : namespace
E : coPset
𝓟 : iProp Σ
H : ↑N ⊆ E
============================
"HP" : ⎡ ▷ 𝓟 ⎤
--------------------------------------∗
|={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
"test_iInv_with_close"
: string
1 goal
Σ : gFunctors
invG0 : invG Σ
I : biIndex
N : namespace
E : coPset
𝓟 : iProp Σ
H : ↑N ⊆ E
============================
"HP" : ⎡ ▷ 𝓟 ⎤
"Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
--------------------------------------∗
|={E ∖ ↑N,E}=> emp
"p1"
: string
1 goal
PROP : bi
============================
forall (P : PROP) (_ : True), bi_entails P P
"p2"
: string
1 goal
PROP : bi
============================
forall P : PROP, and True (bi_entails P P)
"p3"
: string
1 goal
PROP : bi
============================
ex (fun P : PROP => bi_entails P P)
"p4"
: string
1 goal
PROP : bi
============================
bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
"p5"
: string
1 goal
PROP : bi
============================
bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
"p6"
: string
1 goal
PROP : bi
============================
ex
(unique
(fun z : nat =>
bi_emp_valid
(bi_exist
(fun _ : nat =>
bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
"p7"
: string
1 goal
PROP : bi
============================
forall (a : nat) (_ : eq a O) (y : nat),
bi_entails (bi_pure True) (bi_pure (ge y O))
"p8"
: string
1 goal
PROP : bi
============================
forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
"p9"
: string
1 goal
PROP : bi
============================
forall (a : nat) (_ : eq a O) (_ : nat),
bi_emp_valid (bi_forall (fun z : nat => bi_pure (ge z O)))
1 goal
I : biIndex
PROP : bi
P, Q : monPred
i : I
============================
"HW" : (P -∗ Q) i
--------------------------------------∗
(P -∗ Q) i
1 goal
I : biIndex
PROP : bi
P, Q : monPred
i, j : I
============================
"HW" : (P -∗ Q) j
"HP" : P j
--------------------------------------∗
Q j
1 goal
I : biIndex
PROP : bi
P, Q : monPred
Objective0 : Objective Q
𝓟, 𝓠 : PROP
============================
"H2" : ∀ i : I, Q i
"H3" : 𝓟
"H4" : 𝓠
--------------------------------------∗
∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
1 goal
I : biIndex
PROP : bi
FU : BiFUpd PROP
P, Q : monPred
i : I
============================
--------------------------------------∗
(Q -∗ emp) i
1 goal
I : biIndex
PROP : bi
FU : BiFUpd PROP
P : monPred
i : I
============================
--------------------------------------∗
∀ _ : (), ∃ _ : (), emp
The command has indeed failed with message:
Tactic failure: iFrame: cannot frame (P i).
1 goal
I : biIndex
Σ : gFunctors
invG0 : invG Σ
N : namespace
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟 ⎤
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
1 goal
I : biIndex
Σ : gFunctors
invG0 : invG Σ
N : namespace
𝓟 : iProp Σ
============================
"H" : ⎡ inv N (<pers> 𝓟) ⎤
"H2" : ⎡ ▷ <pers> 𝓟 ⎤
--------------------------------------□
"Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
Supports Markdown
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