proofmode.ref 22.7 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
399
"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)
400
401
402
403
404
405
406
407
408
409
410
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
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
"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
434
435
"elim_mod_accessor"
     : string
436
1 goal
437
  
438
  PROP : bi
439
440
441
  BiFUpd0 : BiFUpd PROP
  X : Type
  E1, E2 : coPset.coPset
442
  α, β : X → PROP
443
444
445
446
447
  γ : X → option PROP
  ============================
  "Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
  --------------------------------------∗
  |={E2,E1}=> True
Ralf Jung's avatar
Ralf Jung committed
448
449
"print_long_line_1"
     : string
450
1 goal
451
  
452
  PROP : bi
453
  BiFUpd0 : BiFUpd PROP
454
  P_P_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
455
  ============================
456
457
  "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
458
  --------------------------------------∗
459
  True
460
1 goal
461
  
462
  PROP : bi
463
  BiFUpd0 : BiFUpd PROP
464
  P_P_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
465
  ============================
466
467
  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P ∗
      P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
468
  --------------------------------------∗
469
  True
Ralf Jung's avatar
Ralf Jung committed
470
471
"print_long_line_2"
     : string
472
1 goal
473
  
474
  PROP : bi
475
  BiFUpd0 : BiFUpd PROP
476
  P_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
477
  ============================
478
479
  "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 }}
480
  --------------------------------------∗
481
  True
482
1 goal
483
  
484
  PROP : bi
485
  BiFUpd0 : BiFUpd PROP
486
  P_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
487
  ============================
488
489
  _ : 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 }}
490
  --------------------------------------∗
491
  True
Ralf Jung's avatar
Ralf Jung committed
492
493
"long_impl"
     : string
494
1 goal
495
  
496
  PROP : bi
497
498
499
500
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
501
502
  PPPPPPPPPPPPPPPPP → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
  QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
503
504
"long_impl_nested"
     : string
505
1 goal
506
  
507
  PROP : bi
508
509
510
511
512
513
514
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
515
516
"long_wand"
     : 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_wand_nested"
     : string
528
1 goal
529
  
530
  PROP : bi
531
532
533
534
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
535
536
537
  PPPPPPPPPPPPPPPPP -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ -∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
538
539
"long_fupd"
     : string
540
1 goal
541
  
542
  PROP : bi
543
544
545
546
547
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
548
549
  PPPPPPPPPPPPPPPPP ={E}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Ralf Jung's avatar
Ralf Jung committed
550
551
"long_fupd_nested"
     : string
552
1 goal
553
  
554
  PROP : bi
555
556
557
558
559
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
560
561
562
  PPPPPPPPPPPPPPPPP ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ={E1,E2}=∗
  QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
Robbert Krebbers's avatar
Robbert Krebbers committed
563
564
565
566
"iStopProof_not_proofmode"
     : string
The command has indeed failed with message:
Tactic failure: iStopProof: proofmode not started.
567
568
"iAlways_spatial_non_empty"
     : string
569
570
The command has indeed failed with message:
Tactic failure: iModIntro: spatial context is non-empty.
571
572
"iDestruct_bad_name"
     : string
573
The command has indeed failed with message:
574
Tactic failure: iRename: "HQ" not found.
575
576
"iIntros_dup_name"
     : string
577
578
The command has indeed failed with message:
Tactic failure: iIntro: "HP" not fresh.
579
580
The command has indeed failed with message:
x is already used.
581
582
583
584
"iIntros_pure_not_forall"
     : string
The command has indeed failed with message:
Tactic failure: iIntro: cannot turn (P -∗ Q)%I into a universal quantifier.
585
"iSplitL_one_of_many"
586
     : string
587
588
589
590
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.
591
592
593
594
595
596
"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.
597
598
599
600
601
602
603
604
"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.
605
606
607
608
609
610
611
612
613
614
615
616
"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
617
618
619
"iSpecialize_autoframe_fail"
     : string
The command has indeed failed with message:
620
Tactic failure: iSpecialize: premise P cannot be solved by framing.
Robbert Krebbers's avatar
Robbert Krebbers committed
621
The command has indeed failed with message:
622
623
624
625
626
627
628
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.
629
630
"iExact_fail"
     : string
631
632
The command has indeed failed with message:
Tactic failure: iExact: "HQ" not found.
633
634
635
The command has indeed failed with message:
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
636
Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing.
637
638
639
640
641
642
643
644
645
646
"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
647
PROP : bi
648
649
650
651
652
653
654
655
656
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:
657
Tactic failure: iPoseProof: (0 = 0) not a BI assertion.
658
659
The command has indeed failed with message:
Tactic failure: iRename: "H" not fresh.
660
661
662
663
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
Tactic failure: iPoseProof: "Hx" not found.
664
665
666
667
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
668
669
670
671
672
673
674
675
"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.
676
677
678
679
680
681
682
"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:
683
684
685
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.
686
The command has indeed failed with message:
687
688
Tactic failure: iDestruct: "HP //"
should contain exactly one proper introduction pattern.
689
690
The command has indeed failed with message:
Tactic failure: iDestruct: "[HP HQ HR]" has too many conjuncts.
691
The command has indeed failed with message:
692
693
694
695
696
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.
697
698
699
700
701
702
"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.
703
704
705
706
"iApply_fail"
     : string
The command has indeed failed with message:
Tactic failure: iApply: cannot apply P.
707
708
709
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
710
Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing.
711
712
713
714
715
716
717
718
719
720
721
722
723
724
"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.
725
726
727
"iApply_fail_not_affine_2"
     : string
The command has indeed failed with message:
728
729
730
731
732
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.
733
734
735
736
"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.
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
"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".
755
"iLöb_no_BiLöb"
Robbert Krebbers's avatar
Robbert Krebbers committed
756
757
     : string
The command has indeed failed with message:
758
Tactic failure: iLöb: no 'BiLöb' instance found.
759
760
761
762
763
764
765
766
767
768
"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]".
769
770
771
772
773
774
775
776
777
778
"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
779
780
781
"iRevert_wrong_sel_pat"
     : string
The command has indeed failed with message:
782
783
784
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
785
786
787
"iInduction_wrong_sel_pat"
     : string
The command has indeed failed with message:
788
789
790
Tactic failure: sel_pat.parse: the term m
is expected to be a selection pattern (usually a string),
but has unexpected type nat.
791
792
"test_pure_name"
     : string
793
1 goal
794
  
795
  PROP : bi
796
797
798
799
  P : PROP
  φ1, φ2 : Prop
  Himpl : φ1 → φ2
  HP2 : φ1
800
  ============================
801
  "HP" : P
802
  --------------------------------------∗
803
  P ∗ ⌜φ2⌝
804
805
806
807
"test_not_fresh"
     : string
The command has indeed failed with message:
H is already used.
808
809
810
811
812
813
814
815
816
817
818
819
"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.
820
821
822
823
824
825
826
827
"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
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
"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
848
      P t) l) into proof mode context (IntoIH instance missing).