Documentation

LeanPool.Lean4GlCoalgebras.Split.Soundness

Soundness of GL-split proof system. #

source
noncomputable def Lean4GlCoalgebras.ExtSkip.chain {𝕏 : Proof} {x : 𝕏.X} {Ξ“ : SplitSequent} (prop : f (r 𝕏.Ξ± x) = Ξ“) {W : Type} {M : Model W} {w : W} (w_prop : Β¬evaluateSSeq (M, w) Ξ“) (n : β„•) :
(y : 𝕏.X) Γ— { u : W // Β¬evaluateSSeq (M, u) (f (r 𝕏.Ξ± y)) }

Helper for soundness, Given a proof of Ξ“ and a countermodel of Ξ“, find a path in the proof and the model

Equations
Instances For
    source
    theorem Lean4GlCoalgebras.ExtSkip.chain_proof_prop {𝕏 : Proof} {x : 𝕏.X} {Ξ“ : SplitSequent} (prop : f (r 𝕏.Ξ± x) = Ξ“) {W : Type} {M : Model W} {w : W} (w_prop : Β¬evaluateSSeq (M, w) Ξ“) (n : β„•) :
    edge 𝕏.Ξ± (chain prop w_prop n).fst (chain prop w_prop (n + 1)).fst

    The left projection of chain is a chain in the proof.

    source
    theorem Lean4GlCoalgebras.ExtSkip.chain_model_prop {𝕏 : Proof} {x : 𝕏.X} {Ξ“ : SplitSequent} (prop : f (r 𝕏.Ξ± x) = Ξ“) {W : Type} {M : Model W} {w : W} (w_prop : Β¬evaluateSSeq (M, w) Ξ“) (n : β„•) :
    (Β¬(r 𝕏.Ξ± (chain prop w_prop n).fst).isBox β†’ ↑(chain prop w_prop n).snd = ↑(chain prop w_prop (n + 1)).snd) ∧ ((r 𝕏.Ξ± (chain prop w_prop n).fst).isBox β†’ M.R ↑(chain prop w_prop n).snd ↑(chain prop w_prop (n + 1)).snd)

    The right projection of chain makes progress in the model on box nodes.

    source
    theorem Lean4GlCoalgebras.ExtSkip.has_children_of_chain_model {𝕏 : Proof} {x : 𝕏.X} {Ξ“ : SplitSequent} (prop : f (r 𝕏.Ξ± x) = Ξ“) {W : Type} {M : Model W} {w : W} (w_prop : Β¬evaluateSSeq (M, w) Ξ“) (n : β„•) :
    βˆƒ (m : β„•), M.R ↑(chain prop w_prop n).snd ↑(chain prop w_prop (n + m)).snd

    The right projection of chain eventually progresses.

    source
    noncomputable def Lean4GlCoalgebras.ExtSkip.incChainEventualIncChain {Ξ² : Sort u_1} {Q : Ξ² β†’ Ξ² β†’ Prop} {g : β„• β†’ Ξ²} (Q_prop : βˆ€ (n : β„•), βˆƒ (m : β„•), Q (g n) (g m)) (n : β„•) :
    { b : Ξ² // βˆƒ (n : β„•), b = g n }

    Progressing subchain of an eventually increasing chain.

    Equations
    Instances For
      source
      theorem Lean4GlCoalgebras.ExtSkip.inc_chain_eventual_inc_chain_prop {Ξ² : Sort u_1} {Q : Ξ² β†’ Ξ² β†’ Prop} {g : β„• β†’ Ξ²} (Q_prop : βˆ€ (n : β„•), βˆƒ (m : β„•), Q (g n) (g m)) (n : β„•) :
      Q ↑(incChainEventualIncChain Q_prop n) ↑(incChainEventualIncChain Q_prop (n + 1))

      An eventually progressing chain has an progressing subchain.

      source
      theorem Lean4GlCoalgebras.ExtSkip.soundness (Ξ“ : SplitSequent) :
      βŠ’Ξ“ β†’ βŠ¨Ξ“

      Soundness lemma for the GL-split proof system.

      Soundness of GL-split cut proof system. #

      This soundness lemma follows by converting any GL-split proof into a GL-split cut proof.

      source
      def Lean4GlCoalgebras.Ξ±Conv (𝕏 : Split.Proof) :
      𝕏.X β†’ ExtSkip.T.obj 𝕏.X

      Converts structure morphism for GL-split proof into one for GL-split cut proofs.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem Lean4GlCoalgebras.SplitProofIsExtSkipProof (Ξ“ : SplitSequent) :
        βŠ’Ξ“ β†’ βŠ’Ξ“

        If there is a GL-split proof of Ξ“ then there is a GL-split cut proof of Ξ“.

        source
        theorem Lean4GlCoalgebras.Split.soundness (Ξ“ : SplitSequent) :
        βŠ’Ξ“ β†’ βŠ¨Ξ“

        Soundness theorem for the GL-split cut proof system.