The GL-proof 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.Builder : Player

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Builder = Lean4GlCoalgebras.Player.A

@[reducible, inline]

abbrev Lean4GlCoalgebras.Prover : Player

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Prover = Lean4GlCoalgebras.Player.B

def Lean4GlCoalgebras.Sequent.ruleApps (Γ : Sequent) : Finset RuleApp

The available rule applications for a sequent Γ.

Equations

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

def Lean4GlCoalgebras.RuleApp.sequents (R : RuleApp) : Finset Sequent

The sequents possible after a rule application R.

Equations

• (Lean4GlCoalgebras.RuleApp.top Δ a).sequents = ∅
• (Lean4GlCoalgebras.RuleApp.ax Δ n a).sequents = ∅
• (Lean4GlCoalgebras.RuleApp.and Δ φ ψ a).sequents = {Δ \ {φ&ψ} ∪ {φ}, Δ \ {φ&ψ} ∪ {ψ}}
• (Lean4GlCoalgebras.RuleApp.or Δ φ ψ a).sequents = {Δ \ {φ v ψ} ∪ {φ, ψ}}
• (Lean4GlCoalgebras.RuleApp.box Δ φ a).sequents = {(Δ \ {□φ}).D ∪ {φ}}

@[reducible, inline]

abbrev Lean4GlCoalgebras.GamePos : Type

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

Equations

• Lean4GlCoalgebras.GamePos = ((Lean4GlCoalgebras.Sequent ⊕ Lean4GlCoalgebras.RuleApp) × List Lean4GlCoalgebras.Sequent × List Lean4GlCoalgebras.RuleApp)

inductive Lean4GlCoalgebras.Move : GamePos → GamePos → Prop

Auxiliary declaration used in the GL coalgebra development.

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

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

The game is converse well-founded.

@[reducible]

def Lean4GlCoalgebras.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.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.startPos (Γ : Sequent) : GamePos

We will always start the game from a sequent Γ and no history.

Equations

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