Defining GL-split proof systems.

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

Basic components of the GL-split proof system.

inductive Lean4GlCoalgebras.Split.RuleApp : Type

Rule applications for the GL-split proof system.

• 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.Split.T : CategoryTheory.Functor Type Type

Endofunctor for the GL-split proof system.

Equations

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

def Lean4GlCoalgebras.Split.fₚ : RuleApp → SplitSequent

Given a RuleApp, obtain the principal formulas.

Equations

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

def Lean4GlCoalgebras.Split.f : RuleApp → SplitSequent

Given a RuleApp, obtain the split sequent.

Equations

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

def Lean4GlCoalgebras.Split.fₙ : RuleApp → SplitSequent

Given a RuleApp, obtain the non-principal formulas.

Equations

• Lean4GlCoalgebras.Split.fₙ Γ = Lean4GlCoalgebras.Split.f Γ \ Lean4GlCoalgebras.Split.fₚ Γ

theorem Lean4GlCoalgebras.Split.fₙ_alternate (r : RuleApp) : fₙ r = match r with | 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 sequent.

theorem Lean4GlCoalgebras.Split.fₙ_sub_f {r : RuleApp} : fₙ r ⊆ f r

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Get RuleApp of a node (first projection).

Equations

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

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

Get premises of a node (second projection).

Equations

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

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

Edge relation induced by p.

Equations

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

structure Lean4GlCoalgebras.Split.Proof : Type 1

Definition of GL-split 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.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}]

def Lean4GlCoalgebras.Split.Proof.toCoalgebra (𝕏 : Proof) : CategoryTheory.Endofunctor.Coalgebra T

GL-split proofs are coalgebras. Note: we can do this the other way around, i.e. Proof extends CategoryTheory.Endofunctor.Coalgebra T, however I find X and α more explicative than V and str

Equations

• 𝕏.toCoalgebra = { V := 𝕏.X, str := TypeCat.ofHom 𝕏.α }

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

def Lean4GlCoalgebras.Split.«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.Split.«term⊢_» : Lean.ParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.«term⊢_» = Lean.ParserDescr.node `Lean4GlCoalgebras.Split.«term⊢_» 40 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢") (Lean.ParserDescr.cat `term 40))

def Lean4GlCoalgebras.Split.equiv (φ ψ : Formula) : Prop

Auxiliary declaration used in the GL coalgebra development.

Equations

• (φ≅ψ) = ((∃ (𝕏 : Lean4GlCoalgebras.Split.Proof), 𝕏⊢{Sum.inl (~ψ), Sum.inr φ}) ∧ ∃ (𝕏 : Lean4GlCoalgebras.Split.Proof), 𝕏⊢{Sum.inr ψ, Sum.inl (~φ)})

def Lean4GlCoalgebras.Split.«term_≅_» : Lean.TrailingParserDescr

Auxiliary declaration used in the GL coalgebra development.

Equations

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

Fischer-Ladner properties of GL-split proofs

theorem Lean4GlCoalgebras.Split.edge_in_FL {𝕏 : Proof} {x y : 𝕏.X} (x_y : edge 𝕏.α x y) : f (r 𝕏.α y) ⊆ (f (r 𝕏.α x)).FL

Every edge is contained in FL closure.

theorem Lean4GlCoalgebras.Split.path_in_FL {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) : f (r 𝕏.α y) ⊆ (f (r 𝕏.α x)).FL

Every path is contained in FL closure.

Point Generated GL-split Proofs

