@[reducible, inline]

abbrev Split.Builder : Player

Equations

• Split.Builder = Player.A

@[reducible, inline]

abbrev Split.Prover : Player

Equations

• Split.Prover = Player.B

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.

def 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 Split.RuleApp.splitSequents (R : RuleApp) : Finset SplitSequent

The sequents possible after a rule application R.

Equations

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

@[reducible, inline]

abbrev Split.GamePos : Type

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

Equations

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

inductive Split.Move : GamePos → GamePos → Prop

• 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 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 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 Split.matches_finite : WellFounded (Function.swap Move)

The game is converse well-founded.

def Split.coalgebraGame : Game

Equations

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

theorem 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 Split.startPos (Γ : SplitSequent) : GamePos

Equations

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