Prover winning the GL-game builds a GL-proof.

If Prover has a winning strategy in the game starting from Γ, then there is a proof of Γ, proven in prover_win_builds_proof, all other definitions and proofs in this file are helpers.

def Lean4GlCoalgebras.rewindHistoryOneStep (g : Game.Pos) (h : Game.turn g = Prover ∧ g.2.2 ≠ ∅ ∨ Game.turn g = Builder ∧ g.2.1 ≠ ∅) : Game.Pos

Rewinding the history one step to get previous move.

Equations

• Lean4GlCoalgebras.rewindHistoryOneStep (Sum.inl Γ, Γs, Rs) h_2 = (Sum.inr (Rs.head ⋯), Γs, Rs.tail)
• Lean4GlCoalgebras.rewindHistoryOneStep (Sum.inr R, Γs, Rs) h_2 = (Sum.inl (Γs.head ⋯), Γs.tail, Rs)

theorem Lean4GlCoalgebras.rewind_history_one_step_of_move {q g : Game.Pos} (mv : Move q g) (h : Game.turn g = Prover ∧ g.2.2 ≠ ∅ ∨ Game.turn g = Builder ∧ g.2.1 ≠ ∅) : rewindHistoryOneStep g h = q

theorem Lean4GlCoalgebras.rewind_history_one_step_in_cone {Γ : Sequent} (g : Game.Pos) (h : Game.turn g = Prover ∧ g.2.2 ≠ ∅ ∨ Game.turn g = Builder ∧ g.2.1 ≠ ∅) (strat : Strategy coalgebraGame Prover) (in_cone : inMyCone strat (startPos Γ) g) : inMyCone strat (startPos Γ) (rewindHistoryOneStep g h)

Rewinding the history one step is still in the cone of the game.

@[irreducible]

