proofmode.ref 23.8 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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
"test_iStopProof"
     : string
1 subgoal
  
  PROP : sbi
  Q : PROP
  ============================
  "H1" : emp
  --------------------------------------□
  "H2" : Q
  --------------------------------------∗
  Q
  
1 subgoal
  
  PROP : sbi
  Q : PROP
  ============================
  □ emp ∗ Q -∗ Q
Ralf Jung's avatar
Ralf Jung committed
43
44
"test_iDestruct_and_emp"
     : string
45
46
47
1 subgoal
  
  PROP : sbi
48
49
50
51
52
53
54
55
56
  P, Q : PROP
  Persistent0 : Persistent P
  Persistent1 : Persistent Q
  ============================
  _ : P
  _ : Q
  --------------------------------------□
  <affine> (P ∗ Q)
  
57
58
59
60
61
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
62
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
63
Tactic failure: iElaborateSelPat: "HQ" not found.
64
65
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
Ralf Jung's avatar
Ralf Jung committed
66
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
67
Tactic failure: iElaborateSelPat: "HQ" not found.
68
The command has indeed failed with message:
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
In nested Ltac calls to "iSpecialize (open_constr) as #",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)" and
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
last call failed.
Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic"
     : string
The command has indeed failed with message:
In nested Ltac calls to "<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
"<ssreflect_plugin::ssrtclseq@0> iAssert (|==> P)%I with "[#]" as "#HPupd2" ; first  done",
"iAssert (open_constr) with (constr) as (constr)",
"iAssertCore (open_constr) with (constr) as (constr) (tactic3)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: (|==> P)%I not persistent.
The command has indeed failed with message:
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
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
103
104
"test_iNext_plus_3"
     : string
105
106
107
108
109
110
111
112
113
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  n, m, k : nat
  ============================
  --------------------------------------∗
  ▷^(S n + S m) emp
  
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
"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
130
131
132
133
134
135
136
137
138
139
140
"test_iSimpl_in"
     : string
1 subgoal
  
  PROP : sbi
  x, y : nat
  ============================
  "H" : ⌜S (S (S x)) = y⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
141
142
143
144
145
146
147
148
149
150
1 subgoal
  
  PROP : sbi
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  "H2" : ⌜S y = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
151
152
153
154
155
156
157
158
159
160
161
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
162
163
164
165
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
166
"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
Dan Frumin's avatar
Dan Frumin committed
167
168
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
Ralf Jung's avatar
Ralf Jung committed
169
170
"test_iFrame_later_1"
     : string
171
172
173
174
175
176
177
178
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
Ralf Jung's avatar
Ralf Jung committed
179
180
"test_iFrame_later_2"
     : string
181
182
183
184
185
186
187
188
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
189
190
191
192
193
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
194
195
"test_and_sep_affine_bi"
     : string
196
197
198
1 subgoal
  
  PROP : sbi
199
  BiAffine0 : BiAffine PROP
200
201
202
203
204
205
206
  P, Q : PROP
  ============================
  _ : □ P
  _ : Q
  --------------------------------------∗
  □ P
  
Ralf Jung's avatar
Ralf Jung committed
207
208
"test_big_sepL_simpl"
     : string
209
210
211
212
213
214
215
216
217
218
219
220
221
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
  
222
223
224
225
226
227
228
229
230
231
232
233
234
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
235
236
"test_big_sepL2_simpl"
     : string
237
238
239
240
241
242
243
244
245
246
247
248
249
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
250
251
252
253
254
255
256
257
258
259
260
261
262
263
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
264
265
"test_big_sepL2_iDestruct"
     : string
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
270
271
272
273
274
275
276
277
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
278
279
"test_reducing_after_iDestruct"
     : string
280
281
282
283
284
285
286
287
1 subgoal
  
  PROP : sbi
  ============================
  "H" : □ True
  --------------------------------------∗
  True
  
Ralf Jung's avatar
Ralf Jung committed
288
289
"test_reducing_after_iApply"
     : string
290
291
292
293
294
295
296
297
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
298
299
"test_reducing_after_iApply_late_evar"
     : string
300
301
302
303
304
305
306
307
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
308
309
"test_wandM"
     : string
310
311
312
313
314
315
316
317
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
  "HPQ" : mP -∗? Q
  "HQR" : Q -∗ R
318
  "HP" : default emp mP
319
320
321
322
323
324
325
326
327
  --------------------------------------∗
  R
  
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
328
  "HP" : default emp mP
329
  --------------------------------------∗
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
  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
347
  
Ralf Jung's avatar
Ralf Jung committed
348
349
"print_long_line_1"
     : string
350
351
352
353
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
354
  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
355
  ============================
356
357
  "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
358
  --------------------------------------∗
359
  True
360
361
362
363
  
1 subgoal
  
  PROP : sbi
364
  BiFUpd0 : BiFUpd PROP
365
  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
366
  ============================
367
368
  _ : 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
369
  --------------------------------------∗
370
  True
371
  
Ralf Jung's avatar
Ralf Jung committed
372
373
"print_long_line_2"
     : string
374
375
376
1 subgoal
  
  PROP : sbi
377
  BiFUpd0 : BiFUpd PROP
378
  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
379
  ============================
380
381
  "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 }}
382
  --------------------------------------∗
383
  True
384
385
386
387
  
1 subgoal
  
  PROP : sbi
388
  BiFUpd0 : BiFUpd PROP
389
  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
390
  ============================
391
392
  _ : 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 }}
