GL.Split.ProofTransformations

Defining GL-ext+pre proof system. #

Here we define the GL-ext+pre system. This system is different from the paper, where we build in how we connect non-axiomatic leaf nodes into RuleApp directly.

source

inductive Ext.RuleApp {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :

Type

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

pre {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (y : 𝕏.X) : y ∈ Split.p 𝕏.α x → RuleApp x τ
cutₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : RuleApp x τ
cutᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : RuleApp x τ
wkₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : Sum.inl A ∈ Δ → RuleApp x τ
wkᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : Sum.inr A ∈ Δ → RuleApp x τ
topₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) : Sum.inl ⊤ ∈ Δ → RuleApp x τ
topᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) : Sum.inr ⊤ ∈ Δ → RuleApp x τ
axₗₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp x τ
axₗᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (n : ℕ) : Sum.inl (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp x τ
axᵣₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ → RuleApp x τ
axᵣᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (n : ℕ) : Sum.inr (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ → RuleApp x τ
andₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A B : Formula) : Sum.inl (A&B) ∈ Δ → RuleApp x τ
andᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A B : Formula) : Sum.inr (A&B) ∈ Δ → RuleApp x τ
orₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A B : Formula) : Sum.inl (A v B) ∈ Δ → RuleApp x τ
orᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A B : Formula) : Sum.inr (A v B) ∈ Δ → RuleApp x τ
boxₗ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : Sum.inl (□A) ∈ Δ → RuleApp x τ
boxᵣ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (Δ : SplitSequent) (A : Formula) : Sum.inr (□A) ∈ Δ → RuleApp x τ

Instances For

source

def Ext.fₚ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :

RuleApp x τ → SplitSequent

Given a RuleApp, obtain the principal formulas.

Equations

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

Instances For

source

