Prover winning the GL-split game builds a GL-split 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 Split.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

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

theorem Split.rewind_history_one_step_in_cone {Γ : SplitSequent} (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 Split.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

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

@[irreducible]

theorem Split.rewind_history_in_cone {Γ : SplitSequent} (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 Split.rewind_history_zero (g : Game.Pos) : rewind_history g 0 = g

def Split.proof_type (Γ : SplitSequent) (strat : Strategy coalgebraGame Prover) : Type

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

Equations

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

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

Equations

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

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

Defines the premise when we do not have a repeat.

Equations

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

theorem Split.next_next_cor {Γ Δ : SplitSequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (h : winning strat (startPos Γ)) (nrep : Δ ∉ (↑g).2.1) (pos : Δ ∈ (builder_RuleApp ↑g ⋯).splitSequents) : 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 Split.history_length_in_cone {Γ : SplitSequent} (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 Split.rep_pos {Γ Δ : SplitSequent} {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

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

@[irreducible]

theorem Split.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 Split.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 Split.rewind_history_one_step_correspondence {Γ : SplitSequent} {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 Split.rewind_history_correspondence (Γ : SplitSequent) (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 Split.rep_next (Γ : SplitSequent) {Δ : SplitSequent} {strat : Strategy coalgebraGame Prover} (g : proof_type Γ strat) (rep : Δ ∈ (↑g).2.1) : proof_type Γ strat

Defines the premise when we have a repeat.

Equations

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

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

theorem Split.prover_win_builds_proof {Γ : SplitSequent} (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-split game builds a GL-model.

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.

def Split.after_box (g : Game.Pos) : Prop

Equations

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

def Split.is_box (g : Game.Pos) : Prop

Equations

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

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

Equations

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

structure Split.MaximalPath (Γ : SplitSequent) (strat : Strategy coalgebraGame Builder) : Type

• 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 Split.MaximalPath.last {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → Game.Pos

Equations

• π.last = π.list.getLast ⋯

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

Equations

• π.first = π.list.head ⋯

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

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

@[irreducible]

noncomputable def Split.make_path_from (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : List Game.Pos

Equations

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

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

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

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

@[irreducible]

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

@[irreducible]

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

@[irreducible]

theorem Split.make_path_is_in_cone (Δ : SplitSequent) (strat : Strategy coalgebraGame Builder) (g : Game.Pos) (in_cone : inMyCone strat (startPos Δ) g) (h : winning strat (startPos Δ)) (i : Fin (make_path_from strat g).length) : inMyCone strat (startPos Δ) ((make_path_from strat g).get i)

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

def Split.prover_SplitSequent (g : Game.Pos) (h : Game.turn g = Prover) : SplitSequent

Equations

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

def Split.first_SplitSequent {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} : MaximalPath Γ strat → SplitSequent

Equations

• Split.first_SplitSequent π = Split.prover_SplitSequent π.first ⋯

def Split.last_SplitSequent {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) : MaximalPath Γ strat → SplitSequent

Equations

• Split.last_SplitSequent h π = Split.prover_SplitSequent π.last ⋯

def Split.path_relation (Γ : SplitSequent) (strat : Strategy coalgebraGame Builder) (π₁ π₂ : MaximalPath Γ strat) : Prop

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

Equations

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

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

Interesting for MathLib?

theorem Split.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 Split.game_b_model (Γ : SplitSequent) {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) : Model (MaximalPath Γ strat)

Builds the counter-model from a Builder winning strategy.

Equations

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

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

theorem Split.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_SplitSequent x hx).toSequent → ◇φ ∈ (prover_SplitSequent z hz).toSequent

@[irreducible]

theorem Split.diamond_in_last_of_diamond_in_first {Γ : SplitSequent} {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_SplitSequent π.list[π.list.length - i - 1] ps).toSequent → ◇φ ∈ (last_SplitSequent h π).toSequent

theorem Split.formula_in_successor_of_diamond_formula_in {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : path_relation Γ strat π ρ) (φ : Formula) : ◇φ ∈ (last_SplitSequent h π).toSequent → φ ∈ (first_SplitSequent ρ).toSequent

theorem Split.diamond_in_path_of_diamond_formula_in {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : Relation.TransGen (path_relation Γ strat) π ρ) (φ : Formula) : ◇φ ∈ (last_SplitSequent h π).toSequent → ◇φ ∈ (first_SplitSequent ρ).toSequent

theorem Split.formula_in_path_of_diamond_formula_in {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Γ)) {π ρ : MaximalPath Γ strat} (π_ρ : Relation.TransGen (path_relation Γ strat) π ρ) (φ : Formula) : ◇φ ∈ (last_SplitSequent h π).toSequent → φ ∈ (first_SplitSequent ρ).toSequent

@[irreducible]

theorem Split.builder_win_strong {Δ : SplitSequent} (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_SplitSequent π.list[π.list.length - i - 1] ps).toSequent → ¬evaluate (game_b_model Δ h, π) φ

If Builder wins, no formula in the sequents at Prover positions evaluates to true.

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

If Builder wins, there exists a counter-model.

theorem Split.completeness_sseq (Γ : SplitSequent) : ⊨Γ → ⊢Γ

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

theorem Split.equiv_iff_sem_equiv {φ ψ : Formula} : semEquiv φ ψ ↔ (φ≅ψ)

Corollary of completeness_sseq, used in Interpolants.lean

theorem Split.single_preserves_equiv (n : ℕ) (φ ψ χ : Formula) (equiv : φ≅ψ) : single n χ φ≅single n χ ψ