Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Reduction to co-pairings of guarded terms

Lax149335.GuardedReduction · concepts/Lax149335/GuardedReduction.lean · lax-149335

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Lemma

    Lemma 6.4. In the proof of the conjugacy rule of Lemma 6.1, let k≥1k \geq 1 be the length of ww. Without loss of generality, ff and gg are co-pairings

    ⟨f1,…,fn⟩and⟨g1,…,gn⟩for some k-guarded terms fi,gi:Ai→B∗.\langle f_1, \ldots, f_n \rangle \quad\text{and}\quad \langle g_1, \ldots, g_n \rangle \qquad\text{for some $k$-guarded terms } f_i, g_i : A_i \to B^*.
    Concept map
    7 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax149335.GuardedTerms
    2
    3/-!
    4---
    5title: Reduction to co-pairings of guarded terms
    6type: lemma
    7---
    8**Lemma 6.4.** In the proof of the conjugacy rule of Lemma 6.1, let k≥1k \geq 1 be the length
    9of ww. Without loss of generality, ff and gg are co-pairings
    10
    11⟨f1,…,fn⟩and⟨g1,…,gn⟩for some k-guarded terms fi,gi:Ai→B∗.\langle f_1, \ldots, f_n \rangle \quad\text{and}\quad \langle g_1, \ldots, g_n \rangle \qquad\text{for some $k$-guarded terms } f_i, g_i : A_i \to B^*.
    12
    13
    14
    15# Formalization notes
    16
    17The "without loss of generality" is formalised as a reduction: if the conjugacy rule
    18f⋅w≡w⋅g⇒(hom f)⋅w≡w⋅(hom g)f \cdot w \equiv w \cdot g \Rightarrow (\mathrm{hom}\, f) \cdot w \equiv w \cdot (\mathrm{hom}\, g)
    19 holds for all such co-pairings, then it holds for all simple rational
    20terms f,g:A→B∗f, g : A \to B^*. The proof of Lemma 6.1 is an induction on the nesting depth of
    21lists in the input type, so the reduction is stated with the additional guarantee that the
    22co-pairings have an input type whose nesting depth is at most that of AA. The assumption
    23that BB is a finite alphabet is not needed.
    24-/
    25
    26namespace Lax149335.GuardedReduction
    27
    28open Lax149335.Types Lax149335.Terms Lax149335.DerivedTerms Lax149335.DerivedTerms.Term
    29 Lax149335.EquationalTheory Lax149335.SimpleRationalWithinSyntax Lax149335.GuardedTerms
    30
    31/-- **Lemma 6.4.** The conjugacy rule for simple rational terms follows from the conjugacy
    32rule for co-pairings of `k`-guarded terms, where `k > 0` is the length of `w`. -/
    33axiom wlog_kguarded {B : Ty} (w : Value B⋆) (hw : 0 < valLength w) {A : Ty}
    34 (H : ∀ (A₀ : Ty) (As : List Ty) (f₀ g₀ : Term A₀ B⋆) (fs gs : Cases B⋆ As),
    35 Ty.listDepth (sumTyOf A₀ As) ≤ Ty.listDepth A →
    36 KGuarded (valLength w) B f₀ → KGuarded (valLength w) B g₀ →
    37 fs.All (fun _ f => KGuarded (valLength w) B f) →
    38 gs.All (fun _ g => KGuarded (valLength w) B g) →
    39 dotR (copair f₀ fs) w ≡ₜ dotL w (copair g₀ gs) →
    40 dotR (homT (copair f₀ fs)) w ≡ₜ dotL w (homT (copair g₀ gs)))
    41 (f g : Term A B⋆) (hf : IsSimple B f) (hg : IsSimple B g)
    42 (hfg : dotR f w ≡ₜ dotL w g) :
    43 dotR (homT f) w ≡ₜ dotL w (homT g)
    44
    45end Lax149335.GuardedReduction
    46
    Show Proof
    Formalization notes

    The "without loss of generality" is formalised as a reduction: if the conjugacy rule f⋅w≡w⋅g⇒(hom f)⋅w≡w⋅(hom g)f \cdot w \equiv w \cdot g \Rightarrow (\mathrm{hom}\, f) \cdot w \equiv w \cdot (\mathrm{hom}\, g) holds for all such co-pairings, then it holds for all simple rational terms f,g:A→B∗f, g : A \to B^*. The proof of Lemma 6.1 is an induction on the nesting depth of lists in the input type, so the reduction is stated with the additional guarantee that the co-pairings have an input type whose nesting depth is at most that of AA. The assumption that BB is a finite alphabet is not needed.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…