Documentation

LeanPool.Lean4GlCoalgebras.Split.ProofTransformations

Defining GL-ext+pre proof system. #

Here we define the GL-ext+pre system. This system is different from the paper, where we build in how we connect non-axiomatic leaf nodes into RuleApp directly.

source
inductive Lean4GlCoalgebras.Ext.RuleApp {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
Type

Rule applications for the GL-ext+pre proof system.

Instances For
    source
    def Lean4GlCoalgebras.Ext.fₚ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
    RuleApp x τ → SplitSequent

    Given a RuleApp, obtain the principal formulas.

    Equations
    Instances For
      source
      def Lean4GlCoalgebras.Ext.f {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
      RuleApp x τ → SplitSequent

      Given a RuleApp, obtain the split sequent.

      Equations
      Instances For
        source
        def Lean4GlCoalgebras.Ext.fₙ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
        RuleApp x τ → SplitSequent

        Given a RuleApp, obtain the non-principal formulas.

        Equations
        Instances For
          source
          theorem Lean4GlCoalgebras.Ext.fₙ_alternate {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : RuleApp x τ) :
          fₙ r = match r with | RuleApp.pre y a => τ y | RuleApp.cutₗ Δ A => Δ | RuleApp.cutᵣ Δ A => Δ | RuleApp.wkₗ Δ A a => Δ \ {Sum.inl A} | RuleApp.wkᵣ Δ A a => Δ \ {Sum.inr A} | RuleApp.topₗ Δ a => Δ \ {Sum.inl ⊤} | RuleApp.topᵣ Δ a => Δ \ {Sum.inr ⊤} | RuleApp.axₗₗ Δ n a => Δ \ {Sum.inl (at n), Sum.inl (na n)} | RuleApp.axₗᵣ Δ n a => Δ \ {Sum.inl (at n), Sum.inr (na n)} | RuleApp.axᵣₗ Δ n a => Δ \ {Sum.inr (at n), Sum.inl (na n)} | RuleApp.axᵣᵣ Δ n a => Δ \ {Sum.inr (at n), Sum.inr (na n)} | RuleApp.andₗ Δ A B a => Δ \ {Sum.inl (A&B)} | RuleApp.andᵣ Δ A B a => Δ \ {Sum.inr (A&B)} | RuleApp.orₗ Δ A B a => Δ \ {Sum.inl (A v B)} | RuleApp.orᵣ Δ A B a => Δ \ {Sum.inr (A v B)} | RuleApp.boxₗ Δ A a => Δ \ {Sum.inl (□A)} | RuleApp.boxᵣ Δ A a => Δ \ {Sum.inr (□A)}

          Relating principal formulas, non-principal formulas, and the split sequent.

          source
          def Lean4GlCoalgebras.Ext.T {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
          CategoryTheory.Functor Type Type

          Auxiliary declaration used in the GL coalgebra development.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Lean4GlCoalgebras.Ext.r {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
            X → RuleApp x τ

            Get RuleApp of a node (first projection).

            Equations
            Instances For
              source
              def Lean4GlCoalgebras.Ext.p {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
              X → List X

              Get premises of a node (second projection).

              Equations
              Instances For
                source
                def Lean4GlCoalgebras.Ext.edge {X : Type} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
                X → (y : X) → Prop

                Edge relation induced by p.

                Equations
                Instances For
                  source
                  def Lean4GlCoalgebras.Ext.RuleApp.isBox {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
                  RuleApp x τ → Prop

                  Auxiliary declaration used in the GL coalgebra development.

                  Equations
                  Instances For
                    source
                    def Lean4GlCoalgebras.Ext.RuleApp.isNonAxLeaf {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
                    RuleApp x τ → Prop

                    Auxiliary declaration used in the GL coalgebra development.

                    Equations
                    Instances For
                      source
                      structure Lean4GlCoalgebras.Ext.PreProof {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
                      Type 1

                      Auxiliary declaration used in the GL coalgebra development.

                      Instances For
                        source
                        def Lean4GlCoalgebras.Ext.Proves {𝕏 : Split.Proof} (x : 𝕏.X) {σ : 𝕏.X → SplitSequent} (𝕐 : PreProof x σ) (Δ : SplitSequent) :
                        Prop

                        Auxiliary declaration used in the GL coalgebra development.

                        Equations
                        Instances For
                          source
                          def Lean4GlCoalgebras.proofTransformationMap {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) :
                          (y : 𝕏.X) × (partialProof y).X → ExtSkip.T.obj ((y : 𝕏.X) × (partialProof y).X)

                          Structure morphism of a proof transformation!

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Lean4GlCoalgebras.proofTransformation_f {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :
                            ExtSkip.f (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.f (Ext.r (partialProof y).α z_in_Cy)
                            source
                            @[simp]
                            theorem Lean4GlCoalgebras.proofTransformation_fₚ {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :
                            ExtSkip.fₚ (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.fₚ (Ext.r (partialProof y).α z_in_Cy)
                            source
                            @[simp]
                            theorem Lean4GlCoalgebras.proofTransformation_fₙ {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (y : 𝕏.X) (z_in_Cy : (partialProof y).X) :
                            ExtSkip.fₙ (ExtSkip.r (proofTransformationMap partialProof) ⟨y, z_in_Cy⟩) = Ext.fₙ (Ext.r (partialProof y).α z_in_Cy)
                            source
                            theorem Lean4GlCoalgebras.proofTransformation_isBox {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (z_in_Cy : (y : 𝕏.X) × (partialProof y).X) :
                            (ExtSkip.r (proofTransformationMap partialProof) z_in_Cy).isBox ↔ (Ext.r (partialProof z_in_Cy.fst).α z_in_Cy.snd).isBox
                            source
                            noncomputable def Lean4GlCoalgebras.depSumSeqProj {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) :
                            ℕ → α × ℕ

                            Auxiliary declaration used in the GL coalgebra development.

                            Equations
                            Instances For
                              source
                              theorem Lean4GlCoalgebras.sigmaMemOfMemMap {α : Type} {β : α → Type} {a : α} {xs : List (β a)} {u : (a' : α) × β a'} (hmem : u ∈ List.map (fun (b : β a) => ⟨a, b⟩) xs) :
                              ∃ (h : a = u.fst), ⋯ ▸ u.snd ∈ xs
                              source
                              theorem Lean4GlCoalgebras.sigmaCastApplyHEq {α : Type} {β : α → Type} {ρ : (a : α) → β a → Type} (r : (a : α) → (b : β a) → ρ a b) {a : α} {s t : (x : α) × β x} (ha : s.fst = a) (hst : s = t) :
                              r a (ha ▸ s.snd) ≍ r t.fst t.snd
                              source
                              theorem Lean4GlCoalgebras.sigmaMkCastEq {α : Type} {β : α → Type} {s t : (a : α) × β a} {a : α} (ha : s.fst = a) (hst : s = t) :
                              ⟨a, ha ▸ s.snd⟩ = t
                              source
                              theorem Lean4GlCoalgebras.sigmaPredicateOfEq {α : Type} {β : α → Type} {ρ : (a : α) → β a → Prop} {s t : (a : α) × β a} (hst : s = t) (h : ρ t.fst t.snd) :
                              ρ s.fst s.snd
                              source
                              theorem Lean4GlCoalgebras.sigmaRootOfEq {α : Type} {β : α → Type} (root : (a : α) → β a) {s : (a : α) × β a} {a : α} (hst : s = ⟨a, root a⟩) :
                              s.snd = root s.fst
                              source
                              theorem Lean4GlCoalgebras.transformedSuccessorRoot {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} {partialProof : (x : 𝕏.X) → Ext.PreProof x σ} {f : ℕ → (y : 𝕏.X) × (partialProof y).X} (f_succ : ∀ (n : ℕ), ExtSkip.edge (proofTransformationMap partialProof) (f n) (f (n + 1))) (i : ℕ) (hnot : ∀ (h : (f i).fst = (f (i + 1)).fst), ¬Ext.edge (partialProof (f i).fst).α (f i).snd (⋯ ▸ (f (i + 1)).snd)) :
                              (f (i + 1)).snd = (partialProof (f (i + 1)).fst).root
                              source
                              theorem Lean4GlCoalgebras.transformedFinderIsNonAxLeaf {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} {partialProof : (x : 𝕏.X) → Ext.PreProof x σ} {f : ℕ → (y : 𝕏.X) × (partialProof y).X} (f_succ : ∀ (n : ℕ), ExtSkip.edge (proofTransformationMap partialProof) (f n) (f (n + 1))) (i : ℕ) (hnot : ∀ (h : (f i).fst = (f (i + 1)).fst), ¬Ext.edge (partialProof (f i).fst).α (f i).snd (⋯ ▸ (f (i + 1)).snd)) :
                              (Ext.r (partialProof (f i).fst).α (f i).snd).isNonAxLeaf
                              source
                              theorem Lean4GlCoalgebras.infinite_dep_sum_sequence_proj_eq {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n : ℕ) :
                              (f (depSumSeqProj h n).2).fst = (depSumSeqProj h n).1
                              source
                              theorem Lean4GlCoalgebras.dep_sum_seq_proj_leq {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n : ℕ) :
                              n ≤ (depSumSeqProj h n).2
                              source
                              theorem Lean4GlCoalgebras.fst_same_in_range {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (n m : ℕ) :
                              n ≤ Nat.find ⋯ → n ≥ (depSumSeqProj h m).2 → (f (depSumSeqProj h m).2).fst = (f n).fst
                              source
                              theorem Lean4GlCoalgebras.infinite_dep_sum_chain {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {R : α → α → Prop} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (f_chain : ∀ (n : ℕ), Sigma.Lex R Q (f n) (f (n + 1))) (n : ℕ) :
                              R (depSumSeqProj h n).1 (depSumSeqProj h (n + 1)).1
                              source
                              noncomputable def Lean4GlCoalgebras.infiniteDepSumChainFiniteSubchain {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (m : ℕ) :
                              Fin (Nat.find ⋯ - (depSumSeqProj h m).2 + 1) → β (depSumSeqProj h m).1

                              Auxiliary declaration used in the GL coalgebra development.

                              Equations
                              Instances For
                                source
                                theorem Lean4GlCoalgebras.infinite_dep_sum_chain_finite_subchain_prop {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (m : ℕ) (k : Fin (Nat.find ⋯ - (depSumSeqProj h m).2)) :
                                Q (depSumSeqProj h m).1 (infiniteDepSumChainFiniteSubchain h m k.castSucc) (infiniteDepSumChainFiniteSubchain h m k.succ)
                                source
                                theorem Lean4GlCoalgebras.infinite_dep_sum_chain_inf {α : Type} {β : α → Type} {f : ℕ → (a : α) × β a} {Q : (a : α) → β a → β a → Prop} (h : ∀ (n : ℕ), ∃ m ≥ n, ∀ (h : (f m).fst = (f (m + 1)).fst), ¬Q (f m).fst (f m).snd (⋯ ▸ (f (m + 1)).snd)) (p : α → Prop) (q : (a : α) × β a → Prop) (inf : ∀ (n : ℕ), ∃ (m : ℕ), p (depSumSeqProj h (n + m)).1) (conv : ∀ (n : ℕ), p (depSumSeqProj h n).1 → ∃ (m : ℕ), q (f ((depSumSeqProj h n).2 + m))) (n : ℕ) :
                                ∃ (m : ℕ), q (f (n + m))
                                source
                                noncomputable def Lean4GlCoalgebras.proofTransformation {𝕏 : Split.Proof} {σ : 𝕏.X → SplitSequent} (partialProof : (x : 𝕏.X) → Ext.PreProof x σ) (root_prop : ∀ (x : 𝕏.X), Ext.Proves x (partialProof x) (σ x)) (box_prop : ∀ (x : 𝕏.X), (Split.r 𝕏.α x).isBox → ∀ (n : ℕ) (f : Fin (n + 1) → (partialProof x).X), f 0 = (partialProof x).root → (Ext.r (partialProof x).α (f ⟨n, ⋯⟩)).isNonAxLeaf → (∀ (m : Fin n), Ext.edge (partialProof x).α (f m.castSucc) (f m.succ)) → ∃ (m : Fin (n + 1)), (Ext.r (partialProof x).α (f m)).isBox) :
                                ExtSkip.Proof

                                Provides the proof transformation from local pre-proofs and its path witnesses.

                                Equations
                                Instances For
                                  source
                                  theorem Lean4GlCoalgebras.noInfinitePathOfIncreasing {α : Type u_1} [Preorder α] [Finite α] {relation : α → α → Prop} {f : ℕ → α} (path : ∀ (k : ℕ), relation (f k) (f (k + 1))) (increasing : ∀ (i j : α), relation i j → i < j) :
                                  False

                                  A relation that strictly increases a finite preorder has no infinite paths.