proofmode.ref 20.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
"demo_0"
     : string
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
  --------------------------------------□
  "H" : □ (P ∨ Q)
  --------------------------------------∗
  Q ∨ P
  
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
  _ : P
  --------------------------------------□
  Q ∨ P
  
Ralf Jung's avatar
Ralf Jung committed
24
25
"test_iDestruct_and_emp"
     : string
26
27
28
1 subgoal
  
  PROP : sbi
29
30
31
32
33
34
35
36
37
  P, Q : PROP
  Persistent0 : Persistent P
  Persistent1 : Persistent Q
  ============================
  _ : P
  _ : Q
  --------------------------------------□
  <affine> (P ∗ Q)
  
38
39
40
41
42
The command has indeed failed with message:
Ltac call to "done" failed.
No applicable tactic.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
Ralf Jung's avatar
Ralf Jung committed
43
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
44
Tactic failure: iElaborateSelPat: "HQ" not found.
45
46
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
Ralf Jung's avatar
Ralf Jung committed
47
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
48
Tactic failure: iElaborateSelPat: "HQ" not found.
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
Ralf Jung's avatar
Ralf Jung committed
66
67
"test_iNext_plus_3"
     : string
68
69
70
71
72
73
74
75
76
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  n, m, k : nat
  ============================
  --------------------------------------∗
  ▷^(S n + S m) emp
  
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
"test_specialize_nested_intuitionistic"
     : string
1 subgoal
  
  PROP : sbi
  φ : Prop
  P, P2, Q, R1, R2 : PROP
  H : φ
  ============================
  "HP" : P
  "HQ" : P -∗ Q
  --------------------------------------□
  "HR" : R2
  --------------------------------------∗
  R2
  
Robbert Krebbers's avatar
Robbert Krebbers committed
93
94
95
96
97
98
99
100
101
102
103
"test_iSimpl_in"
     : string
1 subgoal
  
  PROP : sbi
  x, y : nat
  ============================
  "H" : ⌜S (S (S x)) = y⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
104
105
106
107
108
109
110
111
112
113
1 subgoal
  
  PROP : sbi
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  "H2" : ⌜S y = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
114
115
116
117
118
119
120
121
122
123
124
1 subgoal
  
  PROP : sbi
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  --------------------------------------□
  "H2" : ⌜(1 + y)%nat = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
Dan Frumin's avatar
Dan Frumin committed
125
126
127
128
129
130
131
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
Ralf Jung's avatar
Ralf Jung committed
132
133
"test_iFrame_later_1"
     : string
134
135
136
137
138
139
140
141
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
Ralf Jung's avatar
Ralf Jung committed
142
143
"test_iFrame_later_2"
     : string
144
145
146
147
148
149
150
151
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
152
153
154
155
156
The command has indeed failed with message:
In nested Ltac calls to "iFrame (constr)",
"<iris.proofmode.ltac_tactics.iFrame_go>" and
"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
Tactic failure: iFrame: cannot frame Q.
Ralf Jung's avatar
Ralf Jung committed
157
158
"test_and_sep_affine_bi"
     : string
159
160
161
1 subgoal
  
  PROP : sbi
162
  BiAffine0 : BiAffine PROP
163
164
165
166
167
168
169
  P, Q : PROP
  ============================
  _ : □ P
  _ : Q
  --------------------------------------∗
  □ P
  
Ralf Jung's avatar
Ralf Jung committed
170
171
"test_big_sepL_simpl"
     : string
172
173
174
175
176
177
178
179
180
181
182
183
184
1 subgoal
  
  PROP : sbi
  x : nat
  l : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
  _ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
  --------------------------------------∗
  P
  
185
186
187
188
189
190
191
192
193
194
195
196
197
1 subgoal
  
  PROP : sbi
  x : nat
  l : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
  _ : <affine> ⌜x = x⌝ ∗ ([∗ list] y ∈ l, <affine> ⌜y = y⌝)
  --------------------------------------∗
  P
  
Ralf Jung's avatar
Ralf Jung committed
198
199
"test_big_sepL2_simpl"
     : string
200
201
202
203
204
205
206
207
208
209
210
211
212
1 subgoal
  
  PROP : sbi
  x1, x2 : nat
  l1, l2 : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
  _ : [∗ list] y1;y2 ∈ (x1 :: l1);((x2 :: l2) ++ l2), <affine> ⌜y1 = y2⌝
  --------------------------------------∗
  P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
  
Robbert Krebbers's avatar
Robbert Krebbers committed
213
214
215
216
217
218
219
220
221
222
223
224
225
226
1 subgoal
  
  PROP : sbi
  x1, x2 : nat
  l1, l2 : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
  _ : <affine> ⌜x1 = x2⌝
      ∗ ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
  --------------------------------------∗
  P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
  
Ralf Jung's avatar
Ralf Jung committed
227
228
"test_big_sepL2_iDestruct"
     : string
Robbert Krebbers's avatar
Robbert Krebbers committed
229
230
231
232
233
234
235
236
237
238
239
240
1 subgoal
  
  PROP : sbi
  Φ : nat → nat → PROP
  x1, x2 : nat
  l1, l2 : list nat
  ============================
  _ : Φ x1 x2
  _ : [∗ list] y1;y2 ∈ l1;l2, Φ y1 y2
  --------------------------------------∗
  <absorb> Φ x1 x2
  
Ralf Jung's avatar
Ralf Jung committed
241
242
"test_reducing_after_iDestruct"
     : string
243
244
245
246
247
248
249
250
1 subgoal
  
  PROP : sbi
  ============================
  "H" : □ True
  --------------------------------------∗
  True
  
