proofmode.ref 20.2 KB
Newer Older
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
  
24 25
"test_iDestruct_and_emp"
     : string
26 27 28
1 subgoal
  
  PROP : sbi
29 30 31 32 33 34 35 36 37
  P, Q : PROP
  Persistent0 : Persistent P
  Persistent1 : Persistent Q
  ============================
  _ : P
  _ : Q
  --------------------------------------□
  <affine> (P ∗ Q)
  
38 39 40 41 42
The command has indeed failed with message:
Ltac call to "done" failed.
No applicable tactic.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
43
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
44
Tactic failure: iElaborateSelPat: "HQ" not found.
45 46
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
47
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
48
Tactic failure: iElaborateSelPat: "HQ" not found.
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
P.
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
66 67
"test_iNext_plus_3"
     : string
68 69 70 71 72 73 74 75 76
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  n, m, k : nat
  ============================
  --------------------------------------∗
  ▷^(S n + S m) emp
  
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
"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
  
93 94 95 96 97 98 99 100 101 102 103
"test_iSimpl_in"
     : string
1 subgoal
  
  PROP : sbi
  x, y : nat
  ============================
  "H" : ⌜S (S (S x)) = y⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
104 105 106 107 108 109 110 111 112 113
1 subgoal
  
  PROP : sbi
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  "H2" : ⌜S y = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
114 115 116 117 118 119 120 121 122 123 124
1 subgoal
  
  PROP : sbi
  x, y, z : nat
  ============================
  "H1" : ⌜S (S (S x)) = y⌝
  --------------------------------------□
  "H2" : ⌜(1 + y)%nat = z⌝
  --------------------------------------∗
  ⌜S (S (S x)) = y⌝
  
125 126 127 128
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
129
"iEval (tactic3) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
130 131
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
132 133
"test_iFrame_later_1"
     : string
134 135 136 137 138 139 140 141
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
142 143
"test_iFrame_later_2"
     : string
144 145 146 147 148 149 150 151
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
152 153 154 155 156
The command has indeed failed with message:
In nested Ltac calls to "iFrame (constr)",
"<iris.proofmode.ltac_tactics.iFrame_go>" and
"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
Tactic failure: iFrame: cannot frame Q.
157 158
"test_and_sep_affine_bi"
     : string
159 160 161
1 subgoal
  
  PROP : sbi
162
  BiAffine0 : BiAffine PROP
163 164 165 166 167 168 169
  P, Q : PROP
  ============================
  _ : □ P
  _ : Q
  --------------------------------------∗
  □ P
  
170 171
"test_big_sepL_simpl"
     : string
172 173 174 175 176 177 178 179 180 181 182 183 184
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
  
185 186 187 188 189 190 191 192 193 194 195 196 197
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
  
198 199
"test_big_sepL2_simpl"
     : string
200 201 202 203 204 205 206 207 208 209 210 211 212
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)
  
213 214 215 216 217 218 219 220 221 222 223 224 225 226
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)
  
227 228
"test_big_sepL2_iDestruct"
     : string
229 230 231 232 233 234 235 236 237 238 239 240
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
  
241 242
"test_reducing_after_iDestruct"
     : string
243 244 245 246 247 248 249 250
1 subgoal
  
  PROP : sbi
  ============================
  "H" : □ True
  --------------------------------------∗
  True
  
251 252
"test_reducing_after_iApply"
     : string
253 254 255 256 257 258 259 260
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
261 262
"test_reducing_after_iApply_late_evar"
     : string
263 264 265 266 267 268 269 270
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
271 272
"test_wandM"
     : string
273 274 275 276 277 278 279 280
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
  "HPQ" : mP -∗? Q
  "HQR" : Q -∗ R
281
  "HP" : default emp mP
282 283 284 285 286 287 288 289 290
  --------------------------------------∗
  R
  
1 subgoal
  
  PROP : sbi
  mP : option PROP
  Q, R : PROP
  ============================
291
  "HP" : default emp mP
292
  --------------------------------------∗
293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309
  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
310
  
311 312
"print_long_line_1"
     : string
313 314 315 316
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
317
  P_P_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
318
  ============================
319 320
  "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
