Defining GL-ext+skip proof systems.

Here we define the GL-ext proof system along with finitization and basic properties. We use the namespace ExtSkip to distinguish from our general GL-proofs.

Basic components of the GL-ext+skip proof system.

inductive Lean4GlCoalgebras.ExtSkip.RuleApp : Type

Rule applications for the GL-ext+skip proof system.

• skp (Δ : SplitSequent) : RuleApp
• cutₗ (Δ : SplitSequent) (A : Formula) : RuleApp
• cutᵣ (Δ : SplitSequent) (A : Formula) : RuleApp
• wkₗ (Δ : SplitSequent) (A : Formula) : Sum.inl A ∈ Δ → RuleApp
• wkᵣ (Δ : SplitSequent) (A : Formula) : Sum.inr A ∈ Δ → RuleApp
• topₗ (Δ : SplitSequent) : Sum.inl ⊤ ∈ Δ → RuleApp
• topᵣ (Δ : SplitSequent) : Sum.inr ⊤ ∈ Δ → RuleApp
• axₗₗ (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp
• axₗᵣ (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp
• axᵣₗ (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp
• axᵣᵣ (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp
• andₗ (Δ : SplitSequent) (A B : Formula) : Sum.inl (A&B) ∈ Δ → RuleApp
• andᵣ (Δ : SplitSequent) (A B : Formula) : Sum.inr (A&B) ∈ Δ → RuleApp
• orₗ (Δ : SplitSequent) (A B : Formula) : Sum.inl (A v B) ∈ Δ → RuleApp
• orᵣ (Δ : SplitSequent) (A B : Formula) : Sum.inr (A v B) ∈ Δ → RuleApp
• boxₗ (Δ : SplitSequent) (A : Formula) : Sum.inl (□A) ∈ Δ → RuleApp
• boxᵣ (Δ : SplitSequent) (A : Formula) : Sum.inr (□A) ∈ Δ → RuleApp

def Lean4GlCoalgebras.ExtSkip.T : CategoryTheory.Functor Type Type

Endofunctor for the GL-ext+skip proof system.

Equations

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

def Lean4GlCoalgebras.ExtSkip.fₚ : RuleApp → SplitSequent

Given a RuleApp, obtain the principal formulas.

Equations

• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.skp Δ) = ∅
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.cutₗ Δ A) = ∅
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.cutᵣ Δ A) = ∅
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.wkₗ Δ A a) = {Sum.inl A}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.wkᵣ Δ A a) = {Sum.inr A}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.topₗ Δ a) = {Sum.inl ⊤}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.topᵣ Δ a) = {Sum.inr ⊤}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.axₗₗ Δ n a) = {Sum.inl (at n), Sum.inl (na n)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.axₗᵣ Δ n a) = {Sum.inl (at n), Sum.inr (na n)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.axᵣₗ Δ n a) = {Sum.inr (at n), Sum.inl (na n)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.axᵣᵣ Δ n a) = {Sum.inr (at n), Sum.inr (na n)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.andₗ Δ A B a) = {Sum.inl (A&B)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.andᵣ Δ A B a) = {Sum.inr (A&B)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.orₗ Δ A B a) = {Sum.inl (A v B)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.orᵣ Δ A B a) = {Sum.inr (A v B)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.boxₗ Δ A a) = {Sum.inl (□A)}
• Lean4GlCoalgebras.ExtSkip.fₚ (Lean4GlCoalgebras.ExtSkip.RuleApp.boxᵣ Δ A a) = {Sum.inr (□A)}

def Lean4GlCoalgebras.ExtSkip.f : RuleApp → SplitSequent

Given a RuleApp, obtain the split sequent.

Equations

• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.skp Δ) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.cutₗ Δ A) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.cutᵣ Δ A) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.wkₗ Δ A a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.wkᵣ Δ A a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.topₗ Δ a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.topᵣ Δ a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.axₗₗ Δ n a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.axₗᵣ Δ n a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.axᵣₗ Δ n a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.axᵣᵣ Δ n a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.andₗ Δ A B a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.andᵣ Δ A B a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.orₗ Δ A B a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.orᵣ Δ A B a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.boxₗ Δ A a) = Δ
• Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.RuleApp.boxᵣ Δ A a) = Δ

def Lean4GlCoalgebras.ExtSkip.fₙ : RuleApp → SplitSequent

Given a RuleApp, obtain the non-principal formulas.

Equations

• Lean4GlCoalgebras.ExtSkip.fₙ r = Lean4GlCoalgebras.ExtSkip.f r \ Lean4GlCoalgebras.ExtSkip.fₚ r

