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 rewind_history_one_step (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

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

theorem 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 Γ) (rewind_history_one_step g h)

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

@[irreducible]

def rewind_history (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

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

@[irreducible]

theorem 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 Γ) (rewind_history g n)

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

@[simp]

theorem rewind_history_zero (g : Game.Pos) : rewind_history g 0 = g

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

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

Equations

• proof_type Γ strat = { g : Game.Pos // inMyCone strat (startPos Γ) g ∧ Game.turn g = Builder }

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

Equations

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

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

Defines the premise when we do not have a repeat.

Equations

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

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

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

theorem 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 rep_pos {Γ Δ : 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

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

@[irreducible]

theorem 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 (rewind_history g ⟨n + 1, h1⟩) = other (Game.turn (rewind_history g ⟨n, h2⟩))

Rewinding the game one step changes the player.

theorem 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 (rewind_history g n) = Game.turn g else Game.turn (rewind_history 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 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 (rewind_history_one_step g h0) = Builder} {h2 : 0 < g.2.1.length} (in_cone : inMyCone strat (startPos Γ) g) : f (builder_RuleApp (rewind_history_one_step g h0) h1) = g.2.1[0]

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

@[irreducible]

theorem 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 (builder_RuleApp (rewind_history g ⟨2 * n, h3⟩) ⋯) = g.2.1[n]) ∧ ∀ (p_turn_q : Game.turn g = Prover), f (builder_RuleApp (rewind_history g ⟨2 * n + 1, h4⟩) ⋯) = g.2.1[n]

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

def rep_next (Γ : 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

• rep_next Γ g rep = ⟨rep_pos g rep, ⋯⟩

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

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

def builder_move_premises {Γ : 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.
• builder_move_premises ⟨(Sum.inl val, fst, snd), ⋯⟩ h = ⋯.elim
• builder_move_premises ⟨(Sum.inr (RuleApp.top Δ a), Γs, Rs), property_2⟩ h = []
• builder_move_premises ⟨(Sum.inr (RuleApp.ax Δ n a), Γs, Rs), property_2⟩ h = []

theorem 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 after_box (g : Game.Pos) : Prop

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

Equations

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

def is_box (g : Game.Pos) : Prop

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

Equations

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

def non_box_move : Game.Pos → Game.Pos → Prop

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

Equations

• non_box_move x y = (Move x y ∧ ¬is_box y)

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

The type of a maximal path in the game.

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

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

Equations

• π.last = π.list.getLast ⋯

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

Equations

• π.first = π.list.head ⋯

theorem 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 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 make_path_from (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 make_path_from_is_nonempty (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : ¬make_path_from strat g = ∅

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

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

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

@[irreducible]

theorem make_path_from_is_chain (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : List.IsChain non_box_move (make_path_from strat g)

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

@[irreducible]

theorem make_path_is_max (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : ¬∃ (g' : Game.Pos), non_box_move ((make_path_from strat g).getLast ⋯) g'

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

@[irreducible]

theorem 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 (make_path_from strat g).length) : inMyCone strat (Sum.inl Δ, [], []) ((make_path_from strat g).get i)

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

theorem 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 : after_box 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 prover_sequent (g : Game.Pos) (h : Game.turn g = Prover) : Sequent

Given a prover move, find the underlying sequent.

Equations

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

def first_sequent {Γ : Sequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → Sequent

Equations

• first_sequent π = prover_sequent π.first ⋯

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

Equations

• last_sequent h π = prover_sequent π.last ⋯

def path_relation (Γ : 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

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

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

Interesting for MathLib?

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

def game_b_model (Γ : 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

• game_b_model Γ h = { V := fun (π : MaximalPath Γ strat) (n : ℕ) => at n ∉ last_sequent h π, R := Relation.TransGen (path_relation Γ strat), trans := ⋯, con_wf := ⋯ }

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

theorem 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) : ◇φ ∈ prover_sequent x hx → ◇φ ∈ prover_sequent z hz

Helper for ◇ case of builder_win_strong.

@[irreducible]

theorem 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) : ◇φ ∈ prover_sequent π.list[π.list.length - i - 1] ps → ◇φ ∈ last_sequent h π

Helper for ◇ case of builder_win_strong.

theorem formula_in_successor_of_diamond_formula_in {Γ : Sequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : path_relation Γ strat π ρ) (φ : Formula) : ◇φ ∈ last_sequent h π → φ ∈ first_sequent ρ

Helper for ◇ case of builder_win_strong.

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

Helper for ◇ case of builder_win_strong.

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

Helper for ◇ case of builder_win_strong.

@[irreducible]

def 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) : φ ∈ prover_sequent π.list[π.list.length - i - 1] ps → ¬evaluate (game_b_model Δ h, π) φ

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

Equations

• ⋯ = ⋯

theorem 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 completeness_seq (Γ : Sequent) : ⊨Γ → ⊢Γ

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