proofmode.ref 21.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
"demo_0"
     : string
3
1 goal
4
  
5
  PROP : bi
6
  BiPersistentlyForall0 : BiPersistentlyForall PROP
7
8
9
10
11
12
13
  P, Q : PROP
  ============================
  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
  --------------------------------------□
  "H" : □ (P ∨ Q)
  --------------------------------------∗
  Q ∨ P
14
1 goal
15
  
16
  PROP : bi
17
  BiPersistentlyForall0 : BiPersistentlyForall PROP
18
19
20
21
22
23
  P, Q : PROP
  ============================
  "H2" : ∀ x : nat, ⌜x = 0⌝ ∨ ⌜x = 1⌝
  _ : P
  --------------------------------------□
  Q ∨ P
Ralf Jung's avatar
Ralf Jung committed
24
25
"test_iStopProof"
     : string
26
1 goal
Ralf Jung's avatar
Ralf Jung committed
27
  
28
  PROP : bi
Ralf Jung's avatar
Ralf Jung committed
29
30
31
32
33
34
35
  Q : PROP
  ============================
  "H1" : emp
  --------------------------------------□
  "H2" : Q
  --------------------------------------∗
  Q
36
1 goal
Ralf Jung's avatar
Ralf Jung committed
37
  
38
  PROP : bi
Ralf Jung's avatar
Ralf Jung committed
39
40
41
  Q : PROP
  ============================
  □ emp ∗ Q -∗ Q
Ralf Jung's avatar
Ralf Jung committed
42
43
"test_iDestruct_and_emp"
     : string
44
1 goal
45
  
46
  PROP : bi
47
48
49
50
51
52
53
54
  P, Q : PROP
  Persistent0 : Persistent P
  Persistent1 : Persistent Q
  ============================
  _ : P
  _ : Q
  --------------------------------------□
  <affine> (P ∗ Q)
55
56
"test_iDestruct_spatial"
     : string
57
1 goal
58
  
59
  PROP : bi
60
61
62
63
64
65
66
  Q : PROP
  ============================
  "HQ" : <affine> Q
  --------------------------------------∗
  Q
"test_iDestruct_spatial_affine"
     : string
67
1 goal
68
  
69
  PROP : bi
70
71
72
73
74
75
  Q : PROP
  Affine0 : Affine Q
  ============================
  "HQ" : Q
  --------------------------------------∗
  Q
76
77
78
79
80
81
"test_iDestruct_exists_not_exists"
     : string
The command has indeed failed with message:
Tactic failure: iExistDestruct: cannot destruct P.
"test_iDestruct_exists_intuitionistic"
     : string
82
1 goal
83
84
85
86
87
88
89
90
91
  
  PROP : bi
  P : PROP
  Φ : nat → PROP
  y : nat
  ============================
  "H" : Φ y ∧ P
  --------------------------------------□
  P
92
93
"test_iDestruct_exists_anonymous"
     : string
94
1 goal
95
96
97
98
99
100
101
102
103
  
  PROP : bi
  P : PROP
  Φ : nat → PROP
  H : nat
  ============================
  "HΦ" : ∃ x : nat, Φ x
  --------------------------------------∗
  ∃ x : nat, Φ x
104
105
"test_iIntros_forall_pure"
     : string
106
1 goal
107
  
108
  PROP : bi
109
  Ψ : nat → PROP
110
  x : nat
111
112
  ============================
  --------------------------------------∗
113
114
115
  Ψ x → Ψ x
"test_iIntros_pure_names"
     : string
116
1 goal
117
118
119
120
121
122
123
124
125
  
  PROP : bi
  H : True
  P : PROP
  x, y : nat
  H0 : x = y
  ============================
  --------------------------------------∗
  P -∗ P
126
127
128
The command has indeed failed with message:
No applicable tactic.
The command has indeed failed with message:
129
Tactic failure: iElaborateSelPat: "HQ" not found.
130
The command has indeed failed with message:
131
Tactic failure: iElaborateSelPat: "HQ" not found.
132
133
134
135
136
137
138
139
140
141
142
143
"test_iSpecialize_pure_error"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: P not pure.
"test_iSpecialize_pure_error"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot solve φ using done.
"test_iSpecialize_done_error"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot solve P using done.
144
The command has indeed failed with message:
145
146
147
148
149
Tactic failure: iSpecialize: Q not persistent.
"test_iAssert_intuitionistic"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: (|==> P)%I not persistent.
150
151
152
153
154
155
156
157
158
159
160
161
162
163
"test_iInduction_multiple_IHs"
     : string
