proofmode_iris.ref 4.02 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
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
114 115
"iInvCore (constr) in (tactic3)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
116 117 118 119
failed.
Tactic failure: iInv: selector 34 is not of the right type .
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
120 121
"iInvCore (constr) in (tactic3)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
122 123 124 125
failed.
Tactic failure: iInv: invariant nroot not found.
The command has indeed failed with message:
In nested Ltac calls to "iInv (constr) as (constr)",
126 127
"iInvCore (constr) in (tactic3)" and
"iInvCore (constr) with (constr) as (open_constr) in (tactic3)", last call
128 129
failed.
Tactic failure: iInv: invariant "H2" not found.
130 131
"test_iInv"
     : string
132 133 134
1 subgoal
  
  Σ : gFunctors
135
  invG0 : invG Σ
136 137 138 139
  I : biIndex
  N : namespace
  E : coPset
  𝓟 : iProp Σ
140
  H : ↑N ⊆ E
141 142 143 144 145
  ============================
  "HP" : ⎡ ▷ 𝓟 ⎤
  --------------------------------------∗
  |={E ∖ ↑N}=> ⎡ ▷ 𝓟 ⎤ ∗ (|={E}=> emp)
  
146 147
"test_iInv_with_close"
     : string
148 149 150
1 subgoal
  
  Σ : gFunctors
151
  invG0 : invG Σ
152 153 154 155
  I : biIndex
  N : namespace
  E : coPset
  𝓟 : iProp Σ
156
  H : ↑N ⊆ E
157 158 159 160 161 162
  ============================
  "HP" : ⎡ ▷ 𝓟 ⎤
  "Hclose" : ⎡ ▷ 𝓟 ={E ∖ ↑N,E}=∗ emp ⎤
  --------------------------------------∗
  |={E ∖ ↑N,E}=> emp