Iris.ProofMode.Tactics.Split

source

theorem Iris.ProofMode.from_and_intro {PROP : Type u_1} [BI PROP] {P Q A1 A2 : PROP} [inst : FromAnd Q A1 A2] (h1 : P ⊢ A1) (h2 : P ⊢ A2) :

P ⊢ Q

source

def Iris.ProofMode.tacticIsplit :

Lean.ParserDescr

Equations

Iris.ProofMode.tacticIsplit = Lean.ParserDescr.node `Iris.ProofMode.tacticIsplit 1024 (Lean.ParserDescr.nonReservedSymbol "isplit" false)

Instances For

source

theorem Iris.ProofMode.split_es {PROP : Type u_1} [BI PROP] {Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) :

emp ∗ Q ⊣⊢ Q1 ∗ Q2

source

theorem Iris.ProofMode.split_ls {PROP : Type u_1} [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) :

P ∗ Q ⊣⊢ (P ∗ Q1) ∗ Q2

source

theorem Iris.ProofMode.split_rs {PROP : Type u_1} [BI PROP] {P Q Q1 Q2 : PROP} (h : Q ⊣⊢ Q1 ∗ Q2) :

P ∗ Q ⊣⊢ Q1 ∗ P ∗ Q2

source

theorem Iris.ProofMode.split_se {PROP : Type u_1} [BI PROP] {P P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) :

P ∗ emp ⊣⊢ P1 ∗ P2

source

theorem Iris.ProofMode.split_sl {PROP : Type u_1} [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) :

P ∗ Q ⊣⊢ (P1 ∗ Q) ∗ P2

source

theorem Iris.ProofMode.split_sr {PROP : Type u_1} [BI PROP] {P Q P1 P2 : PROP} (h : P ⊣⊢ P1 ∗ P2) :

P ∗ Q ⊣⊢ P1 ∗ P2 ∗ Q

source

theorem Iris.ProofMode.split_ss {PROP : Type u_1} [BI PROP] {P Q P1 P2 Q1 Q2 : PROP} (h1 : P ⊣⊢ P1 ∗ P2) (h2 : Q ⊣⊢ Q1 ∗ Q2) :

P ∗ Q ⊣⊢ (P1 ∗ Q1) ∗ P2 ∗ Q2

source

inductive Iris.ProofMode.SplitResult {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (e : Q(«$prop»)) :

Type

emp {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} : «$e» =Q iprop(emp) → SplitResult bi e
left {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} : SplitResult bi e
right {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e : Q(«$prop»)} : SplitResult bi e
split {u : Lean.Level} {prop : Q(Type u)} {bi : Q(BI «$prop»)} {e elhs erhs : Q(«$prop»)} (lhs : Hyps bi elhs) (rhs : Hyps bi erhs) (pf : Q(«$e» ⊣⊢ «$elhs» ∗ «$erhs»)) : SplitResult bi e

Instances For

source

def Iris.ProofMode.Hyps.splitCore {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (toRight : Lean.Name → Lean.Name → Bool) {e : Q(«$prop»)} :

Hyps bi e → SplitResult bi e

Equations

One or more equations did not get rendered due to their size.
Iris.ProofMode.Hyps.splitCore bi toRight (Iris.ProofMode.Hyps.emp x_3) = Iris.ProofMode.SplitResult.emp ⋯

Instances For

source

def Iris.ProofMode.Hyps.split {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) (toRight : Lean.Name → Lean.Name → Bool) {e : Q(«$prop»)} (hyps : Hyps bi e) :

(elhs : Q(«$prop»)) × (erhs : Q(«$prop»)) × Hyps bi elhs × Hyps bi erhs × Q(«$e» ⊣⊢ «$elhs» ∗ «$erhs»)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Iris.ProofMode.sep_split {PROP : Type u_1} [BI PROP] {P P1 P2 Q Q1 Q2 : PROP} [inst : FromSep Q Q1 Q2] (h : P ⊣⊢ P1 ∗ P2) (h1 : P1 ⊢ Q1) (h2 : P2 ⊢ Q2) :

P ⊢ Q

source

def Lean.Parser.Category.splitSide :