theorem Lean4GlCoalgebras.ExtSkip.fₙ_alternate (r : RuleApp) : fₙ r = match r with | RuleApp.skp Δ => Δ | RuleApp.cutₗ Δ A => Δ | RuleApp.cutᵣ Δ A => Δ | RuleApp.wkₗ Δ A a => Δ \ {Sum.inl A} | RuleApp.wkᵣ Δ A a => Δ \ {Sum.inr A} | RuleApp.topₗ Δ a => Δ \ {Sum.inl ⊤} | RuleApp.topᵣ Δ a => Δ \ {Sum.inr ⊤} | RuleApp.axₗₗ Δ n a => Δ \ {Sum.inl (at n), Sum.inl (na n)} | RuleApp.axₗᵣ Δ n a => Δ \ {Sum.inl (at n), Sum.inr (na n)} | RuleApp.axᵣₗ Δ n a => Δ \ {Sum.inr (at n), Sum.inl (na n)} | RuleApp.axᵣᵣ Δ n a => Δ \ {Sum.inr (at n), Sum.inr (na n)} | RuleApp.andₗ Δ A B a => Δ \ {Sum.inl (A&B)} | RuleApp.andᵣ Δ A B a => Δ \ {Sum.inr (A&B)} | RuleApp.orₗ Δ A B a => Δ \ {Sum.inl (A v B)} | RuleApp.orᵣ Δ A B a => Δ \ {Sum.inr (A v B)} | RuleApp.boxₗ Δ A a => Δ \ {Sum.inl (□A)} | RuleApp.boxᵣ Δ A a => Δ \ {Sum.inr (□A)}

Relating principal formulas, non-principal formulas, and the split sequent.

def Lean4GlCoalgebras.ExtSkip.RuleApp.isBox : RuleApp → Prop

Auxiliary declaration used in the GL coalgebra development.

Equations

• (Lean4GlCoalgebras.ExtSkip.RuleApp.boxₗ Δ A a).isBox = (true = true)
• (Lean4GlCoalgebras.ExtSkip.RuleApp.boxᵣ Δ A a).isBox = (true = true)
• x✝.isBox = (false = true)

def Lean4GlCoalgebras.ExtSkip.r {X : Type} (α : X → T.obj X) (x : X) : RuleApp

Get RuleApp of a node (first projection).

Equations

• Lean4GlCoalgebras.ExtSkip.r α x = (α x).1

def Lean4GlCoalgebras.ExtSkip.p {X : Type} (α : X → T.obj X) (x : X) : List X

Get premises of a node (second projection).

Equations

• Lean4GlCoalgebras.ExtSkip.p α x = (α x).2

def Lean4GlCoalgebras.ExtSkip.edge {X : Type} (α : X → T.obj X) (x y : X) : Prop

Edge relation induced by p.

Equations

• Lean4GlCoalgebras.ExtSkip.edge α x y = (y ∈ Lean4GlCoalgebras.ExtSkip.p α x)

structure Lean4GlCoalgebras.ExtSkip.Proof : Type 1

Definition of GL-ext+skip proof.

• X : Type

  Auxiliary declaration used in the GL coalgebra development.

• α : self.X → T.obj self.X

  Auxiliary declaration used in the GL coalgebra development.

• step (x : self.X) : match r self.α x with | RuleApp.skp Δ => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [f (r self.α x)] | RuleApp.cutₗ Δ A => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).filterRight ∪ {Sum.inl A}, (fₙ (r self.α x)).filterLeft ∪ {Sum.inr (~A)}] | RuleApp.cutᵣ Δ A => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).filterLeft ∪ {Sum.inr A}, (fₙ (r self.α x)).filterRight ∪ {Sum.inl (~A)}] | RuleApp.wkₗ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x)] | RuleApp.wkᵣ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x)] | RuleApp.topₗ Δ a => p self.α x = ∅ | RuleApp.topᵣ Δ a => p self.α x = ∅ | RuleApp.axₗₗ Δ n a => p self.α x = ∅ | RuleApp.axₗᵣ Δ n a => p self.α x = ∅ | RuleApp.axᵣₗ Δ n a => p self.α x = ∅ | RuleApp.axᵣᵣ Δ n a => p self.α x = ∅ | RuleApp.andₗ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inl A}, fₙ (r self.α x) ∪ {Sum.inl B}] | RuleApp.andᵣ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inr A}, fₙ (r self.α x) ∪ {Sum.inr B}] | RuleApp.orₗ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inl A, Sum.inl B}] | RuleApp.orᵣ Δ A B a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inr A, Sum.inr B}] | RuleApp.boxₗ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {Sum.inl A}] | RuleApp.boxᵣ Δ A a => List.map (fun (x : self.X) => f (r self.α x)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {Sum.inr A}]
• path (x : self.X) (f : { f : ℕ → self.X // f 0 = x ∧ ∀ (n : ℕ), edge self.α (f n) (f (n + 1)) }) (n : ℕ) : ∃ (m : ℕ), (r self.α (↑f (n + m))).isBox

def Lean4GlCoalgebras.ExtSkip.proves (𝕏 : Proof) (Δ : SplitSequent) : Prop

Auxiliary declaration used in the GL coalgebra development.

Equations

• (𝕏⊢Δ) = ∃ (x : 𝕏.X), Lean4GlCoalgebras.ExtSkip.f (Lean4GlCoalgebras.ExtSkip.r 𝕏.α x) = Δ

def Lean4GlCoalgebras.ExtSkip.SplitSequent.isTrue (Δ : SplitSequent) : Prop

Auxiliary declaration used in the GL coalgebra development.

Equations

• (⊢Δ) = ∃ (𝕏 : Lean4GlCoalgebras.ExtSkip.Proof), 𝕏⊢Δ

def Lean4GlCoalgebras.ExtSkip.«term_⊢_» : Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

def Lean4GlCoalgebras.ExtSkip.«term⊢_» : Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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