The GL-split game.

Builder-Prover game for constructive counter-models/proofs. Builder gets a rule application R and plays an applicable sequent Γ in order to construct a counter-model. Prover get a sequent Γ and plays rule applications R in order to construct a proof.

@[reducible, inline]

abbrev Lean4GlCoalgebras.Split.Builder : Player

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.Builder = Lean4GlCoalgebras.Player.A

@[reducible, inline]

abbrev Lean4GlCoalgebras.Split.Prover : Player

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.Prover = Lean4GlCoalgebras.Player.B

def Lean4GlCoalgebras.Split.SplitSequent.ruleApps (Γ : SplitSequent) : Finset RuleApp

The available rule applications for a sequent Γ.

Equations

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

def Lean4GlCoalgebras.Split.RuleApp.splitSequents (R : RuleApp) : Finset SplitSequent

The sequents possible after a rule application R.

Equations

• (Lean4GlCoalgebras.Split.RuleApp.topₗ Δ a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.topᵣ Δ a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.axₗₗ Δ n a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.axₗᵣ Δ n a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.axᵣₗ Δ n a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.axᵣᵣ Δ n a).splitSequents = ∅
• (Lean4GlCoalgebras.Split.RuleApp.andₗ Δ A B a).splitSequents = {Δ \ {Sum.inl (A&B)} ∪ {Sum.inl A}, Δ \ {Sum.inl (A&B)} ∪ {Sum.inl B}}
• (Lean4GlCoalgebras.Split.RuleApp.andᵣ Δ A B a).splitSequents = {Δ \ {Sum.inr (A&B)} ∪ {Sum.inr A}, Δ \ {Sum.inr (A&B)} ∪ {Sum.inr B}}
• (Lean4GlCoalgebras.Split.RuleApp.orₗ Δ A B a).splitSequents = {Δ \ {Sum.inl (A v B)} ∪ {Sum.inl A, Sum.inl B}}
• (Lean4GlCoalgebras.Split.RuleApp.orᵣ Δ A B a).splitSequents = {Δ \ {Sum.inr (A v B)} ∪ {Sum.inr A, Sum.inr B}}
• (Lean4GlCoalgebras.Split.RuleApp.boxₗ Δ A a).splitSequents = {(Δ \ {Sum.inl (□A)}).D ∪ {Sum.inl A}}
• (Lean4GlCoalgebras.Split.RuleApp.boxᵣ Δ A a).splitSequents = {(Δ \ {Sum.inr (□A)}).D ∪ {Sum.inr A}}

@[reducible, inline]

abbrev Lean4GlCoalgebras.Split.GamePos : Type

Note: the game stores the history of which rule applications have come prior.

Equations

• Lean4GlCoalgebras.Split.GamePos = ((Lean4GlCoalgebras.SplitSequent ⊕ Lean4GlCoalgebras.Split.RuleApp) × List Lean4GlCoalgebras.SplitSequent × List Lean4GlCoalgebras.Split.RuleApp)

inductive Lean4GlCoalgebras.Split.Move : GamePos → GamePos → Prop

Auxiliary declaration used in the GL coalgebra development.

• prover {R : RuleApp} {Rs : List RuleApp} {Γ : SplitSequent} {Γs : List SplitSequent} : R ∈ SplitSequent.ruleApps Γ → Move (Sum.inl Γ, Γs, Rs) (Sum.inr R, Γ :: Γs, Rs)
• builder {R : RuleApp} {Rs : List RuleApp} {Γ : SplitSequent} {Γs : List SplitSequent} : Γ ∈ R.splitSequents → Γ ∉ Γs → Move (Sum.inr R, Γs, Rs) (Sum.inl Γ, Γs, R :: Rs)

theorem Lean4GlCoalgebras.Split.move_move_in_FL {g1 g2 : GamePos} (h1 : g1.1.isLeft = true) (h3 : g2.1.isLeft = true) (g1_g2 : Relation.ReflTransGen (Relation.Comp Move Move) g1 g2) : g2.1.getLeft h3 ∈ Finset.powerset (g1.1.getLeft h1).FL

Given two consecutive Prover moves, the latter move is in the FL closure of the prior.

theorem Lean4GlCoalgebras.Split.no_inf_chain_from_prover (g : ℕ → GamePos) (g_rel : ∀ (n : ℕ), Function.swap Move (g (n + 1)) (g n)) (h : (g 0).1.isLeft = true) : False

theorem Lean4GlCoalgebras.Split.matches_finite : WellFounded (Function.swap Move)

The game is converse well-founded.

@[reducible]

def Lean4GlCoalgebras.Split.coalgebraGame : Game

Auxiliary declaration used in the GL coalgebra development.

Equations

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

theorem Lean4GlCoalgebras.Split.move_iff_in_moves {g g' : Game.Pos} : Move g g' ↔ g' ∈ Game.moves g

Move relation and being in the set of game moves are equivalent.

@[reducible, inline]

abbrev Lean4GlCoalgebras.Split.startPos (Γ : SplitSequent) : GamePos

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.startPos Γ = (Sum.inl Γ, [], [])