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