Ralf Jung's avatar
Ralf Jung committed
251
252
"test_reducing_after_iApply"
     : string
253
254
255
256
257
258
259
260
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
261
262
"test_reducing_after_iApply_late_evar"
     : string
263
264
265
266
267
268
269
270
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
271
272
"test_wandM"
     : string
273
274
275
276
277
278
279
280
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
  "HPQ" : mP -∗? Q
  "HQR" : Q -∗ R
281
  "HP" : default emp mP
282
283
284
285
286
287
288
289
290
  --------------------------------------∗
  R
  
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
291
  "HP" : default emp mP
292
  --------------------------------------∗
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
  default emp mP
  
"elim_mod_accessor"
     : string
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  X : Type
  E1, E2 : coPset.coPset
  α : X → PROP
  β : X → PROP
  γ : X → option PROP
  ============================
  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
  --------------------------------------∗
  |={E2,E1}=> True
310
  
Ralf Jung's avatar
Ralf Jung committed
311
312
"print_long_line_1"
     : string
313
314
315
316
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
317
  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
318
  ============================
319
320
  "HP" : 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
321
  --------------------------------------∗
322
  True
323
324
325
326
  
1 subgoal
  
  PROP : sbi
327
  BiFUpd0 : BiFUpd PROP
328
  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
329
  ============================
330
331
  _ : 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
332
  --------------------------------------∗
333
  True
334
  
Ralf Jung's avatar
Ralf Jung committed
335
336
"print_long_line_2"
     : string
337
338
339
1 subgoal
  
  PROP : sbi
340
  BiFUpd0 : BiFUpd PROP
341
  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
342
  ============================
343
344
  "HP" : 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 }}
345
  --------------------------------------∗
346
  True
347
348
349
350
  
1 subgoal
  
  PROP : sbi
351
  BiFUpd0 : BiFUpd PROP
352
  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
353
  ============================
354
355
  _ : 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 }}
356
  --------------------------------------∗
357
  True
358
  
Ralf Jung's avatar
Ralf Jung committed
359
360
"long_impl"
     : string
361
362
363
364
365
366
367
368
369
370
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
371
372
"long_impl_nested"
     : string
373
374
375
376
377
378
379
380
381
382
383
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
384
385
"long_wand"
     : string
386
387
388
389
390
391
392
393
394
395
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
396
397
"long_wand_nested"
     : string
398
399
400
401
402
403
404
405
406
407
408
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
     -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
409
410
"long_fupd"
     : string
411
412
413
414
415
416
417
418
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
419
420
  PPPPPPPPPPPPPPPPP
  ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
421
  
Ralf Jung's avatar
Ralf Jung committed
422
423
"long_fupd_nested"
     : string
424
425
426
427
428
429
430
431
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
432
433
434
  PPPPPPPPPPPPPPPPP
  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
             ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
435
  
436
437
"iAlways_spatial_non_empty"
     : string
438
439
440
441
The command has indeed failed with message:
In nested Ltac calls to "iAlways", "iModIntro" and 
"iModIntro (uconstr)", last call failed.
Tactic failure: iModIntro: spatial context is non-empty.
442
443
"iDestruct_bad_name"
     : string
444
445
446
447
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", last call failed.
448
Tactic failure: iDestruct: "HQ" not found.
449
450
"iIntros_dup_name"
     : string
451
452
453
454
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
455
456
457
458
The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
459
"iSplitL_one_of_many"
460
     : string
461
462
463
464
465
466
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
467
468
469
470
471
472
473
474
"iSplitR_one_of_many"
     : string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
475
476
477
478
479
480
481
482
483
484
"iSplitL_non_splittable"
     : string
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: P not a separating conjunction.
"iSplitR_non_splittable"
     : string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: P not a separating conjunction.
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
"iCombine_fail"
     : string
The command has indeed failed with message:
Ltac call to "iCombine (constr) as (constr)" failed.
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
510
511
"iExact_fail"
     : string
512
513
514
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HP"
not absorbing and the remaining hypotheses not affine.
"iClear_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HP" not found.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)",
"<iris.proofmode.ltac_tactics.iClear_go>" and
"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
"iSpecializeArgs_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializeArgs (constr) (open_constr)",
"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
"notypeclasses refine (uconstr)", last call failed.
In environment
PROP : sbi
P : PROP
The term "true" has type "bool" while it is expected to have type "nat".
"iStartProof_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
     : string
The command has indeed failed with message:
555
556
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
Robbert Krebbers's avatar
Robbert Krebbers committed
557
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" and
558
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
559
560
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
561
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
562
563
564
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
565
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
566
567
568
569
570
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
571
Tactic failure: iRename: "H" not fresh.
572
573
574
575
576
577
578
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
"spec_tac" (bound to
fun _ =>
  lazymatch lem with
  | {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
  {| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
  | _ => idtac
  end), "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
599
600
601
602
603
604
605
606
607
608
"iPoseProofCoreHyp_not_found_fail"
     : string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_fresh_fail"
     : string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "H1" not fresh.
609
610
611
612
613
614
615
616
617
618
619
"iRevert_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "H" not found.
"iDestruct_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
620
621
622
623
624
625
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", 
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
626
627
628
629
630
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)",
631
632
633
634
635
636
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", 
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
637
638
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
639
640
641
642
643
644
645
646
"iOrDestruct_fail"
     : string
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
647
648
649
650
"iApply_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
651
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
652
653
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
654
Tactic failure: iApply: cannot apply P.
655
656
657
658
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
659
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
660
661
662
663
664
665
666
667
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.
"iApply_fail_not_affine_2"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
668
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
669
670
671
672
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.