393
  --------------------------------------∗
394
  True
395
  
Ralf Jung's avatar
Ralf Jung committed
396
397
"long_impl"
     : string
398
399
400
401
402
403
404
405
406
407
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
408
409
"long_impl_nested"
     : string
410
411
412
413
414
415
416
417
418
419
420
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
421
422
"long_wand"
     : string
423
424
425
426
427
428
429
430
431
432
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
433
434
"long_wand_nested"
     : string
435
436
437
438
439
440
441
442
443
444
445
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
     -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
Ralf Jung's avatar
Ralf Jung committed
446
447
"long_fupd"
     : string
448
449
450
451
452
453
454
455
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
456
457
  PPPPPPPPPPPPPPPPP
  ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
458
  
Ralf Jung's avatar
Ralf Jung committed
459
460
"long_fupd_nested"
     : string
461
462
463
464
465
466
467
468
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
469
470
471
  PPPPPPPPPPPPPPPPP
  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
             ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
472
  
Robbert Krebbers's avatar
Robbert Krebbers committed
473
474
475
476
477
"iStopProof_not_proofmode"
     : string
The command has indeed failed with message:
Ltac call to "iStopProof" failed.
Tactic failure: iStopProof: proofmode not started.
478
479
"iAlways_spatial_non_empty"
     : string
480
481
482
483
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.
484
485
"iDestruct_bad_name"
     : string
486
487
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
488
489
"iDestructCore (open_constr) as (constr) (tactic3)" and
"iDestructCore (open_constr) as (constr) (tactic3)", last call failed.
490
Tactic failure: iDestruct: "HQ" not found.
491
492
"iIntros_dup_name"
     : string
493
494
495
496
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.
497
498
499
500
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.
501
"iSplitL_one_of_many"
502
     : string
503
504
505
506
507
508
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.
509
510
511
512
513
514
515
516
"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.
517
518
519
520
521
522
523
524
525
526
"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.
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
"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.
552
553
"iExact_fail"
     : string
554
555
556
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" not found.
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
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:
597
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
598
"iPoseProofCore (open_constr) as (constr) (tactic3)",
599
600
601
"iPoseProofCoreLem (open_constr) as (tactic3)" and 
"iIntoEmpValid", last call failed.
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
602
The command has indeed failed with message:
603
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
604
"iPoseProofCore (open_constr) as (constr) (tactic3)",
605
"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
606
607
608
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
609
610
611
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
612
Tactic failure: iRename: "H" not fresh.
613
614
615
616
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
617
"iPoseProofCore (open_constr) as (constr) (tactic3)" and
618
619
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
620
621
622
623
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
624
"iPoseProofCore (open_constr) as (constr) (tactic3)",
625
"iPoseProofCoreLem (open_constr) as (tactic3)", "tac" (bound to
626
627
628
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
629
630
631
632
633
634
635
636
637
638
  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.
639
640
641
642
643
644
645
646
647
648
"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.
649
650
651
652
653
654
655
656
657
658
"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)",
659
660
661
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
662
663
664
665
"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.
666
667
668
669
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)",
670
671
672
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
673
674
675
676
"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.
677
678
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
679
680
681
682
683
684
685
686
"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.
687
688
689
690
"iApply_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
691
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
692
693
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
694
Tactic failure: iApply: cannot apply P.
695
696
697
698
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
699
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
700
701
702
703
704
705
706
707
"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)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
708
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
709
710
711
712
"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.
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
"iRevert_wrong_var"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert ( (ident) )" and 
"iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k1 not in scope.
The command has indeed failed with message:
In nested Ltac calls to "iLöb as (constr) forall ( (ident) )",
"iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
"iRevertIntros_go", "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as
IH), "tac" (bound to iRevertIntros ( x1 ) "" with iLöbCore as IH),
"iRevertIntros ( (ident) ) (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )), 
"tac" (bound to iRevert ( x1 ); tac; iIntros ( x1 )),
"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k1 not in scope.
"iRevert_dup_var"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert ( (ident) (ident) )",
"iRevert ( (ident) )" and "iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k not in scope.
"iRevert_dep_var_coq"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert ( (ident) )", "iForallRevert (ident)" and
"revert (ne_var_list)", last call failed.
k is used in hypothesis Hk.
"iRevert_dep_var"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert ( (ident) )" and 
"iForallRevert (ident)", last call failed.
Tactic failure: iRevert: k is used in hypothesis "Hk".
Robbert Krebbers's avatar
Robbert Krebbers committed
751
752
753
754
755
756
757
758
759
760
761
"iLöb_no_sbi"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iLöb as (constr)",
"iLöbRevert (constr) with (tactic3)",
"iRevertIntros (constr) with (tactic3)", "iRevertIntros_go", 
"tac" (bound to iRevertIntros "∗" with tac), "tac" (bound to iRevertIntros
"∗" with tac), "iRevertIntros (constr) with (tactic3)", 
"iRevertIntros_go", "tac" (bound to iLöbCore as IH), 
"tac" (bound to iLöbCore as IH) and "iLöbCore as (constr)", last call failed.
Tactic failure: iLöb: not a step-indexed BI entailment.