def Ext.f {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :

RuleApp x τ → SplitSequent

Given a RuleApp, obtain the split sequent.

Equations

Instances For

source

def Ext.fₙ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :

RuleApp x τ → SplitSequent

Given a RuleApp, obtain the non-principal formulas.

Equations

Ext.fₙ r = Ext.f r \ Ext.fₚ r

Instances For

source

theorem Ext.fₙ_alternate {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : RuleApp x τ) :

fₙ r = match r with | RuleApp.pre y a => τ y | 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.

source

def Ext.T {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :

CategoryTheory.Functor Type Type

Equations

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

Instances For

source

def Ext.r {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :

X → RuleApp x τ

Get RuleApp of a node (first projection).

Equations

Ext.r α x = (α x).1

Instances For

source

def Ext.p {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :

X → List X

Get premises of a node (second projection).

Equations

Ext.p α x = (α x).2

Instances For

source

def Ext.edge {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :

X → (y : X) → Prop

Edge relation induced by p.

Equations

Ext.edge α x y = (y ∈ Ext.p α x)

Instances For

source

def Ext.RuleApp.isBox {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :

RuleApp x τ → Prop

Equations

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

Instances For

source

def Ext.RuleApp.isNonAxLeaf {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :

RuleApp x τ → Prop

Equations

(Ext.RuleApp.pre y a).isNonAxLeaf = (true = true)
x✝.isNonAxLeaf = (false = true)

Instances For

source

structure Ext.PreProof {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :

Type 1

X : Type
α : self.X → (T x τ).obj self.X
root : self.X
step (x : self.X) : match r self.α x with | RuleApp.pre y a => p self.α x = [] | RuleApp.cutₗ Δ A => List.map (fun (x_1 : self.X) => f (r self.α x_1)) (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_1 : self.X) => f (r self.α x_1)) (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_1 : self.X) => f (r self.α x_1)) (p self.α x) = [fₙ (r self.α x)] | RuleApp.wkᵣ Δ A a => List.map (fun (x_1 : self.X) => f (r self.α x_1)) (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_1 : self.X) => f (r self.α x_1)) (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_1 : self.X) => f (r self.α x_1)) (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_1 : self.X) => f (r self.α x_1)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inl A, Sum.inl B}] | RuleApp.orᵣ Δ A B a => List.map (fun (x_1 : self.X) => f (r self.α x_1)) (p self.α x) = [fₙ (r self.α x) ∪ {Sum.inr A, Sum.inr B}] | RuleApp.boxₗ Δ A a => List.map (fun (x_1 : self.X) => f (r self.α x_1)) (p self.α x) = [(fₙ (r self.α x)).D ∪ {Sum.inl A}] | RuleApp.boxᵣ Δ A a => List.map (fun (x_1 : self.X) => f (r self.α x_1)) (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

Instances For

source

def Ext.Proves {𝕏 : Split.Proof} (x : 𝕏.X) {σ : 𝕏.X → SplitSequent} (𝕐 : PreProof x σ) (Δ : SplitSequent) :

Prop

Equations

Ext.Proves x 𝕐 Δ = (Ext.f (Ext.r 𝕐.α 𝕐.root) = Δ)

Instances For

source

def proofTransformationMap {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) :

(y : 𝕏.X) × (partialProof y).X → ExtSkip.T.obj ((y : 𝕏.X) × (partialProof y).X)

Structure morphism of a proof transformation!

Equations

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

Instances For

source

@[simp]

theorem proofTransformation_f {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :

ExtSkip.f (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.f (Ext.r (partialProof y).α z_in_Cy)

source

@[simp]

theorem proofTransformation_fₚ {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :

ExtSkip.fₚ (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.fₚ (Ext.r (partialProof y).α z_in_Cy)

source

@[simp]

theorem proofTransformation_fₙ {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :

ExtSkip.fₙ (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.fₙ (Ext.r (partialProof y).α z_in_Cy)

source

theorem proofTransformation_isBox {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (z_in_Cy : (y : 𝕏.X) × (partialProof y).X) :

(ExtSkip.r (proofTransformationMap partialProof) z_in_Cy).isBox ↔ (Ext.r (partialProof z_in_Cy.fst).α z_in_Cy.snd).isBox

source

noncomputable def dep_sum_seq_proj {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) :

ℕ → α × ℕ

Equations

dep_sum_seq_proj h 0 = ((f (Nat.find ⋯ + 1)).fst, Nat.find ⋯ + 1)
dep_sum_seq_proj h n.succ = ((f (Nat.find ⋯ + 1)).fst, Nat.find ⋯ + 1)

Instances For

source

theorem infinite_dep_sum_sequence_proj_eq {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n : ℕ) :

(f (dep_sum_seq_proj h n).2).fst = (dep_sum_seq_proj h n).1

source

theorem dep_sum_seq_proj_leq {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n : ℕ) :

n ≤ (dep_sum_seq_proj h n).2

source

theorem fst_same_in_range {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n m : ℕ) :

n ≤ Nat.find ⋯ → n ≥ (dep_sum_seq_proj h m).2 → (f (dep_sum_seq_proj h m).2).fst = (f n).fst

source

theorem infinite_dep_sum_chain {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {R : α → α → Prop} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (f_chain : ∀ (n : ℕ), Sigma.Lex R Q (f n) (f (n + 1))) (n : ℕ) :

R (dep_sum_seq_proj h n).1 (dep_sum_seq_proj h (n + 1)).1

source

noncomputable def infinite_dep_sum_chain_finite_subchain {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (m : ℕ) :

Fin (Nat.find ⋯ - (dep_sum_seq_proj h m).2 + 1) → β (dep_sum_seq_proj h m).1

Equations

infinite_dep_sum_chain_finite_subchain h m ⟨n, n_prop⟩ = ⋯ ▸ (f ((dep_sum_seq_proj h m).2 + n)).snd

Instances For

source

theorem infinite_dep_sum_chain_finite_subchain_prop {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (m : ℕ) (k : Fin (Nat.find ⋯ - (dep_sum_seq_proj h m).2)) :

Q (dep_sum_seq_proj h m).1 (infinite_dep_sum_chain_finite_subchain h m k.castSucc) (infinite_dep_sum_chain_finite_subchain h m k.succ)

source

theorem infinite_dep_sum_chain_inf {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (p : α → Prop) (q : (a : α) × β a → Prop) (inf : ∀ (n : ℕ), ∃ (m : ℕ), p (dep_sum_seq_proj h (n + m)).1) (conv : ∀ (n : ℕ), p (dep_sum_seq_proj h n).1 → ∃ (m : ℕ), q (f ((dep_sum_seq_proj h n).2 + m))) (n : ℕ) :

∃ (m : ℕ), q (f (n + m))

source

noncomputable def proofTransformation {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (root_prop : ∀ (x : 𝕏.X), Ext.Proves x (partialProof x) (σ x)) (box_prop : ∀ (x : 𝕏.X), (Split.r 𝕏.α x).isBox → ∀ (n : ℕ) (f : Fin (n + 1) → (partialProof x).X), f 0 = (partialProof x).root → (Ext.r (partialProof x).α (f ⟨n, ⋯⟩)).isNonAxLeaf → (∀ (m : Fin n), Ext.edge (partialProof x).α (f m.castSucc) (f m.succ)) → ∃ (m : Fin (n + 1)), (Ext.r (partialProof x).α (f m)).isBox) :

ExtSkip.Proof

Provides the Proof Transformation and proves it is a proof if it satisfies box_prop and root_prop.

Equations

proofTransformation partialProof root_prop box_prop = { X := (y : 𝕏.X) × (partialProof y).X, α := proofTransformationMap partialProof, step := ⋯, path := ⋯ }

Instances For