1 goal
  
  PROP : bi
  l, t1 : tree
  Φ : tree → PROP
  ============================
  "Hleaf" : Φ leaf
  "Hnode" : ∀ l0 r : tree, Φ l0 -∗ Φ r -∗ Φ (node l0 r)
  "IH" : Φ l
  "IH1" : Φ t1
  --------------------------------------□
  Φ (node l t1)
164
The command has indeed failed with message:
165
166
167
168
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
The command has indeed failed with message:
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
Ralf Jung's avatar
Ralf Jung committed
169
170
"test_iNext_plus_3"
     : string
171
1 goal
172
  
173
  PROP : bi
174
175
176
177
178
  P, Q : PROP
  n, m, k : nat
  ============================
  --------------------------------------∗
  ▷^(S n + S m) emp
179
180
"test_specialize_nested_intuitionistic"
     : string
181
1 goal
182
  
183
  PROP : bi
184
185
186
187
188
189
190
191
192
193
  φ : Prop
  P, P2, Q, R1, R2 : PROP
  H : φ
  ============================
  "HP" : P
  "HQ" : P -∗ Q
  --------------------------------------□
  "HR" : R2
  --------------------------------------∗
  R2
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
"test_iSimpl_in"
     : string
196
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
197
  
198
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
199
200
201
202
203
  x, y : nat
  ============================
  "H" : ⌜S (S (S x)) = y⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
204
1 goal
205
  
206
  PROP : bi
207
208
209
210
211
212
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  "H2" : ⌜S y = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
213
1 goal
214
  
215
  PROP : bi
216
217
218
219
220
221
222
  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
223
224
225
226
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
Tactic failure: iEval: %: unsupported selection pattern.
227
228
229
230
231
232
233
234
235
236
"test_iRename"
     : string
1 goal
  
  PROP : bi
  P : PROP
  ============================
  "X" : P
  --------------------------------------□
  P
Ralf Jung's avatar
Ralf Jung committed
237
238
"test_iFrame_later_1"
     : string
239
1 goal
240
  
241
  PROP : bi
242
243
244
245
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
Ralf Jung's avatar
Ralf Jung committed
246
247
"test_iFrame_later_2"
     : string
248
1 goal
249
  
250
  PROP : bi
251
252
253
254
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
255
256
The command has indeed failed with message:
Tactic failure: iFrame: cannot frame Q.
257
258
259
260
The command has indeed failed with message:
No applicable tactic.
The command has indeed failed with message:
No applicable tactic.
Ralf Jung's avatar
Ralf Jung committed
261
262
"test_and_sep_affine_bi"
     : string
263
1 goal
264
  
265
  PROP : bi
266
  BiAffine0 : BiAffine PROP
267
268
269
270
271
272
  P, Q : PROP
  ============================
  _ : □ P
  _ : Q
  --------------------------------------∗
  □ P
Ralf Jung's avatar
Ralf Jung committed
273
274
"test_big_sepL_simpl"
     : string
275
1 goal
276
  
277
  PROP : bi
278
279
280
281
282
283
284
285
286
  x : nat
  l : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
  _ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
  --------------------------------------∗
  P
287
1 goal
288
  
289
  PROP : bi
290
291
292
293
294
295
296
297
298
  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
299
300
"test_big_sepL2_simpl"
     : string
301
1 goal
302
  
303
  PROP : bi
304
305
306
307
308
309
310
311
312
  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)
313
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
314
  
315
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
316
317
318
319
320
321
  x1, x2 : nat
  l1, l2 : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
322
323
  _ : <affine> ⌜x1 = x2⌝ ∗
      ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
Robbert Krebbers's avatar
Robbert Krebbers committed
324
325
  --------------------------------------∗
  P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
Ralf Jung's avatar
Ralf Jung committed
326
327
"test_big_sepL2_iDestruct"
     : string
