proofmode.ref 23.1 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
Tactic failure: iSpecialize: Q not persistent.
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
"test_iSpecialize_impl_pure"
     : string
1 goal
  
  PROP : bi
  φ : Prop
  P, Q : PROP
  H : φ
  ============================
  --------------------------------------∗
  <affine> ⌜φ⌝
"test_iSpecialize_impl_pure_affine"
     : string
1 goal
  
  PROP : bi
  BiAffine0 : BiAffine PROP
  φ : Prop
  P, Q : PROP
  H : φ
  ============================
  --------------------------------------∗
  ⌜φ⌝
169
170
171
172
"test_iAssert_intuitionistic"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: (|==> P)%I not persistent.
173
174
175
176
177
178
179
180
181
182
183
184
185
186
"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)
187
The command has indeed failed with message:
188
189
190
191
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
192
193
"test_iNext_plus_3"
     : string
194
1 goal
195
  
196
  PROP : bi
197
198
199
200
201
  P, Q : PROP
  n, m, k : nat
  ============================
  --------------------------------------∗
  ▷^(S n + S m) emp
202
203
"test_specialize_nested_intuitionistic"
     : string
204
1 goal
205
  
206
  PROP : bi
207
208
209
210
211
212
213
214
215
216
  φ : Prop
  P, P2, Q, R1, R2 : PROP
  H : φ
  ============================
  "HP" : P
  "HQ" : P -∗ Q
  --------------------------------------□
  "HR" : R2
  --------------------------------------∗
  R2
Robbert Krebbers's avatar
Robbert Krebbers committed
217
218
"test_iSimpl_in"
     : string
219
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
220
  
221
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
222
223
224
225
226
  x, y : nat
  ============================
  "H" : ⌜S (S (S x)) = y⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
227
1 goal
228
  
229
  PROP : bi
230
231
232
233
234
235
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  "H2" : ⌜S y = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
236
1 goal
237
  
238
  PROP : bi
239
240
241
242
243
244
245
  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
246
247
248
249
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
Tactic failure: iEval: %: unsupported selection pattern.
250
251
252
253
254
255
256
257
258
259
"test_iRename"
     : string
1 goal
  
  PROP : bi
  P : PROP
  ============================
  "X" : P
  --------------------------------------□
  P
Ralf Jung's avatar
Ralf Jung committed
260
261
"test_iFrame_later_1"
     : string
262
1 goal
263
  
264
  PROP : bi
265
266
267
268
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
Ralf Jung's avatar
Ralf Jung committed
269
270
"test_iFrame_later_2"
     : string
271
1 goal
272
  
273
  PROP : bi
274
275
276
277
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
278
279
The command has indeed failed with message:
Tactic failure: iFrame: cannot frame Q.
280
281
282
283
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
284
285
"test_and_sep_affine_bi"
     : string
286
1 goal
287
  
288
  PROP : bi
289
  BiAffine0 : BiAffine PROP
290
291
292
293
294
295
  P, Q : PROP
  ============================
  _ : □ P
  _ : Q
  --------------------------------------∗
  □ P
Ralf Jung's avatar
Ralf Jung committed
296
297
"test_big_sepL_simpl"
     : string
298
1 goal
299
  
300
  PROP : bi
301
302
303
304
305
306
307
308
309
  x : nat
  l : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y ∈ l, <affine> ⌜y = y⌝
  _ : [∗ list] y ∈ (x :: l), <affine> ⌜y = y⌝
  --------------------------------------∗
  P
310
1 goal
311
  
312
  PROP : bi
313
314
315
316
317
318
319
320
321
  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
322
323
"test_big_sepL2_simpl"
     : string
324
1 goal
325
  
326
  PROP : bi
327
328
329
330
331
332
333
334
335
  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)
336
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
337
  
338
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
339
340
341
342
343
344
  x1, x2 : nat
  l1, l2 : list nat
  P : PROP
  ============================
  "HP" : P
  _ : [∗ list] y1;y2 ∈ [];l2, <affine> ⌜y1 = y2⌝
345
346
  _ : <affine> ⌜x1 = x2⌝ ∗
      ([∗ list] y1;y2 ∈ l1;(l2 ++ l2), <affine> ⌜y1 = y2⌝)
Robbert Krebbers's avatar
Robbert Krebbers committed
347
348
  --------------------------------------∗
  P ∨ True ∗ ([∗ list] _;_ ∈ l1;l2, True)
Ralf Jung's avatar
Ralf Jung committed
349
350
"test_big_sepL2_iDestruct"
     : string
351
1 goal
Robbert Krebbers's avatar
Robbert Krebbers committed
352
  
353
  PROP : bi
Robbert Krebbers's avatar
Robbert Krebbers committed
354
355
356
357
358
359
360
361
  Φ : 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
362
363
"test_reducing_after_iDestruct"
     : string
364
1 goal
365
  
366
  PROP : bi
367
368
369
370
  ============================
  "H" : □ True
  --------------------------------------∗
  True