321
  --------------------------------------∗
322
  True
323 324 325 326
  
1 subgoal
  
  PROP : sbi
327
  BiFUpd0 : BiFUpd PROP
328
  P_P_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
329
  ============================
330 331
  _ : P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
      ∗ P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P_P
332
  --------------------------------------∗
333
  True
334
  
335 336
"print_long_line_2"
     : string
337 338 339
1 subgoal
  
  PROP : sbi
340
  BiFUpd0 : BiFUpd PROP
341
  P_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
342
  ============================
343 344
  "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 }}
345
  --------------------------------------∗
346
  True
347 348 349 350
  
1 subgoal
  
  PROP : sbi
351
  BiFUpd0 : BiFUpd PROP
352
  P_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
353
  ============================
354 355
  _ : 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 }}
356
  --------------------------------------∗
357
  True
358
  
359 360
"long_impl"
     : string
361 362 363 364 365 366 367 368 369 370
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
371 372
"long_impl_nested"
     : string
373 374 375 376 377 378 379 380 381 382 383
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
  PPPPPPPPPPPPPPPPP
  → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
    → QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
  
384 385
"long_wand"
     : 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
  
396 397
"long_wand_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
  
409 410
"long_fupd"
     : string
411 412 413 414 415 416 417 418
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
419 420
  PPPPPPPPPPPPPPPPP
  ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
421
  
422 423
"long_fupd_nested"
     : string
424 425 426 427 428 429 430 431
1 subgoal
  
  PROP : sbi
  BiFUpd0 : BiFUpd PROP
  E1, E2 : coPset.coPset
  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
  ============================
  --------------------------------------∗
432 433 434
  PPPPPPPPPPPPPPPPP
  ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
             ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
435
  
436 437
"iAlways_spatial_non_empty"
     : string
438 439 440 441
The command has indeed failed with message:
In nested Ltac calls to "iAlways", "iModIntro" and 
"iModIntro (uconstr)", last call failed.
Tactic failure: iModIntro: spatial context is non-empty.
442 443
"iDestruct_bad_name"
     : string
444 445
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
446 447
"iDestructCore (open_constr) as (constr) (tactic3)" and
"iDestructCore (open_constr) as (constr) (tactic3)", last call failed.
448
Tactic failure: iDestruct: "HQ" not found.
449 450
"iIntros_dup_name"
     : string
451 452 453 454
The command has indeed failed with message:
In nested Ltac calls to "iIntros (constr)", "iIntros_go" and
"iIntro (constr)", last call failed.
Tactic failure: iIntro: "HP" not fresh.
455 456 457 458
The command has indeed failed with message:
In nested Ltac calls to "iIntros ( (intropattern) )",
"iIntro ( (intropattern) )" and "intros x", last call failed.
x is already used.
459
"iSplitL_one_of_many"
460
     : string
461 462 463 464 465 466
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: hypotheses ["HPx"] not found.
467 468 469 470 471 472 473 474
"iSplitR_one_of_many"
     : string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: hypotheses ["HPx"] not found.
475 476 477 478 479 480 481 482 483 484
"iSplitL_non_splittable"
     : string
The command has indeed failed with message:
Ltac call to "iSplitL (constr)" failed.
Tactic failure: iSplitL: P not a separating conjunction.
"iSplitR_non_splittable"
     : string
The command has indeed failed with message:
Ltac call to "iSplitR (constr)" failed.
Tactic failure: iSplitR: P not a separating conjunction.
485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509
"iCombine_fail"
     : string
The command has indeed failed with message:
Ltac call to "iCombine (constr) as (constr)" failed.
Tactic failure: iCombine: hypotheses ["HP3"] not found.
"iSpecialize_bad_name1_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
"iSpecialize_bad_name2_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: "H" not found.
510 511
"iExact_fail"
     : string
