Documentation

GL.Split.ProofTransformations

source
inductive CutPre.RuleApp {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
Type
Instances For
    source
    def CutPre.fₚ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
    RuleApp x τ → SplitSequent
    Equations
    Instances For
      source
      def CutPre.f {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
      RuleApp x τ → SplitSequent
      Equations
      Instances For
        source
        def CutPre.fₙ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
        RuleApp x τ → SplitSequent
        Equations
        Instances For
          source
          theorem CutPre.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)}
          source
          def CutPre.T {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
          CategoryTheory.Functor (Type u) (Type u)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CutPre.r {X : Type u} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
            X → RuleApp x τ
            Equations
            Instances For
              source
              def CutPre.p {X : Type u} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
              X → List X
              Equations
              Instances For
                source
                def CutPre.edge {X : Type u} {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (α : X → (T x τ).obj X) :
                X → (y : X) → Prop
                Equations
                Instances For
                  source
                  def CutPre.RuleApp.isBox {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
                  RuleApp x τ → Prop
                  Equations
                  Instances For
                    source
                    def CutPre.RuleApp.isNonAxLeaf {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} :
                    RuleApp x τ → Prop
                    Equations
                    Instances For
                      source
                      structure CutPre.CutProofFromPremises {𝕏 : Split.Proof} (x : 𝕏.X) (τ : 𝕏.X → SplitSequent) :
                      Type 1
                      Instances For
                        source
                        def Split.CutPre.Proves {𝕏 : Proof} (x : 𝕏.X) {σ : 𝕏.X → SplitSequent} (𝕐 : CutPre.CutProofFromPremises x σ) (Δ : SplitSequent) :
                        Prop
                        Equations
                        Instances For
                          source
                          def Split.ProofTransformationMap {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) :
                          (y : 𝕏.X) × (PartialProof y).X → SplitCut.T.obj ((y : 𝕏.X) × (PartialProof y).X)
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            @[simp]
                            theorem Split.ProofTransformation_f {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) (y : 𝕏.X) (z_in_Cy : (PartialProof y).X) :
                            SplitCut.f (SplitCut.r (ProofTransformationMap PartialProof) ⟨y, z_in_Cy⟩) = CutPre.f (CutPre.r (PartialProof y).α z_in_Cy)
                            source
                            @[simp]
                            theorem Split.ProofTransformation_fₚ {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) (y : 𝕏.X) (z_in_Cy : (PartialProof y).X) :
                            SplitCut.fₚ (SplitCut.r (ProofTransformationMap PartialProof) ⟨y, z_in_Cy⟩) = CutPre.fₚ (CutPre.r (PartialProof y).α z_in_Cy)
                            source
                            @[simp]
                            theorem Split.ProofTransformation_fₙ {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) (y : 𝕏.X) (z_in_Cy : (PartialProof y).X) :
                            SplitCut.fₙ (SplitCut.r (ProofTransformationMap PartialProof) ⟨y, z_in_Cy⟩) = CutPre.fₙ (CutPre.r (PartialProof y).α z_in_Cy)
                            source
                            theorem Split.ProofTransformation_isBox {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) (z_in_Cy : (y : 𝕏.X) × (PartialProof y).X) :
                            (SplitCut.r (ProofTransformationMap PartialProof) z_in_Cy).isBox ↔ (CutPre.r (PartialProof z_in_Cy.fst).α z_in_Cy.snd).isBox
                            source
                            noncomputable def Split.dep_sum_seq_proj {α : 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)) :
                            ℕ → α × ℕ
                            Equations
                            Instances For
                              source
                              theorem Split.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 (dep_sum_seq_proj h n).2).fst = (dep_sum_seq_proj h n).1
                              source
                              theorem Split.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 ≤ (dep_sum_seq_proj h n).2
                              source
                              theorem Split.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 ≥ (dep_sum_seq_proj h m).2 → (f (dep_sum_seq_proj h m).2).fst = (f n).fst
                              source
                              theorem Split.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 (dep_sum_seq_proj h n).1 (dep_sum_seq_proj h (n + 1)).1
                              source
                              noncomputable def Split.infinite_dep_sum_chain_finite_subchain {α : 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 ⋯ - (dep_sum_seq_proj h m).2 + 1) → β (dep_sum_seq_proj h m).1
                              Equations
                              Instances For
                                source
                                theorem Split.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 ⋯ - (dep_sum_seq_proj h m).2)) :
                                Q (dep_sum_seq_proj h m).1 (infinite_dep_sum_chain_finite_subchain h m k.castSucc) (infinite_dep_sum_chain_finite_subchain h m k.succ)
                                source
                                theorem Split.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 (dep_sum_seq_proj h (n + m)).1) (conv : ∀ (n : ℕ), p (dep_sum_seq_proj h n).1 → ∃ (m : ℕ), q (f ((dep_sum_seq_proj h n).2 + m))) (n : ℕ) :
                                ∃ (m : ℕ), q (f (n + m))
                                source
                                noncomputable def Split.ProofTransformation {𝕏 : Proof} {σ : 𝕏.X → SplitSequent} (PartialProof : (x : 𝕏.X) → CutPre.CutProofFromPremises x σ) (root_proves : ∀ (x : 𝕏.X), CutPre.Proves x (PartialProof x) (σ x)) (box_prop : ∀ (x : 𝕏.X), (r 𝕏.α x).isBox → ∀ (n : ℕ) (f : Fin (n + 1) → (PartialProof x).X), f 0 = (PartialProof x).root → (CutPre.r (PartialProof x).α (f ⟨n, ⋯⟩)).isNonAxLeaf → (∀ (m : Fin n), CutPre.edge (PartialProof x).α (f m.castSucc) (f m.succ)) → ∃ (m : Fin (n + 1)), (CutPre.r (PartialProof x).α (f m)).isBox) :
                                SplitCut.Proof
                                Equations
                                Instances For