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 Lean4GlCoalgebras.Split.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.Split.rewindHistoryOneStep (Sum.inl Γ, Γs, Rs) h_2 = (Sum.inr (Rs.head ⋯), Γs, Rs.tail)
• Lean4GlCoalgebras.Split.rewindHistoryOneStep (Sum.inr R, Γs, Rs) h_2 = (Sum.inl (Γs.head ⋯), Γs.tail, Rs)

theorem Lean4GlCoalgebras.Split.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.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 Γ) (rewindHistoryOneStep g h)

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

@[irreducible]

def Lean4GlCoalgebras.Split.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.Split.rewindHistory g n = match n_def : ↑n with | 0 => g | m.succ => Lean4GlCoalgebras.Split.rewindHistory (Lean4GlCoalgebras.Split.rewindHistoryOneStep g ⋯) ⟨m, ⋯⟩

theorem Lean4GlCoalgebras.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 Γ) (rewindHistory g n)

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

@[simp]

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

def Lean4GlCoalgebras.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

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Defines the premise when we do not have a repeat.

Equations

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

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

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.Split.repPos {Γ Δ : 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

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

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

Rewinding the game one step changes the player.

theorem Lean4GlCoalgebras.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 (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.Split.f_of_mem_ruleApps {Γ : SplitSequent} {R : RuleApp} (h : R ∈ SplitSequent.ruleApps Γ) : f R = Γ

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

theorem Lean4GlCoalgebras.Split.ruleApp_topl_mem {Γ : SplitSequent} (h : Sum.inl ⊤ ∈ Γ) : RuleApp.topₗ Γ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_topr_mem {Γ : SplitSequent} (h : Sum.inr ⊤ ∈ Γ) : RuleApp.topᵣ Γ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_axll_mem {Γ : SplitSequent} {n : ℕ} (h : Sum.inl (at n) ∈ Γ ∧ Sum.inl (na n) ∈ Γ) : RuleApp.axₗₗ Γ n h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_axlr_mem {Γ : SplitSequent} {n : ℕ} (h : Sum.inl (at n) ∈ Γ ∧ Sum.inr (na n) ∈ Γ) (h_left : Sum.inl (na n) ∉ Γ) : RuleApp.axₗᵣ Γ n h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_axrl_mem {Γ : SplitSequent} {n : ℕ} (h : Sum.inr (at n) ∈ Γ ∧ Sum.inl (na n) ∈ Γ) : RuleApp.axᵣₗ Γ n h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_axrr_mem {Γ : SplitSequent} {n : ℕ} (h : Sum.inr (at n) ∈ Γ ∧ Sum.inr (na n) ∈ Γ) (h_left : Sum.inl (na n) ∉ Γ) : RuleApp.axᵣᵣ Γ n h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_andl_mem {Γ : SplitSequent} {φ ψ : Formula} (h : Sum.inl (φ&ψ) ∈ Γ) : RuleApp.andₗ Γ φ ψ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_andr_mem {Γ : SplitSequent} {φ ψ : Formula} (h : Sum.inr (φ&ψ) ∈ Γ) : RuleApp.andᵣ Γ φ ψ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_orl_mem {Γ : SplitSequent} {φ ψ : Formula} (h : Sum.inl (φ v ψ) ∈ Γ) : RuleApp.orₗ Γ φ ψ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_orr_mem {Γ : SplitSequent} {φ ψ : Formula} (h : Sum.inr (φ v ψ) ∈ Γ) : RuleApp.orᵣ Γ φ ψ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_boxl_mem {Γ : SplitSequent} {φ : Formula} (h : Sum.inl (□φ) ∈ Γ) : RuleApp.boxₗ Γ φ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.Split.ruleApp_boxr_mem {Γ : SplitSequent} {φ : Formula} (h : Sum.inr (□φ) ∈ Γ) : RuleApp.boxᵣ Γ φ h ∈ SplitSequent.ruleApps Γ

theorem Lean4GlCoalgebras.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 (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.Split.builder_RuleApp_head_of_in_cone {Γ : SplitSequent} {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.Split.rewind_history_correspondence_aux (Γ : SplitSequent) (info : SplitSequent ⊕ RuleApp) (Γs : List SplitSequent) (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.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 (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.Split.repNext (Γ : 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

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

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

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

If Prover has a winning strategy in the game 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 Lean4GlCoalgebras.Split.afterBox (g : Game.Pos) : Prop

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

Auxiliary declaration used in the GL coalgebra development.

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

Auxiliary declaration used in the GL coalgebra development.

Equations

• π.last = π.list.getLast ⋯

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

Auxiliary declaration used in the GL coalgebra development.

Equations

• π.first = π.list.head ⋯

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.Split.makePathFrom (strat : Strategy coalgebraGame Builder) (g : Game.Pos) : List Game.Pos

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

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

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

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

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

theorem Lean4GlCoalgebras.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 (makePathFrom strat g).length) : inMyCone strat (startPos Δ) ((makePathFrom strat g).get i)

theorem Lean4GlCoalgebras.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 : afterBox g ∨ g = startPos Γ) : ∃ (π : MaximalPath Γ strat), π.first = g

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

theorem Lean4GlCoalgebras.Split.prover_SplitSequent_eq_of_inl {g : Game.Pos} {h : Game.turn g = Prover} {Γ : SplitSequent} {Γs : List SplitSequent} {Rs : List RuleApp} (hg : (Sum.inl Γ, Γs, Rs) = g) : proverSplitSequent g h = Γ

Recovers the prover sequent from an explicitly identified prover game position.

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

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.firstSplitSequent π = Lean4GlCoalgebras.Split.proverSplitSequent π.first ⋯

theorem Lean4GlCoalgebras.Split.first_SplitSequent_eq_of_first {Γ : SplitSequent} {strat : Strategy coalgebraGame Builder} (π : MaximalPath Γ strat) {Δ : SplitSequent} {Δs : List SplitSequent} {Rs : List RuleApp} (hfirst : π.first = (Sum.inl Δ, Δs, Rs)) : firstSplitSequent π = Δ

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

Auxiliary declaration used in the GL coalgebra development.

Equations

• Lean4GlCoalgebras.Split.lastSplitSequent h π = Lean4GlCoalgebras.Split.proverSplitSequent π.last ⋯

def Lean4GlCoalgebras.Split.pathRelation (Γ : 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

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

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

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

Builds the Kripke counter-model from a Builder winning strategy.

Equations

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

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

theorem Lean4GlCoalgebras.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) : ◇φ ∈ (proverSplitSequent x hx).toSequent → ◇φ ∈ (proverSplitSequent z hz).toSequent

theorem Lean4GlCoalgebras.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) : ◇φ ∈ (proverSplitSequent π.list[π.list.length - i - 1] ps).toSequent → ◇φ ∈ (lastSplitSequent h π).toSequent

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

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

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

theorem Lean4GlCoalgebras.Split.no_terminal_rule_app_at_last {Δ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (R : RuleApp) (R_in : R ∈ SplitSequent.ruleApps (lastSplitSequent h π)) (R_empty : R.splitSequents = ∅) : False

A terminal split rule application cannot be available at the last node of a Builder-winning path.

theorem Lean4GlCoalgebras.Split.no_nonbox_rule_app_at_last {Δ : SplitSequent} {strat : Strategy coalgebraGame Builder} (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (R : RuleApp) (R_in : R ∈ SplitSequent.ruleApps (lastSplitSequent h π)) (R_nonbox : ¬R.isBox) : False

A non-box split rule application cannot extend the last node of a maximal path.

theorem Lean4GlCoalgebras.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) : Sum.inl φ ∈ proverSplitSequent π.list[π.list.length - i - 1] ps ∨ Sum.inr φ ∈ proverSplitSequent π.list[π.list.length - i - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

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

theorem Lean4GlCoalgebras.Split.builder_win_strong_left_zero {Δ : SplitSequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (φ : Formula) (i : ℕ) (h_i : i = 0) (lt : i < π.list.length) (helper : π.list.length - i - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - i - 1] = Prover) (noTerminal : ∀ R ∈ SplitSequent.ruleApps (lastSplitSequent h π), R.splitSequents = ∅ → False) (noNonbox : ∀ R ∈ SplitSequent.ruleApps (lastSplitSequent h π), ¬R.isBox → False) : Sum.inl φ ∈ proverSplitSequent π.list[π.list.length - i - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

Left-side last-node case for builder_win_strong.

theorem Lean4GlCoalgebras.Split.builder_win_strong_left_succ {Δ : SplitSequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (φ : Formula) (j i : ℕ) (h_j : j = i + 1) (lt : j < π.list.length) (helper : π.list.length - j - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - j - 1] = Prover) : Sum.inl φ ∈ proverSplitSequent π.list[π.list.length - j - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

Left-side successor case for builder_win_strong.

theorem Lean4GlCoalgebras.Split.builder_win_strong_right_zero {Δ : SplitSequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (φ : Formula) (i : ℕ) (h_i : i = 0) (lt : i < π.list.length) (helper : π.list.length - i - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - i - 1] = Prover) (noTerminal : ∀ R ∈ SplitSequent.ruleApps (lastSplitSequent h π), R.splitSequents = ∅ → False) (noNonbox : ∀ R ∈ SplitSequent.ruleApps (lastSplitSequent h π), ¬R.isBox → False) : Sum.inr φ ∈ proverSplitSequent π.list[π.list.length - i - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

Right-side last-node case for builder_win_strong.

theorem Lean4GlCoalgebras.Split.builder_win_strong_right_succ {Δ : SplitSequent} (strat : Strategy coalgebraGame Builder) (h : winning strat (startPos Δ)) (π : MaximalPath Δ strat) (φ : Formula) (j i : ℕ) (h_j : j = i + 1) (lt : j < π.list.length) (helper : π.list.length - j - 1 < π.list.length) (ps : Game.turn π.list[π.list.length - j - 1] = Prover) : Sum.inr φ ∈ proverSplitSequent π.list[π.list.length - j - 1] ps → ¬evaluate (gameBModel Δ h, π) φ

Right-side successor case for builder_win_strong.

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

If Builder wins, there exists a counter-model.

theorem Lean4GlCoalgebras.Split.completeness (Γ : SplitSequent) : ⊨Γ → ⊢Γ

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

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

Corollary of completeness, used in Interpolants.lean.

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