Ralf Jung's avatar
Ralf Jung committed
371
372
"test_reducing_after_iApply"
     : string
373
1 goal
374
  
375
  PROP : bi
376
377
378
379
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
Ralf Jung's avatar
Ralf Jung committed
380
381
"test_reducing_after_iApply_late_evar"
     : string
382
1 goal
383
  
384
  PROP : bi
385
386
387
388
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
Ralf Jung's avatar
Ralf Jung committed
389
390
"test_wandM"
     : string
391
1 goal
392
  
393
  PROP : bi
394
395
396
397
398
  mP : option PROP
  Q, R : PROP
  ============================
  "HPQ" : mP -∗? Q
  "HQR" : Q -∗ R
399
  "HP" : default emp mP
400
401
  --------------------------------------∗
  R
402
1 goal
403
  
404
  PROP : bi
405
406
407
  mP : option PROP
  Q, R : PROP
  ============================
408
  "HP" : default emp mP
409
  --------------------------------------∗
410
  default emp mP
411
412
413
414
415
416
417
418
419
420
421
422
"test_iApply_prettification3"
     : string
1 goal
  
  PROP : bi
  Ψ, Φ : nat → PROP
  HP : ∀ (f : nat → nat) (y : nat),
         TCEq f (λ x : nat, x + 10) → Ψ (f 1) -∗ Φ y
  ============================
  "H" : Ψ 11
  --------------------------------------∗
  Ψ (1 + 10)
423
424
425
426
427
428
429
430
431
432
433
1 goal
  
  PROP : bi
  H : BiAffine PROP
  P, Q : PROP
  H0 : Laterable Q
  ============================
  "HP" : ▷ P
  "HQ" : Q
  --------------------------------------∗
  ▷ P ∗ Q
Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
"test_iRevert_pure"
     : string
1 goal
  
  PROP : bi
  φ : Prop
  P : PROP
  ============================
  "H" : <affine> ⌜φ⌝ -∗ P
  --------------------------------------∗
  <affine> ⌜φ⌝ -∗ P
"test_iRevert_pure_affine"
     : string
1 goal
  
  PROP : bi
  BiAffine0 : BiAffine PROP
  φ : Prop
  P : PROP
  ============================
  "H" : ⌜φ⌝ -∗ P
  --------------------------------------∗
  ⌜φ⌝ -∗ P
457
458
"elim_mod_accessor"
     : string
459
1 goal
460
  
461
  PROP : bi
462
463
464
  BiFUpd0 : BiFUpd PROP
  X : Type
  E1, E2 : coPset.coPset
465
  α, β : X → PROP
466
467
468
469
470
  γ : X → option PROP
  ============================
  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
  --------------------------------------∗
  |={E2,E1}=> True
Ralf Jung's avatar
Ralf Jung committed
471
472
"print_long_line_1"
     : string
473
1 goal
474
  
475
  PROP : bi
476
  BiFUpd0 : BiFUpd PROP
477
  P_P_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
478
  ============================
479
480
  "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
481
  --------------------------------------∗
482
  True
483
1 goal
484
  
485
  PROP : bi
486
  BiFUpd0 : BiFUpd PROP
487
  P_P_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
488
  ============================
489
490
  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
      P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
491
  --------------------------------------∗
492
  True
Ralf Jung's avatar
Ralf Jung committed
493
494
"print_long_line_2"
     : string
495
1 goal
496
  
497
  PROP : bi
498
  BiFUpd0 : BiFUpd PROP
499
  P_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
500
  ============================
501
502
  "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 }}
503
  --------------------------------------∗
504
  True
505
1 goal
506
  
507
  PROP : bi
508
  BiFUpd0 : BiFUpd PROP
509
  P_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
510
  ============================
511
512
  _ : 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 }}
513
  --------------------------------------∗
514
  True
Ralf Jung's avatar
Ralf Jung committed
515
516
"long_impl"
     : string
517
1 goal
518
  
519
  PROP : bi
520
521
522
523
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
524
525
  PPPPPPPPPPPPPPPPP → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
  QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
526
527
"long_impl_nested"
     : string
528
1 goal
529
  
530
  PROP : bi
531
532
533
534
535
536
537
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
538
539
"long_wand"
     : string
540
1 goal
541
  
542
  PROP : bi
543
544
545
546
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
547
548
  PPPPPPPPPPPPPPPPP -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
549
550
"long_wand_nested"
     : string
551
1 goal
552
  
553
  PROP : bi
554
555
556
557
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
558
559
560
  PPPPPPPPPPPPPPPPP -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
561
562
"long_fupd"
     : string
563
1 goal
564
  
565
  PROP : bi
566
567
568
569
570
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
571
572
  PPPPPPPPPPPPPPPPP ={E}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
573
574
"long_fupd_nested"
     : string
575
1 goal
576
  
577
  PROP : bi
578
579
580
581
582
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
583
584
585
  PPPPPPPPPPPPPPPPP ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Robbert Krebbers's avatar