328
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
329
  
330
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
331
332
333
334
335
336
337
338
  Φ : 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
339
340
"test_reducing_after_iDestruct"
     : string
341
1 goal
342
  
343
  PROP : bi
344
345
346
347
  ============================
  "H" : □ True
  --------------------------------------∗
  True
Ralf Jung's avatar
Ralf Jung committed
348
349
"test_reducing_after_iApply"
     : string
350
1 goal
351
  
352
  PROP : bi
353
354
355
356
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
Ralf Jung's avatar
Ralf Jung committed
357
358
"test_reducing_after_iApply_late_evar"
     : string
359
1 goal
360
  
361
  PROP : bi
362
363
364
365
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
Ralf Jung's avatar
Ralf Jung committed
366
367
"test_wandM"
     : string
368
1 goal
369
  
370
  PROP : bi
371
372
373
374
375
  mP : option PROP
  Q, R : PROP
  ============================
  "HPQ" : mP -∗? Q
  "HQR" : Q -∗ R
376
  "HP" : default emp mP
377
378
  --------------------------------------∗
  R
379
1 goal
380
  
381
  PROP : bi
382
383
384
  mP : option PROP
  Q, R : PROP
  ============================
385
  "HP" : default emp mP
386
  --------------------------------------∗
387
  default emp mP
388
389
390
391
392
393
394
395
396
397
398
1 goal
  
  PROP : bi
  H : BiAffine PROP
  P, Q : PROP
  H0 : Laterable Q
  ============================
  "HP" : ▷ P
  "HQ" : Q
  --------------------------------------∗
  ▷ P ∗ Q
399
400
"elim_mod_accessor"
     : string
401
1 goal
402
  
403
  PROP : bi
404
405
406
  BiFUpd0 : BiFUpd PROP
  X : Type
  E1, E2 : coPset.coPset
407
  α, β : X → PROP
408
409
410
411
412
  γ : X → option PROP
  ============================
  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
  --------------------------------------∗
  |={E2,E1}=> True
Ralf Jung's avatar
Ralf Jung committed
413
414
"print_long_line_1"
     : string
415
1 goal
416
  
417
  PROP : bi
418
  BiFUpd0 : BiFUpd PROP
419
  P_P_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
420
  ============================
421
422
  "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
423
  --------------------------------------∗
424
  True
425
1 goal
426
  
427
  PROP : bi
428
  BiFUpd0 : BiFUpd PROP
429
  P_P_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
430
  ============================
431
432
  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
      P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
433
  --------------------------------------∗
434
  True
Ralf Jung's avatar
Ralf Jung committed
435
436
"print_long_line_2"
     : string
437
1 goal
438
  
439
  PROP : bi
440
  BiFUpd0 : BiFUpd PROP
441
  P_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
442
  ============================
443
444
  "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 }}
445
  --------------------------------------∗
446
  True
447
1 goal
448
  
449
  PROP : bi
450
  BiFUpd0 : BiFUpd PROP
451
  P_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
452
  ============================
453
454
  _ : 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 }}
455
  --------------------------------------∗
456
  True
Ralf Jung's avatar
Ralf Jung committed
457
458
"long_impl"
     : string
459
1 goal
460
  
461
  PROP : bi
462
463
464
465
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
466
467
  PPPPPPPPPPPPPPPPP → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
  QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
468
469
"long_impl_nested"
     : string
470
1 goal
471
  
472
  PROP : bi
473
474
475
476
477
478
479
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
480
481
"long_wand"
     : string
482
1 goal
483
  
484
  PROP : bi
485
486
487
488
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
489
490
  PPPPPPPPPPPPPPPPP -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
491
492
"long_wand_nested"
     : string
493
1 goal
494
  
495
  PROP : bi
496
497
498
499
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
500
501
502
  PPPPPPPPPPPPPPPPP -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
503
504
"long_fupd"
     : string
505
1 goal
506
  
507
  PROP : bi
508
509
510
511
512
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
513
514
  PPPPPPPPPPPPPPPPP ={E}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
515
516
"long_fupd_nested"
     : string
517
1 goal
518
  
519
  PROP : bi
