proofmode.ref 20.3 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
"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
Ralf Jung's avatar
Ralf Jung committed
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
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
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
  
Robbert Krebbers's avatar
Robbert Krebbers committed
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⌝
  
Dan Frumin's avatar
Dan Frumin committed
125 126 127 128 129 130 131
"test_iSimpl_in4"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iSimpl in (constr)",
"iEval (tactic) in (constr)" and "<iris.proofmode.ltac_tactics.iEval_go>",
last call failed.
Tactic failure: iEval: %: unsupported selection pattern.
Ralf Jung's avatar
Ralf Jung committed
132 133
"test_iFrame_later_1"
     : string
134 135 136 137 138 139 140 141
1 subgoal
  
  PROP : sbi
  P, Q : PROP
  ============================
  --------------------------------------∗
  ▷ emp
  
Ralf Jung's avatar
Ralf Jung committed
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.
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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)
  
Robbert Krebbers's avatar
Robbert Krebbers committed
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)
  
Ralf Jung's avatar
Ralf Jung committed
227 228
"test_big_sepL2_iDestruct"
     : string
Robbert Krebbers's avatar
Robbert Krebbers committed
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
  
Ralf Jung's avatar
Ralf Jung committed
241 242
"test_reducing_after_iDestruct"
     : string
243 244 245 246 247 248 249 250
1 subgoal
  
  PROP : sbi
  ============================
  "H" : □ True
  --------------------------------------∗
  True
  
Ralf Jung's avatar
Ralf Jung committed
251 252
"test_reducing_after_iApply"
     : string
253 254 255 256 257 258 259 260
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
261 262
"test_reducing_after_iApply_late_evar"
     : string
263 264 265 266 267 268 269 270
1 subgoal
  
  PROP : sbi
  ============================
  "H" : emp
  --------------------------------------□
  □ emp
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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
  
Ralf Jung's avatar
Ralf Jung committed
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 446 447
The command has indeed failed with message:
In nested Ltac calls to "iDestruct (open_constr) as (constr)",
"iDestructCore (open_constr) as (constr) (tactic)" and
"iDestructCore (open_constr) as (constr) (tactic)", 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 556
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
Robbert Krebbers's avatar
Robbert Krebbers committed
557
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)" 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)",
Robbert Krebbers's avatar
Robbert Krebbers committed
562 563 564
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
565
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
566 567 568 569 570
"tac" (bound to fun H => iDestructHyp H as pat),
"iDestructHyp (constr) as (constr)",
"<iris.proofmode.ltac_tactics.iDestructHypFindPat>",
"<iris.proofmode.ltac_tactics.iDestructHypGo>" and
"iRename (constr) into (constr)", last call failed.
571
Tactic failure: iRename: "H" not fresh.
572 573 574 575 576 577 578
"iPoseProof_not_found_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)" and
"iPoseProofCoreHyp (constr) as (constr)", last call failed.
Tactic failure: iPoseProof: "Hx" not found.
579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598
"iPoseProof_not_found_fail2"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iPoseProof (open_constr) as (constr)",
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)",
"iPoseProofCoreLem (constr) as (constr) before_tc (tactic)", 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
"tac" (bound to spec_tac ltac:(()); [ .. | tac Htmp ]), 
"spec_tac" (bound to
fun _ =>
  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.
599 600 601 602 603 604 605 606 607 608
"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.
609 610 611 612 613 614 615 616 617 618 619
"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)",
"iDestructCore (open_constr) as (constr) (tactic)",
620 621 622 623 624 625
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", 
"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.
626 627 628 629 630
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)",
"iDestructCore (open_constr) as (constr) (tactic)",
631 632 633 634 635 636
"iDestructCore (open_constr) as (constr) (tactic)",
"iDestructCore (open_constr) as (constr) (tactic)", 
"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.
637 638
Tactic failure: iDestruct: (IList [[IClear (sel_patterns.SelIdent "HP")]])
invalid.
639 640 641 642 643 644 645 646
"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.
647 648 649 650
"iApply_fail"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
651
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
652 653
"tac" (bound to fun H => iApplyHyp H) and "iApplyHyp (constr)", last call
failed.
654
Tactic failure: iApply: cannot apply P.
655 656 657 658
"iApply_fail_not_affine_1"
     : string
The command has indeed failed with message:
In nested Ltac calls to "iApply (open_constr)",
Robbert Krebbers's avatar
Robbert Krebbers committed
659
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
660 661 662 663 664 665 666 667
"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)",
Robbert Krebbers's avatar
Robbert Krebbers committed
668
"iPoseProofCore (open_constr) as (constr) (constr) (tactic)", 
669 670 671 672
"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.