proofmode_monpred.ref 1.97 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  i : I
  ============================
  "HW" : (P -∗ Q) i
  --------------------------------------∗
  (P -∗ Q) i
  
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  i, j : I
  ============================
  "HW" : (P -∗ Q) j
  "HP" : P j
  --------------------------------------∗
  Q j
  
1 subgoal
  
  I : biIndex
  PROP : sbi
  P, Q : monpred.monPred I PROP
  Objective0 : Objective Q
  𝓟, 𝓠 : PROP
  ============================
  "H2" : ∀ i : I, Q i
  "H3" : 𝓟
  "H4" : 𝓠
  --------------------------------------∗
  ∀ i : I, 𝓟 ∗ 𝓠 ∗ Q i
  
38 39 40 41 42 43 44 45 46 47 48
1 subgoal
  
  I : biIndex
  PROP : sbi
  FU0 : BiFUpd PROP * ()
  P, Q : monpred.monPred I PROP
  i : I
  ============================
  --------------------------------------∗
  (Q -∗ emp) i
  
49 50 51 52 53 54 55 56 57 58 59
1 subgoal
  
  I : biIndex
  PROP : sbi
  FU0 : BiFUpd PROP * ()
  P : monpred.monPred I PROP
  i : I
  ============================
  --------------------------------------∗
  ∀ _ : (), ∃ _ : (), emp
  
60 61 62 63 64
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 (P i).
65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92
1 subgoal
  
  I : biIndex
  Σ : gFunctors
  invG0 : invG Σ
  N : namespace
  P : iProp Σ
  ============================
  "H" : ⎡ inv N (<pers> P) ⎤
  "H2" : ⎡ ▷ <pers> P ⎤
  --------------------------------------□
  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
  
1 subgoal
  
  I : biIndex
  Σ : gFunctors
  invG0 : invG Σ
  N : namespace
  P : iProp Σ
  ============================
  "H" : ⎡ inv N (<pers> P) ⎤
  "H2" : ⎡ ▷ <pers> P ⎤
  --------------------------------------□
  "Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
  --------------------------------------∗
  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