proofmode.ref 22.4 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
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
129
"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
Dan Frumin's avatar
Dan Frumin committed
130
131
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
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
446
447
"iDestructCore (open_constr) as (constr) (tactic3)" and
"iDestructCore (open_constr) as (constr) (tactic3)", 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
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
556
"iPoseProofCore (open_constr) as (constr) (tactic3)",
557
"iPoseProofCoreLem (constr) as (tactic3)" 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)",
Paolo G. Giarrusso's avatar
Paolo G. Giarrusso committed
562
"iPoseProofCore (open_constr) as (constr) (tactic3)",
563
564
565
566
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
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)",
567
568
569
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
570
Tactic failure: iRename: "H" not fresh.
571
572
573
574
"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
575
"iPoseProofCore (open_constr) as (constr) (tactic3)" and
576
577
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
578
579
580
581
"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
582
"iPoseProofCore (open_constr) as (constr) (tactic3)",
583
584
585
586
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
587
588
589
590
591
592
593
594
595
596
  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.
597
598
599
600
601
602
603
604
605
606
"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.
607
608
609
610
611
612
613
614
615
616
"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)",
617
618
619
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
620
621
622
623
"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.
624
625
626
627
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)",
628
629
630
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
631
632
633
634
"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.
635
636
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
637
638
639
640
641
642
643
644
"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.
645
646
647
648
"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
649
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
650
651
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
652
Tactic failure: iApply: cannot apply P.
653
654
655
656
"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
657
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
658
659
660
661
662
663
664
665
"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
666
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
667
668
669
670
"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.
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
"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
709
710
711
712
713
714
715
716
717
718
719
"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.