Robbert Krebbers committed
586
587
588
589
"iStopProof_not_proofmode"
     : string
The command has indeed failed with message:
Tactic failure: iStopProof: proofmode not started.
590
591
"iAlways_spatial_non_empty"
     : string
592
593
The command has indeed failed with message:
Tactic failure: iModIntro: spatial context is non-empty.
594
595
"iDestruct_bad_name"
     : string
596
The command has indeed failed with message:
597
Tactic failure: iRename: "HQ" not found.
598
599
"iIntros_dup_name"
     : string
600
601
The command has indeed failed with message:
Tactic failure: iIntro: "HP" not fresh.
602
603
The command has indeed failed with message:
x is already used.
604
605
606
607
"iIntros_pure_not_forall"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: cannot turn (P -∗ Q)%I into a universal quantifier.
608
"iSplitL_one_of_many"
609
     : string
610
611
612
613
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.
614
615
616
617
618
619
"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.
620
621
622
623
624
625
626
627
"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.
628
629
630
631
632
633
634
635
636
637
638
639
"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
640
641
642
"iSpecialize_autoframe_fail"
     : string
The command has indeed failed with message:
643
Tactic failure: iSpecialize: premise P cannot be solved by framing.
Robbert Krebbers's avatar
Robbert Krebbers committed
644
The command has indeed failed with message:
645
646
647
648
649
650
651
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.
652
653
"iExact_fail"
     : string
654
655
The command has indeed failed with message:
Tactic failure: iExact: "HQ" not found.
656
657
658
The command has indeed failed with message:
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
659
Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing.
660
661
662
663
664
665
666
667
668
669
"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
670
PROP : bi
671
672
673
674
675
676
677
678
679
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:
680
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
681
682
The command has indeed failed with message:
Tactic failure: iRename: "H" not fresh.
683
684
685
686
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
Tactic failure: iPoseProof: "Hx" not found.
687
688
689
690
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
691
692
693
694
695
696
697
698
"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.
699
700
701
702
703
704
705
"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:
706
707
708
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.
709
The command has indeed failed with message:
710
711
Tactic failure: iDestruct: "HP //"
should contain exactly one proper introduction pattern.
712
713
The command has indeed failed with message:
Tactic failure: iDestruct: "[HP HQ HR]" has too many conjuncts.
714
The command has indeed failed with message:
715
716
717
718
719
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.
720
721
722
723
724
725
"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.
726
727
728
729
"iApply_fail"
     : string
The command has indeed failed with message:
Tactic failure: iApply: cannot apply P.
730
731
732
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
733
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
734
735
736
737
738
739
740
741
742
743
744
745
746
747
"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.
748
749
750
"iApply_fail_not_affine_2"
     : string
The command has indeed failed with message:
751
752
753
754
755
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.
756
757
758
759
"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.
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
"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".
778
"iLöb_no_BiLöb"
Robbert Krebbers's avatar
Robbert Krebbers committed
779
780
     : string
The command has indeed failed with message:
781
Tactic failure: iLöb: no 'BiLöb' instance found.
782
783
784
785
786
787
788
789
790
791
"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]".
792
793
794
795
796
797
798
799
800
801
"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
802
803
804
"iRevert_wrong_sel_pat"
     : string
The command has indeed failed with message:
805
806
807
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
808
809
810
"iInduction_wrong_sel_pat"
     : string
The command has indeed failed with message:
811
812
813
Tactic failure: sel_pat.parse: the term m
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
814
815
"test_pure_name"
     : string
816
1 goal
817
  
818
  PROP : bi
819
820
821
822
  P : PROP
  φ1, φ2 : Prop
  Himpl : φ1 → φ2
  HP2 : φ1
823
  ============================
824
  "HP" : P
825
  --------------------------------------∗
826
  P ∗ ⌜φ2⌝
827
828
829
830
"test_not_fresh"
     : string
The command has indeed failed with message:
H is already used.
831
832
833
834
835
836
837
838
839
840
841
842
"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.
843
844
845
846
847
848
849
850
"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.
Robbert Krebbers's avatar
Tests.    
Robbert Krebbers committed
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
"test_iInduction_Forall"
     : string
1 goal
  
  PROP : bi
  P : ntree → PROP
  l : list ntree
  ============================
  "H" : ∀ l0 : list ntree, (∀ x : ntree, ⌜x ∈ l0⌝ → P x) -∗ P (Tree l0)
  "IH" : [∗ list] x ∈ l, □ P x
  --------------------------------------□
  P (Tree l)
"test_iInduction_Forall_fail"
     : string
The command has indeed failed with message:
Tactic failure: iInduction: cannot import IH
(my_Forall
   (λ t : ntree,
      "H" : ∀ l : list ntree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
      --------------------------------------□
Robbert Krebbers's avatar
Tweaks.    
Robbert Krebbers committed
871
      P t) l) into proof mode context (IntoIH instance missing).