proofmode_iris.ref 3.51 KB
Newer Older
1 2 3
1 subgoal
  
  Σ : gFunctors
4 5 6
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
7
  N : namespace
8
  P : iProp Σ
9
  ============================
10
  "H" : inv N (<pers> P)
11 12 13 14 15 16 17
  "H2" : ▷ <pers> P
  --------------------------------------□
  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
  
1 subgoal
  
  Σ : gFunctors
18 19 20
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
21
  N : namespace
22
  P : iProp Σ
23
  ============================
24
  "H" : inv N (<pers> P)
25 26 27 28 29 30 31 32 33
  "H2" : ▷ <pers> P
  --------------------------------------□
  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
  --------------------------------------∗
  |={⊤ ∖ ↑N,⊤}=> ▷ P
  
1 subgoal
  
  Σ : gFunctors
34 35 36
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
37 38 39
  γ : gname
  p : Qp
  N : namespace
40
  P : iProp Σ
41
  ============================
42
  _ : cinv N γ (<pers> P)
43 44 45 46 47 48 49 50 51
  "HP" : ▷ <pers> P
  --------------------------------------□
  "Hown" : cinv_own γ p
  --------------------------------------∗
  |={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
  
1 subgoal
  
  Σ : gFunctors
52 53 54
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
55 56 57
  γ : gname
  p : Qp
  N : namespace
58
  P : iProp Σ
59
  ============================
60
  _ : cinv N γ (<pers> P)
61 62 63 64 65 66 67 68 69 70
  "HP" : ▷ <pers> P
  --------------------------------------□
  "Hown" : cinv_own γ p
  "Hclose" : ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp
  --------------------------------------∗
  |={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
  
1 subgoal
  
  Σ : gFunctors
71 72 73
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
74 75 76
  t : na_inv_pool_name
  N : namespace
  E1, E2 : coPset
77
  P : iProp Σ
78
  H : ↑N ⊆ E2
79
  ============================
80
  _ : na_inv t N (<pers> P)
81 82 83 84 85 86 87 88 89 90 91
  "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 subgoal
  
  Σ : gFunctors
92 93 94
  invG0 : invG Σ
  cinvG0 : cinvG Σ
  na_invG0 : na_invG Σ
95 96 97
  t : na_inv_pool_name
  N : namespace
  E1, E2 : coPset
98
  P : iProp Σ
99
  H : ↑N ⊆ E2
100
  ============================
101
  _ : na_inv t N (<pers> P)
102 103 104 105
  "HP" : ▷ <pers> P
  --------------------------------------□
  "Hown1" : na_own t E1
  "Hown2" : na_own t (E2 ∖ ↑N)
106
  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ na_own t E2
107 108 109
  --------------------------------------∗
  |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
  
110 111
"test_iInv_12"
     : string
112 113 114 115 116 117
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.
118 119
"test_iInv"
     : string
120 121 122
1 subgoal
  
  Σ : gFunctors
123
  invG0 : invG Σ
124 125 126 127
  I : biIndex
  N : namespace
  E : coPset
  𝓟 : iProp Σ
128
  H : ↑N ⊆ E
129 130 131 132 133
  ============================
  "HP" : ⎡ ▷ 𝓟 ⎤
  --------------------------------------∗
  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
  
134 135
"test_iInv_with_close"
     : string
136 137 138
1 subgoal
  
  Σ : gFunctors
139
  invG0 : invG Σ
140 141 142 143
  I : biIndex
  N : namespace
  E : coPset
  𝓟 : iProp Σ
144
  H : ↑N ⊆ E
145 146 147 148 149 150
  ============================
  "HP" : ⎡ ▷ 𝓟 ⎤
  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
  --------------------------------------∗
  |={E ∖ ↑N,E}=> emp