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