520
521
522
523
524
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
525
526
527
  PPPPPPPPPPPPPPPPP ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Robbert Krebbers's avatar
Robbert Krebbers committed
528
529
530
531
"iStopProof_not_proofmode"
     : string
The command has indeed failed with message:
Tactic failure: iStopProof: proofmode not started.
532
533
"iAlways_spatial_non_empty"
     : string
534
535
The command has indeed failed with message:
Tactic failure: iModIntro: spatial context is non-empty.
536
537
"iDestruct_bad_name"
     : string
538
The command has indeed failed with message:
539
Tactic failure: iRename: "HQ" not found.
540
541
"iIntros_dup_name"
     : string
542
543
The command has indeed failed with message:
Tactic failure: iIntro: "HP" not fresh.
544
545
The command has indeed failed with message:
x is already used.
546
547
548
549
"iIntros_pure_not_forall"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: cannot turn (P -∗ Q)%I into a universal quantifier.
550
"iSplitL_one_of_many"
551
     : string
552
553
554
555
The command has indeed failed with message:
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
556
557
558
559
560
561
"iSplitR_one_of_many"
     : string
The command has indeed failed with message:
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
562
563
564
565
566
567
568
569
"iSplitL_non_splittable"
     : string
The command has indeed failed with message:
Tactic failure: iSplitL: P not a separating conjunction.
"iSplitR_non_splittable"
     : string
The command has indeed failed with message:
Tactic failure: iSplitR: P not a separating conjunction.
570
571
572
573
574
575
576
577
578
579
580
581
"iCombine_fail"
     : string
The command has indeed failed with message:
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: "H" not found.
Robbert Krebbers's avatar
Robbert Krebbers committed
582
583
584
"iSpecialize_autoframe_fail"
     : string
The command has indeed failed with message:
585
Tactic failure: iSpecialize: premise P cannot be solved by framing.
Robbert Krebbers's avatar
Robbert Krebbers committed
586
The command has indeed failed with message:
587
588
589
590
591
592
593
Tactic failure: iSpecialize: premise P cannot be solved by framing.
"iSpecialize_autoframe_fail2"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: premise Q cannot be solved by framing.
The command has indeed failed with message:
Tactic failure: iSpecialize: premise Q cannot be solved by framing.
594
595
"iExact_fail"
     : string
596
597
The command has indeed failed with message:
Tactic failure: iExact: "HQ" not found.
598
599
600
The command has indeed failed with message:
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
601
Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing.
602
603
604
605
606
607
608
609
610
611
"iClear_fail"
     : string
The command has indeed failed with message:
Tactic failure: iElaborateSelPat: "HP" not found.
The command has indeed failed with message:
Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
"iSpecializeArgs_fail"
     : string
The command has indeed failed with message:
In environment
612
PROP : bi
613
614
615
616
617
618
619
620
621
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:
Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
     : string
The command has indeed failed with message:
622
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
623
624
The command has indeed failed with message:
Tactic failure: iRename: "H" not fresh.
625
626
627
628
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
Tactic failure: iPoseProof: "Hx" not found.
629
630
631
632
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
633
634
635
636
637
638
639
640
"iPoseProofCoreHyp_not_found_fail"
     : string
The command has indeed failed with message:
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_fresh_fail"
     : string
The command has indeed failed with message:
Tactic failure: iPoseProof: "H1" not fresh.
641
642
643
644
645
646
647
"iRevert_fail"
     : string
The command has indeed failed with message:
Tactic failure: iElaborateSelPat: "H" not found.
"iDestruct_fail"
     : string
The command has indeed failed with message:
648
649
650
Tactic failure: iDestruct: "[{HP}]" has just a single conjunct.
The command has indeed failed with message:
Tactic failure: iDestruct: "// H" is not supported due to IDone.
651
The command has indeed failed with message:
652
653
Tactic failure: iDestruct: "HP //"
should contain exactly one proper introduction pattern.
654
655
The command has indeed failed with message:
Tactic failure: iDestruct: "[HP HQ HR]" has too many conjuncts.
656
The command has indeed failed with message:
657
658
659
660
661
Tactic failure: iDestruct: "[HP|HQ|HR]" has too many disjuncts.
The command has indeed failed with message:
Tactic failure: iDestruct: "[HP]" has just a single conjunct.
The command has indeed failed with message:
Tactic failure: iDestruct: in "[HP HQ|HR]" a disjunct has multiple patterns.
662
663
664
665
666
667
"iOrDestruct_fail"
     : string
