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