def Lean4GlCoalgebras.rewindHistory (g : Game.Pos) (n : Fin ((if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1)) : Game.Pos

Rewinding the history n steps.

Equations

• Lean4GlCoalgebras.rewindHistory g n = match n_def : ↑n with | 0 => g | m.succ => Lean4GlCoalgebras.rewindHistory (Lean4GlCoalgebras.rewindHistoryOneStep g ⋯) ⟨m, ⋯⟩

theorem Lean4GlCoalgebras.rewind_history_in_cone {Γ : Sequent} (g : Game.Pos) (n : Fin ((if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1)) (strat : Strategy coalgebraGame Prover) (in_cone : inMyCone strat (startPos Γ) g) : inMyCone strat (startPos Γ) (rewindHistory g n)

Rewinding the history n steps is still in the cone of the game.

@[simp]

theorem Lean4GlCoalgebras.rewind_history_zero (g : Game.Pos) : rewindHistory g 0 = g

def Lean4GlCoalgebras.proof_type (Γ : Sequent) (strat : Strategy coalgebraGame Prover) : Type

This is the type of the coalgebra we will use to build the proof of Γ.

Equations

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

def Lean4GlCoalgebras.builderRuleApp (g : Game.Pos) (h : Game.turn g = Builder) : RuleApp

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.builderRuleApp (Sum.inr R, fst, snd) h_2 = R
• Lean4GlCoalgebras.builderRuleApp (Sum.inl val, fst, snd) h_2 = ⋯.elim

def Lean4GlCoalgebras.nextNext {Γ Δ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (h : winning strat (startPos Γ)) (nrep : Δ ∉ (↑g).2.1) (pos : Δ ∈ (builderRuleApp ↑g ⋯).sequents) : proof_type Γ strat

Defines the premise when we do not have a repeat.

Equations

• Lean4GlCoalgebras.nextNext g h nrep pos = ⟨↑(strat (Sum.inl Δ, (↑g).2.1, Lean4GlCoalgebras.builderRuleApp ↑g ⋯ :: (↑g).2.2) ⋯ ⋯), ⋯⟩

theorem Lean4GlCoalgebras.next_next_cor {Γ Δ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (h : winning strat (startPos Γ)) (nrep : Δ ∉ (↑g).2.1) (pos : Δ ∈ (builderRuleApp ↑g ⋯).sequents) : f (builderRuleApp ↑(nextNext g h nrep pos) ⋯) = Δ

The sequent at the premise defined by nextNext is the sequent Δ which we expect.

theorem Lean4GlCoalgebras.history_length_in_cone {Γ : Sequent} (strat : Strategy coalgebraGame Prover) (g : Game.Pos) (in_cone : inMyCone strat (startPos Γ) g) : (Game.turn g = Prover → g.2.1.length = g.2.2.length) ∧ (Game.turn g = Builder → g.2.1.length = g.2.2.length + 1)

Comparison of rule app history length and sequent history length.

def Lean4GlCoalgebras.repPos {Γ Δ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (rep : Δ ∈ (↑g).2.1) : Game.Pos

Defines the premise when we do not have a repeat.

Equations

• Lean4GlCoalgebras.repPos g rep = Lean4GlCoalgebras.rewindHistory ↑g ⟨2 * ↑(Fin.find (fun (k : Fin (↑g).2.1.length) => (↑g).2.1.get k = Δ) ⋯), ⋯⟩

theorem Lean4GlCoalgebras.rewind_turn_one_step {g : Game.Pos} {n : ℕ} {h1 : n + 1 < (if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1} {h2 : n < (if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1} : Game.turn (rewindHistory g ⟨n + 1, h1⟩) = other (Game.turn (rewindHistory g ⟨n, h2⟩))

Rewinding the game one step changes the player.

theorem Lean4GlCoalgebras.rewind_turn {g : Game.Pos} {n : Fin ((if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1)} : if Even ↑n then Game.turn (rewindHistory g n) = Game.turn g else Game.turn (rewindHistory g n) = other (Game.turn g)

Rewinding an even number of moves is the same players turn, rewinding an odd number is other players turn.

theorem Lean4GlCoalgebras.f_of_mem_ruleApps {Γ : Sequent} {R : RuleApp} (h : R ∈ Γ.ruleApps) : f R = Γ

The sequent at the one step rewind can be found in the history.

theorem Lean4GlCoalgebras.rewind_history_one_step_correspondence {Γ : Sequent} {g : Game.Pos} (strat : Strategy coalgebraGame Prover) {h0 : Game.turn g = Prover ∧ g.2.2 ≠ ∅ ∨ Game.turn g = Builder ∧ g.2.1 ≠ ∅} {h1 : Game.turn (rewindHistoryOneStep g h0) = Builder} {h2 : 0 < g.2.1.length} (in_cone : inMyCone strat (startPos Γ) g) : f (builderRuleApp (rewindHistoryOneStep g h0) h1) = g.2.1[0]

theorem Lean4GlCoalgebras.builder_RuleApp_head_of_in_cone {Γ : Sequent} {g : Game.Pos} (strat : Strategy coalgebraGame Prover) (in_cone : inMyCone strat (startPos Γ) g) (h : Game.turn g = Builder) (h2 : 0 < g.2.1.length) : f (builderRuleApp g h) = g.2.1[0]

The rule application at a builder position in the cone points to the head sequent.

theorem Lean4GlCoalgebras.rewind_history_correspondence_aux (Γ : Sequent) (info : Sequent ⊕ RuleApp) (Γs : List Sequent) (Rs : List RuleApp) (strat : Strategy coalgebraGame Prover) (n : ℕ) (h2 : n < Γs.length) (h3 : 2 * n < (if Game.turn (info, Γs, Rs) = Prover then min (2 * (info, Γs, Rs).2.1.length + 1) (2 * (info, Γs, Rs).2.2.length) else min (2 * (info, Γs, Rs).2.1.length) (2 * (info, Γs, Rs).2.2.length + 1)) + 1) (h4 : 2 * n + 1 < (if Game.turn (info, Γs, Rs) = Prover then min (2 * (info, Γs, Rs).2.1.length + 1) (2 * (info, Γs, Rs).2.2.length) else min (2 * (info, Γs, Rs).2.1.length) (2 * (info, Γs, Rs).2.2.length + 1)) + 1) (h6 : n < Γs.length) (in_cone : inMyCone strat (startPos Γ) (info, Γs, Rs)) : (∀ (b_turn_g : Game.turn (info, Γs, Rs) = Builder), f (builderRuleApp (rewindHistory (info, Γs, Rs) ⟨2 * n, h3⟩) ⋯) = Γs[n]) ∧ ∀ (p_turn_q : Game.turn (info, Γs, Rs) = Prover), f (builderRuleApp (rewindHistory (info, Γs, Rs) ⟨2 * n + 1, h4⟩) ⋯) = Γs[n]

The sequent at the n step rewind can be found in the history.

theorem Lean4GlCoalgebras.rewind_history_correspondence (Γ : Sequent) (g : Game.Pos) (strat : Strategy coalgebraGame Prover) (n : ℕ) (h2 : n < g.2.1.length) (h3 : 2 * n < (if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1) (h4 : 2 * n + 1 < (if Game.turn g = Prover then min (2 * g.2.1.length + 1) (2 * g.2.2.length) else min (2 * g.2.1.length) (2 * g.2.2.length + 1)) + 1) (h6 : n < g.2.1.length) (in_cone : inMyCone strat (startPos Γ) g) : (∀ (b_turn_g : Game.turn g = Builder), f (builderRuleApp (rewindHistory g ⟨2 * n, h3⟩) ⋯) = g.2.1[n]) ∧ ∀ (p_turn_q : Game.turn g = Prover), f (builderRuleApp (rewindHistory g ⟨2 * n + 1, h4⟩) ⋯) = g.2.1[n]

The sequent at the n step rewind can be found in the history.

def Lean4GlCoalgebras.repNext (Γ : Sequent) {Δ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (rep : Δ ∈ (↑g).2.1) : proof_type Γ strat

Defines the premise when we have a repeat.

Equations

• Lean4GlCoalgebras.repNext Γ g rep = ⟨Lean4GlCoalgebras.repPos g rep, ⋯⟩

theorem Lean4GlCoalgebras.rep_next_cor (Γ : Sequent) {Δ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (rep : Δ ∈ (↑g).2.1) : f (builderRuleApp ↑(repNext Γ g rep) ⋯) = Δ

The sequent at the premise defined by repNext is the sequent Δ which we expect.

def Lean4GlCoalgebras.builderMovePremises {Γ : Sequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (h : winning strat (startPos Γ)) : List (proof_type Γ strat)

Define the list of premises from a Builder move.

Equations

• One or more equations did not get rendered due to their size.
• Lean4GlCoalgebras.builderMovePremises ⟨(Sum.inl val, fst, snd), ⋯⟩ h = ⋯.elim
• Lean4GlCoalgebras.builderMovePremises ⟨(Sum.inr (Lean4GlCoalgebras.RuleApp.top Δ a), Γs, Rs), property_2⟩ h = []
• Lean4GlCoalgebras.builderMovePremises ⟨(Sum.inr (Lean4GlCoalgebras.RuleApp.ax Δ n a), Γs, Rs), property_2⟩ h = []

theorem Lean4GlCoalgebras.prover_win_builds_proof {Γ : Sequent} (strat : Strategy coalgebraGame Prover) (h : winning strat (startPos Γ)) : ⊢Γ

If Prover has a winning strategy in the game starting from Γ, then there is a proof of `Γ!

Builder winning the GL-game builds a GL-countermodel.

If Builder has a winning strategy in the game starting from Γ, then there is a proof of Γ, proven in builder_win_builds_model, all other definitions and proofs in this file are helpers.

Maximal Paths.

def Lean4GlCoalgebras.afterBox (g : Game.Pos) : Prop

Predicate on moves in the game necessary for quantifying maximal paths.

Equations

• Lean4GlCoalgebras.afterBox (Sum.inl val, fst, R :: tail) = (R.isBox = true)
• Lean4GlCoalgebras.afterBox g = (false = true)

def Lean4GlCoalgebras.isBox (g : Game.Pos) : Prop

Predicate on moves in the game necessary for quantifying maximal paths.

Equations

• Lean4GlCoalgebras.isBox (Sum.inr R, fst, snd) = (R.isBox = true)
• Lean4GlCoalgebras.isBox g = (false = true)

def Lean4GlCoalgebras.nonBoxMove : Game.Pos → Game.Pos → Prop

Relation on moves in the game necessary for quantifying maximal paths.

Equations

• Lean4GlCoalgebras.nonBoxMove x y = (Lean4GlCoalgebras.Move x y ∧ ¬Lean4GlCoalgebras.isBox y)

structure Lean4GlCoalgebras.MaximalPath (Γ : Sequent) (strat : Strategy coalgebraGame Builder) : Type

The type of a maximal path in the game.

• list : List Game.Pos

  Auxiliary declaration used in the GL coalgebra development.

• ne : self.list ≠ []
• chain : List.IsChain nonBoxMove self.list
• max : ¬∃ (z : Game.Pos), nonBoxMove (self.list.getLast ⋯) z
• head_cases : afterBox (self.list.head ⋯) ∨ self.list.head ⋯ = startPos Γ
• in_cone (x : Game.Pos) : x ∈ self.list → inMyCone strat (startPos Γ) x

def Lean4GlCoalgebras.MaximalPath.last {Γ : Sequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → Game.Pos

Auxiliary declaration used in the GL coalgebra development.

Equations

• π.last = π.list.getLast ⋯

def Lean4GlCoalgebras.MaximalPath.first {Γ : Sequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → Game.Pos

Auxiliary declaration used in the GL coalgebra development.

Equations

• π.first = π.list.head ⋯

theorem Lean4GlCoalgebras.maximal_path_starts_in_prover_turn {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (π : MaximalPath Γ strat) : Game.turn π.first = Prover

Maximal paths always start from a move which is Prover's turn.

theorem Lean4GlCoalgebras.maximal_path_ends_in_prover_turn {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) (π : MaximalPath Γ strat) : Game.turn π.last = Prover

Maximal paths always end in a move which is Prover's turn.

@[irreducible]

noncomputable def Lean4GlCoalgebras.makePathFrom (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : List Game.Pos

If Builder is winning, there is always a maximal path.

Equations

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

theorem Lean4GlCoalgebras.make_path_from_is_nonempty (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : ¬makePathFrom strat g = ∅

If Builder is winning, the List from makePathFrom is nonempty.

theorem Lean4GlCoalgebras.make_path_from_head (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : (makePathFrom strat g).head ⋯ = g

theorem Lean4GlCoalgebras.make_path_from_head? (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : (makePathFrom strat g).head? = some g

theorem Lean4GlCoalgebras.make_path_from_is_chain (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : List.IsChain nonBoxMove (makePathFrom strat g)

If Builder is winning, the List from makePathFrom is a chain.

theorem Lean4GlCoalgebras.make_path_is_max (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : ¬∃ (g' : Game.Pos), nonBoxMove ((makePathFrom strat g).getLast ⋯) g'

If Builder is winning, the List from makePathFrom is maximal.

theorem Lean4GlCoalgebras.make_path_is_in_cone (Δ : Sequent) (strat : Strategy coalgebraGame Builder) (g : Game.Pos) (in_cone : inMyCone strat (Sum.inl Δ, [], []) g) (h : winning strat (Sum.inl Δ, [], [])) (i : Fin (makePathFrom strat g).length) : inMyCone strat (Sum.inl Δ, [], []) ((makePathFrom strat g).get i)

If Builder is winning, every move in the list from makePathFrom is in the cone.

theorem Lean4GlCoalgebras.always_exists_maximal_path_from_root_or_after (Γ : Sequent) (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Γ)) (g : Game.Pos) (in_cone : inMyCone strat (startPos Γ) g) (head_cases : afterBox g ∨ g = startPos Γ) : ∃ (π : MaximalPath Γ strat), π.first = g

If Builder is winning, the starting move or any move after a box move has a maximal path.

def Lean4GlCoalgebras.proverSequent (g : Game.Pos) (h : Game.turn g = Prover) : Sequent

Given a prover move, find the underlying sequent.

Equations

• Lean4GlCoalgebras.proverSequent (Sum.inl Γ, Γs, Rs) h_2 = Γ
• Lean4GlCoalgebras.proverSequent (Sum.inr R, Γ :: Γs, Rs) h_2 = ⋯.elim

def Lean4GlCoalgebras.firstSequent {Γ : Sequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → Sequent

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.firstSequent π = Lean4GlCoalgebras.proverSequent π.first ⋯

theorem Lean4GlCoalgebras.first_sequent_eq_of_first {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (π : MaximalPath Γ strat) {Δ : Sequent} {Δs : List Sequent} {Rs : List RuleApp} (hfirst : π.first = (Sum.inl Δ, Δs, Rs)) : firstSequent π = Δ

def Lean4GlCoalgebras.lastSequent {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) : MaximalPath Γ strat → Sequent

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.lastSequent h π = Lean4GlCoalgebras.proverSequent π.last ⋯

def Lean4GlCoalgebras.pathRelation (Γ : Sequent) (strat : Strategy coalgebraGame Builder) (π₁ π₂ : MaximalPath Γ strat) : Prop

Two maximal paths are related if two steps in the game can connect tail to head.

Equations

• Lean4GlCoalgebras.pathRelation Γ strat π₁ π₂ = Relation.Comp Lean4GlCoalgebras.Move Lean4GlCoalgebras.Move π₁.last π₂.first

theorem Lean4GlCoalgebras.Relation.TransGen.swap_eq_swap_rel {α : Type} (r : α → α → Prop) : Function.swap (Relation.TransGen r) = Relation.TransGen (Function.swap r)

theorem Lean4GlCoalgebras.maximal_path_refl_trans_gen (as : List Game.Pos) (ne : as ≠ []) (chain : List.IsChain nonBoxMove as) : Relation.ReflTransGen Move (as.head ne) (as.getLast ne)

def Lean4GlCoalgebras.gameBModel (Γ : Sequent) {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) : Model (MaximalPath Γ strat)

The definition of the GL-model (M,R,V) we will use as the countermodel. M, R, V are all defined as expected (except R is transtive), transitivity is immediate, and converse well-foundedness follow from well-foundedness of the game.

Equations

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

theorem Lean4GlCoalgebras.move_from_last_implies_box {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (π : MaximalPath Γ strat) (x : GamePos) : Move π.last x → isBox x

theorem Lean4GlCoalgebras.diamond_in_of_move_move_diamond_in {x z : GamePos} (hx : Game.turn x = Prover) (hz : Game.turn z = Prover) (x_z : Relation.Comp Move Move x z) (φ : Formula) : ◇φ ∈ proverSequent x hx → ◇φ ∈ proverSequent z hz

Helper for ◇ case of builder_win_strong.

theorem Lean4GlCoalgebras.diamond_in_last_of_diamond_in_first {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) (π : MaximalPath Γ strat) (φ : Formula) (i : ℕ) (lt : i < π.list.length) (helper : π.list.length - i - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - i - 1] = Prover) : ◇φ ∈ proverSequent π.list[π.list.length - i - 1] ps → ◇φ ∈ lastSequent h π

Helper for ◇ case of builder_win_strong.

theorem Lean4GlCoalgebras.formula_in_successor_of_diamond_formula_in {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : pathRelation Γ strat π ρ) (φ : Formula) : ◇φ ∈ lastSequent h π → φ ∈ firstSequent ρ

Helper for ◇ case of builder_win_strong.

theorem Lean4GlCoalgebras.diamond_in_path_of_diamond_formula_in {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : Relation.TransGen (pathRelation Γ strat) π ρ) (φ : Formula) : ◇φ ∈ lastSequent h π → ◇φ ∈ firstSequent ρ

Helper for ◇ case of builder_win_strong.

theorem Lean4GlCoalgebras.formula_in_path_of_diamond_formula_in {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : Relation.TransGen (pathRelation Γ strat) π ρ) (φ : Formula) : ◇φ ∈ lastSequent h π → φ ∈ firstSequent ρ

Helper for ◇ case of builder_win_strong.

theorem Lean4GlCoalgebras.builder_win_strong {Δ : Sequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (Sum.inl Δ, [], [])) (π : MaximalPath Δ strat) (φ : Formula) (i : ℕ) (lt : i < π.list.length) (helper : π.list.length - i - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - i - 1] = Prover) : φ ∈ proverSequent π.list[π.list.length - i - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

If Builder has a winning strategy, then for any maximal path π, if φ appears in π then the model gameBModel which we previously defined will falsify φ at π.

theorem Lean4GlCoalgebras.builder_win_builds_model {Γ : Sequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Γ)) : ¬⊨Γ

If Builder has a winning strategy in the game starting from Γ, then there is a countermodel of `Γ!

theorem Lean4GlCoalgebras.completeness (Γ : Sequent) : ⊨Γ → ⊢Γ

Completeness! Comes as a corrolary of gamedet, prover_win_builds_proof, and builder_win_builds_model.