proofmode_monpred.ref 2 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
1 subgoal
  
  I : biIndex
  Σ : gFunctors
  invG0 : invG Σ
  N : namespace
71
  𝓟 : iProp Σ
72
  ============================
73 74
  "H" : ⎡ inv N (<pers> 𝓟) ⎤
  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
75
  --------------------------------------□
76
  |={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
77 78 79 80 81 82 83
  
1 subgoal
  
  I : biIndex
  Σ : gFunctors
  invG0 : invG Σ
  N : namespace
84
  𝓟 : iProp Σ
85
  ============================
86 87
  "H" : ⎡ inv N (<pers> 𝓟) ⎤
  "H2" : ⎡ ▷ <pers> 𝓟 ⎤
88
  --------------------------------------□
89
  "Hclose" : ⎡ ▷ <pers> 𝓟 ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
90
  --------------------------------------∗
91
  |={⊤ ∖ ↑N,⊤}=> ⎡ ▷ 𝓟 ⎤
92