def Lean4GlCoalgebras.Split.αPoint (𝕐 : Proof) (x : 𝕐.X) : { y : 𝕐.X // Relation.ReflTransGen (edge 𝕐.α) x y } → T.obj { y : 𝕐.X // Relation.ReflTransGen (edge 𝕐.α) x y }

Structure morphism for Point Generation.

Equations

• Lean4GlCoalgebras.Split.αPoint 𝕐 x y = ((𝕐.α ↑y).1, List.pmap (fun (x_1 : 𝕐.X) (y : Relation.ReflTransGen (Lean4GlCoalgebras.Split.edge 𝕐.α) x x_1) => ⟨x_1, y⟩) (𝕐.α ↑y).2 ⋯)

def Lean4GlCoalgebras.Split.pointGeneratedProof (𝕐 : Proof) (x : 𝕐.X) : Proof

Point Generated Split Proof.

Equations

• Lean4GlCoalgebras.Split.pointGeneratedProof 𝕐 x = { X := { y : 𝕐.X // Relation.ReflTransGen (Lean4GlCoalgebras.Split.edge 𝕐.α) x y }, α := Lean4GlCoalgebras.Split.αPoint 𝕐 x, step := ⋯ }

theorem Lean4GlCoalgebras.Split.node_in_pg_sequent_in_FL (𝕏 : Proof) (x : 𝕏.X) (y : (pointGeneratedProof 𝕏 x).X) : f (r (αPoint 𝕏 x) y) ⊆ (f (r 𝕏.α x)).FL

Filtration of GL-Proofs

@[implicit_reducible]

instance Lean4GlCoalgebras.Split.fEqEquiRel (𝕏 : Proof) : Setoid 𝕏.X

Equivalence relation used for Filtration.

Equations

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

noncomputable def Lean4GlCoalgebras.Split.αQuot (𝕐 : Proof) (x : Quotient (fEqEquiRel 𝕐)) : RuleApp × List (Quotient (fEqEquiRel 𝕐))

Structure morphism for Filtration.

Equations

• Lean4GlCoalgebras.Split.αQuot 𝕐 x = ((𝕐.α x.out).1, List.map (Quotient.mk (Lean4GlCoalgebras.Split.fEqEquiRel 𝕐)) (𝕐.α x.out).2)

noncomputable def Lean4GlCoalgebras.Split.filtration (𝕐 : Proof) : Proof

Filtration of a GL-split Proof is a GL-split proof.

Equations

• Lean4GlCoalgebras.Split.filtration 𝕐 = { X := Quotient (Lean4GlCoalgebras.Split.fEqEquiRel 𝕐), α := Lean4GlCoalgebras.Split.αQuot 𝕐, step := ⋯ }

Finite Proof Property

theorem Lean4GlCoalgebras.Split.finite_proof_of_proof (𝕏 : Proof) (Δ : SplitSequent) : (𝕏⊢Δ) → ∃ (𝕐 : Proof), Finite 𝕐.X ∧ (𝕐⊢Δ)

Given a split proof of Δ there exists a finite split proof of Δ.

Properties of (infinite) paths

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

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.nbEdge α x y = (y ∈ Lean4GlCoalgebras.Split.p α x ∧ ¬(Lean4GlCoalgebras.Split.r α x).isBox)

theorem Lean4GlCoalgebras.Split.lt_if_not_box_edge {𝕏 : Proof} {x y : 𝕏.X} (x_y : nbEdge 𝕏.α x y) : (f (r 𝕏.α y)).length < (f (r 𝕏.α x)).length

Non box edges reduce sequent size.

theorem Lean4GlCoalgebras.Split.lt_if_not_box_path {𝕏 : Proof} {x y : 𝕏.X} : Relation.TransGen (nbEdge 𝕏.α) x y → (f (r 𝕏.α y)).length < (f (r 𝕏.α x)).length

Non box paths reduce sequent size.

theorem Lean4GlCoalgebras.Split.no_non_box_loop {𝕏 : Proof} (x : 𝕏.X) : ¬Relation.TransGen (nbEdge 𝕏.α) x x

Non box paths do not loop.

theorem Lean4GlCoalgebras.Split.exists_box_on_le_path {𝕏 : Proof} (x y : 𝕏.X) : Relation.TransGen (edge 𝕏.α) x y → (f (r 𝕏.α x)).length ≤ (f (r 𝕏.α y)).length → ∃ (z : 𝕏.X), Relation.ReflTransGen (edge 𝕏.α) x z ∧ Relation.ReflTransGen (edge 𝕏.α) z y ∧ (r 𝕏.α z).isBox

Every path of increasing size has a box rule application.

theorem Lean4GlCoalgebras.Split.exists_box_on_loop {𝕏 : Proof} (x : 𝕏.X) : Relation.TransGen (edge 𝕏.α) x x → ∃ (z : 𝕏.X), Relation.ReflTransGen (edge 𝕏.α) x z ∧ Relation.ReflTransGen (edge 𝕏.α) z x ∧ (r 𝕏.α z).isBox

Every loop has a box edge.

def Lean4GlCoalgebras.Split.edgeRestr {𝕏 : Proof} (p : 𝕏.X → Prop) : 𝕏.X → 𝕏.X → Prop

Edge relation restricted to nodes satisfying predicate p.

Equations

• Lean4GlCoalgebras.Split.edgeRestr p x y = (Lean4GlCoalgebras.Split.edge 𝕏.α x y ∧ p x ∧ p y)

theorem Lean4GlCoalgebras.Split.exists_box_on_le_restr_path {𝕏 : Proof} (x y : 𝕏.X) (p : 𝕏.X → Prop) : Relation.TransGen (edgeRestr p) x y → (f (r 𝕏.α x)).length ≤ (f (r 𝕏.α y)).length → ∃ (z : 𝕏.X), Relation.ReflTransGen (edgeRestr p) x z ∧ Relation.TransGen (edgeRestr p) z y ∧ (r 𝕏.α z).isBox

Every restricted path of increasing size has a box rule application.

theorem Lean4GlCoalgebras.Split.exists_box_on_restr_loop {𝕏 : Proof} (x : 𝕏.X) (p : 𝕏.X → Prop) : Relation.TransGen (edgeRestr p) x x → ∃ (z : 𝕏.X), (r 𝕏.α z).isBox ∧ p z ∧ Relation.TransGen (edgeRestr p) z z

Every restricted loop has a box edge.

theorem Lean4GlCoalgebras.Split.inf_path_has_inf_boxes {𝕏 : Proof} (g : ℕ → 𝕏.X) (h : ∀ (n : ℕ), edge 𝕏.α (g n) (g (n + 1))) (n : ℕ) : ∃ (m : ℕ), (r 𝕏.α (g (n + m))).isBox

Every infinite path has an infinite number of nodes which are box rule applications.

theorem Lean4GlCoalgebras.Split.finite_and_no_loop_implies_exists_leaf {𝕏 : Proof} [Finite 𝕏.X] (h : 𝕏.X → Prop) (x : 𝕏.X) (x_sat : h x) : (¬∃ (y : 𝕏.X), Relation.TransGen (edgeRestr h) y y) → ∃ (y : 𝕏.X), h y ∧ ∀ z ∈ p 𝕏.α y, ¬h z

If a finite proof has no restricted loops, then there must exist a leaf.

theorem Lean4GlCoalgebras.Split.in_vocab_of_path_left {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) {n : ℕ} (n_in : n ∈ (f (r 𝕏.α y)).left.vocab) : n ∈ (f (r 𝕏.α x)).left.vocab

theorem Lean4GlCoalgebras.Split.in_vocab_of_path_right {𝕏 : Proof} {x y : 𝕏.X} (x_y : Relation.ReflTransGen (edge 𝕏.α) x y) {n : ℕ} (n_in : n ∈ (f (r 𝕏.α y)).right.vocab) : n ∈ (f (r 𝕏.α x)).right.vocab