The command has indeed failed with message:
Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
The command has indeed failed with message:
Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
668
669
670
671
"iApply_fail"
     : string
The command has indeed failed with message:
Tactic failure: iApply: cannot apply P.
672
673
674
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
675
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
676
677
678
679
680
681
682
683
684
685
686
687
688
689
"iIntros_fail_nonempty_spatial"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: introducing non-persistent "HP" : P
into non-empty spatial context.
"iIntros_fail_not_fresh"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: "HP" not fresh.
"iIntros_fail_nothing_to_introduce"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: could not introduce "HQ"
, goal is not a wand or implication.
690
691
692
"iApply_fail_not_affine_2"
     : string
The command has indeed failed with message:
693
694
695
696
697
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
"iAssumption_fail_not_affine_1"
     : string
The command has indeed failed with message:
Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
698
699
700
701
"iAssumption_fail_not_affine_2"
     : string
The command has indeed failed with message:
Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing.
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
"iRevert_wrong_var"
     : string
The command has indeed failed with message:
Tactic failure: iRevert: k1 not in scope.
The command has indeed failed with message:
Tactic failure: iRevert: k1 not in scope.
"iRevert_dup_var"
     : string
The command has indeed failed with message:
Tactic failure: iRevert: k not in scope.
"iRevert_dep_var_coq"
     : string
The command has indeed failed with message:
k is used in hypothesis Hk.
"iRevert_dep_var"
     : string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
720
"iLöb_no_BiLöb"
Robbert Krebbers's avatar
Robbert Krebbers committed
721
722
     : string
The command has indeed failed with message:
723
Tactic failure: iLöb: no 'BiLöb' instance found.
724
725
726
727
728
729
730
731
732
733
"iMod_mask_mismatch"
     : string
The command has indeed failed with message:
Tactic failure: 
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
The command has indeed failed with message:
Tactic failure: 
"Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]".
734
735
736
737
738
739
740
741
742
743
"iModIntro_mask_mismatch"
     : string
The command has indeed failed with message:
Tactic failure: 
"Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
The command has indeed failed with message:
Tactic failure: 
"Only non-mask-changing update modalities can be introduced directly.
Use [iApply fupd_mask_intro] to introduce mask-changing update modalities".
Robbert Krebbers's avatar
Robbert Krebbers committed
744
745
746
"iRevert_wrong_sel_pat"
     : string
The command has indeed failed with message:
747
748
749
Tactic failure: sel_pat.parse: the term n
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
Robbert Krebbers's avatar
Robbert Krebbers committed
750
751
752
"iInduction_wrong_sel_pat"
     : string
The command has indeed failed with message:
753
754
755
Tactic failure: sel_pat.parse: the term m
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
756
757
"test_pure_name"
     : string
758
1 goal
759
  
760
  PROP : bi
761
762
763
764
  P : PROP
  φ1, φ2 : Prop
  Himpl : φ1 → φ2
  HP2 : φ1
765
  ============================
766
  "HP" : P
767
  --------------------------------------∗
768
  P ∗ ⌜φ2⌝
769
770
771
772
"test_not_fresh"
     : string
The command has indeed failed with message:
H is already used.
773
774
775
776
777
778
779
780
781
782
783
784
"test_iRename_select1"
     : string
The command has indeed failed with message:
No matching clauses for match.
"test_iDestruct_select2"
     : string
The command has indeed failed with message:
Tactic failure: iPure: (φ n) not pure.
"test_iDestruct_select_no_backtracking"
     : string
The command has indeed failed with message:
Tactic failure: iIntuitionistic: Q not persistent.
785
786
787
788
789
790
791
792
"test_iDestruct_intuitionistic_not_fresh"
     : string
The command has indeed failed with message:
Tactic failure: iIntuitionistic: "H" not fresh.
"test_iDestruct_spatial_not_fresh"
     : string
The command has indeed failed with message:
Tactic failure: iSpatial: "H" not fresh.