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