512 513 514
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
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 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HQ" : Q does not match goal.
The command has indeed failed with message:
Ltac call to "iExact (constr)" failed.
Tactic failure: iExact: "HP"
not absorbing and the remaining hypotheses not affine.
"iClear_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "HP" not found.
The command has indeed failed with message:
In nested Ltac calls to "iClear (constr)",
"<iris.proofmode.ltac_tactics.iClear_go>" and
"<iris.proofmode.ltac_tactics.iClearHyp>", last call failed.
Tactic failure: iClear: "HP" : P not affine and the goal not absorbing.
"iSpecializeArgs_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSpecialize (open_constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializeArgs (constr) (open_constr)",
"<iris.proofmode.ltac_tactics.iSpecializeArgs_go>" and
"notypeclasses refine (uconstr)", last call failed.
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:
In nested Ltac calls to "iStartProof" and "iStartProof", last call failed.
Tactic failure: iStartProof: not a BI assertion.
"iPoseProof_fail"
     : string
The command has indeed failed with message:
555
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
556
"iPoseProofCore (open_constr) as (constr) (tactic3)",
557
"iPoseProofCoreLem (constr) as (tactic3)" and
558
"<iris.proofmode.ltac_tactics.iIntoEmpValid>", last call failed.
559 560
Tactic failure: iPoseProof: not a BI assertion.
The command has indeed failed with message:
561
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
562
"iPoseProofCore (open_constr) as (constr) (tactic3)",
563 564 565 566
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun H => iDestructHyp H as pat), "iDestructHyp (constr) as (constr)",
567 568 569
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
570
Tactic failure: iRename: "H" not fresh.
571 572 573 574
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
575
"iPoseProofCore (open_constr) as (constr) (tactic3)" and
576 577
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
578 579 580 581
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
582
"iPoseProofCore (open_constr) as (constr) (tactic3)",
583 584 585 586
"iPoseProofCoreLem (constr) as (tactic3)", "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "tac" (bound to
fun Htmp => spec_tac Htmp; [ .. | tac Htmp ]), "spec_tac" (bound to
fun Htmp =>
587 588 589 590 591 592 593 594 595 596
  lazymatch lem with
  | {| itrm := _; itrm_vars := ?xs; itrm_hyps := ?pat |} => iSpecializeCore
  {| itrm := Htmp; itrm_vars := xs; itrm_hyps := pat |} as p
  | _ => idtac
  end), "iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) as (constr)",
"iSpecializeCore (open_constr) with (open_constr) (open_constr) as (constr)",
"iSpecializePat (open_constr) (constr)" and "iSpecializePat_go", last call
failed.
Tactic failure: iSpecialize: hypotheses ["HQ"] not found.
597 598 599 600 601 602 603 604 605 606
"iPoseProofCoreHyp_not_found_fail"
     : string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "Hx" not found.
"iPoseProofCoreHyp_not_fresh_fail"
     : string
The command has indeed failed with message:
Ltac call to "iPoseProofCoreHyp (constr) as (constr)" failed.
Tactic failure: iPoseProof: "H1" not fresh.
607 608 609 610 611 612 613 614 615 616
"iRevert_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iRevert (constr)", "iElaborateSelPat" and
"<iris.proofmode.ltac_tactics.iElaborateSelPat_go>", last call failed.
Tactic failure: iElaborateSelPat: "H" not found.
"iDestruct_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
617 618 619
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
620 621 622 623
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>", last call failed.
624 625 626 627
Tactic failure: iDestruct: "{HP}"
should contain exactly one proper introduction pattern.
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
628 629 630
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)",
"iDestructCore (open_constr) as (constr) (tactic3)", 
631 632 633 634
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>" and
"<iris.proofmode.ltac_tactics.iDestructHypGo>", last call failed.
635 636
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
637 638 639 640 641 642 643 644
"iOrDestruct_fail"
     : string
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H'" or "H2" not fresh.
The command has indeed failed with message:
Ltac call to "iOrDestruct (constr) as (constr) (constr)" failed.
Tactic failure: iOrDestruct: "H1" or "H'" not fresh.
645 646 647 648
"iApply_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
649
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
650 651
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
652
Tactic failure: iApply: cannot apply P.
653 654 655 656
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
657
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
658 659 660 661 662 663 664 665
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
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:
In nested Ltac calls to "iApply (open_constr)",
666
"iPoseProofCore (open_constr) as (constr) (tactic3)", 
667 668 669 670
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
Tactic failure: iApply: Q
not absorbing and the remaining hypotheses not affine.