Lax Lean Archive

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

Conjugacy completeness

Lax149335.ConjugacyCompleteness · concepts/Lax149335/ConjugacyCompleteness.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

    Theorem

    Theorem 2.6 (Conjugacy completeness). Two simple rational terms define the same function if and only if they are equivalent with respect to the least equivalence relation ≡\equiv on simple rational terms that satisfies the following rules (where f,g,hf, g, h are simple rational terms, w,vw, v are strings and ε\varepsilon is the empty string):

    1. Congruence: ≡\equiv is preserved by co-pairing, concatenation, homomorphism and adding constants.
    2. Concatenation monoidality: (f⋅w)⋅v≡f⋅wv(f \cdot w) \cdot v \equiv f \cdot wv, w⋅(v⋅f)≡wv⋅fw \cdot (v \cdot f) \equiv wv \cdot f, f⋅ε≡f≡ε⋅ff \cdot \varepsilon \equiv f \equiv \varepsilon \cdot f, (w⋅f)⋅v≡w⋅(f⋅v)(w \cdot f) \cdot v \equiv w \cdot (f \cdot v), (f⋅w)⊙g≡f⊙(w⋅g)(f \cdot w) \odot g \equiv f \odot (w \cdot g), w⋅(f⊙g)≡(w⋅f)⊙gw \cdot (f \odot g) \equiv (w \cdot f) \odot g, (f⊙g)⋅w≡f⊙(g⋅w)(f \odot g) \cdot w \equiv f \odot (g \cdot w), and []⋅w≡w⋅[][] \cdot w \equiv w \cdot [].
    3. Constants and co-pairing: w⋅⟨f1,f2⟩≡⟨w⋅f1,w⋅f2⟩w \cdot \langle f_1, f_2 \rangle \equiv \langle w \cdot f_1, w \cdot f_2 \rangle and ⟨f1,f2⟩⋅w≡⟨f1⋅w,f2⋅w⟩\langle f_1, f_2 \rangle \cdot w \equiv \langle f_1 \cdot w, f_2 \cdot w \rangle.
    4. Case splitting: if ⟨f1⊙h,f2⊙h⟩≡⟨g1⊙h,g2⊙h⟩\langle f_1 \odot h, f_2 \odot h \rangle \equiv \langle g_1 \odot h, g_2 \odot h \rangle then ⟨f1,f2⟩⊙h≡⟨g1,g2⟩⊙h\langle f_1, f_2 \rangle \odot h \equiv \langle g_1, g_2 \rangle \odot h, and symmetrically on the other side.
    5. Conjugacy: if f⋅w≡w⋅gf \cdot w \equiv w \cdot g then (hom f)⋅w≡w⋅(hom g)(\mathrm{hom}\, f) \cdot w \equiv w \cdot (\mathrm{hom}\, g).
    Concept map
    3 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.SimpleRationalTerms
    2
    3/-!
    4---
    5title: Conjugacy completeness
    6type: theorem
    7---
    8**Theorem 2.6 (Conjugacy completeness).** Two simple rational terms define the same function
    9if and only if they are equivalent with respect to the least equivalence relation ≡\equiv
    10on simple rational terms that satisfies the following rules (where f,g,hf, g, h are simple
    11rational terms, w,vw, v are strings and ε\varepsilon is the empty string):
    12
    131. *Congruence:* ≡\equiv is preserved by co-pairing, concatenation, homomorphism and
    14 adding constants.
    152. *Concatenation monoidality:* (f⋅w)⋅v≡f⋅wv(f \cdot w) \cdot v \equiv f \cdot wv,
    16 w⋅(v⋅f)≡wv⋅fw \cdot (v \cdot f) \equiv wv \cdot f, f⋅ε≡f≡ε⋅ff \cdot \varepsilon \equiv f \equiv \varepsilon \cdot f
    17, (w⋅f)⋅v≡w⋅(f⋅v)(w \cdot f) \cdot v \equiv w \cdot (f \cdot v),
    18 (f⋅w)⊙g≡f⊙(w⋅g)(f \cdot w) \odot g \equiv f \odot (w \cdot g),
    19 w⋅(f⊙g)≡(w⋅f)⊙gw \cdot (f \odot g) \equiv (w \cdot f) \odot g,
    20 (f⊙g)⋅w≡f⊙(g⋅w)(f \odot g) \cdot w \equiv f \odot (g \cdot w), and
    21 []⋅w≡w⋅[][] \cdot w \equiv w \cdot [].
    223. *Constants and co-pairing:* w⋅⟨f1,f2⟩≡⟨w⋅f1,w⋅f2⟩w \cdot \langle f_1, f_2 \rangle \equiv \langle w \cdot f_1, w \cdot f_2 \rangle
    23 and ⟨f1,f2⟩⋅w≡⟨f1⋅w,f2⋅w⟩\langle f_1, f_2 \rangle \cdot w \equiv \langle f_1 \cdot w, f_2 \cdot w \rangle
    24.
    254. *Case splitting:* if ⟨f1⊙h,f2⊙h⟩≡⟨g1⊙h,g2⊙h⟩\langle f_1 \odot h, f_2 \odot h \rangle \equiv \langle g_1 \odot h, g_2 \odot h \rangle
    26 then
    27 ⟨f1,f2⟩⊙h≡⟨g1,g2⟩⊙h\langle f_1, f_2 \rangle \odot h \equiv \langle g_1, g_2 \rangle \odot h, and
    28 symmetrically on the other side.
    295. *Conjugacy:* if f⋅w≡w⋅gf \cdot w \equiv w \cdot g then
    30 (hom f)⋅w≡w⋅(hom g)(\mathrm{hom}\, f) \cdot w \equiv w \cdot (\mathrm{hom}\, g).
    31-/
    32
    33namespace Lax149335.ConjugacyCompleteness
    34
    35open Lax149335.Types Lax149335.SimpleRationalTerms
    36
    37namespace SimpleTerm
    38
    39/-- The equivalence `≡` of simple rational terms from Theorem 2.6: the least relation closed
    40under (1) congruence, (2) concatenation monoidality, (3) constants and co-pairing, (4) case
    41splitting and (5) conjugacy. -/
    42inductive SEq {Bs : Type} : {A : Ty} → SimpleTerm Bs A → SimpleTerm Bs A → Prop
    43 -- (1) congruence, together with the equivalence relation rules
    44 | refl {A : Ty} (f : SimpleTerm Bs A) : SEq f f
    45 | symm {A : Ty} {f g : SimpleTerm Bs A} : SEq f g → SEq g f
    46 | trans {A : Ty} {f g h : SimpleTerm Bs A} : SEq f g → SEq g h → SEq f h
    47 | congr_either {A₁ A₂ : Ty} {f₁ g₁ : SimpleTerm Bs A₁} {f₂ g₂ : SimpleTerm Bs A₂} :
    48 SEq f₁ g₁ → SEq f₂ g₂ → SEq (.either f₁ f₂) (.either g₁ g₂)
    49 | congr_conc {A₁ A₂ : Ty} {f₁ g₁ : SimpleTerm Bs A₁} {f₂ g₂ : SimpleTerm Bs A₂} :
    50 SEq f₁ g₁ → SEq f₂ g₂ → SEq (.conc f₁ f₂) (.conc g₁ g₂)
    51 | congr_hom {A : Ty} {f g : SimpleTerm Bs A} : SEq f g → SEq (.hom f) (.hom g)
    52 | congr_pre {A : Ty} {f g : SimpleTerm Bs A} (w : List Bs) :
    53 SEq f g → SEq (.pre w f) (.pre w g)
    54 | congr_post {A : Ty} {f g : SimpleTerm Bs A} (w : List Bs) :
    55 SEq f g → SEq (.post f w) (.post g w)
    56 -- (2) concatenation monoidality
    57 | post_post {A : Ty} (f : SimpleTerm Bs A) (w v : List Bs) :
    58 SEq (.post (.post f w) v) (.post f (w ++ v))
    59 | pre_pre {A : Ty} (f : SimpleTerm Bs A) (w v : List Bs) :
    60 SEq (.pre w (.pre v f)) (.pre (w ++ v) f)
    61 | post_nil {A : Ty} (f : SimpleTerm Bs A) : SEq (.post f []) f
    62 | pre_nil {A : Ty} (f : SimpleTerm Bs A) : SEq (.pre [] f) f
    63 | pre_post {A : Ty} (f : SimpleTerm Bs A) (w v : List Bs) :
    64 SEq (.post (.pre w f) v) (.pre w (.post f v))
    65 | conc_shift {A₁ A₂ : Ty} (f : SimpleTerm Bs A₁) (g : SimpleTerm Bs A₂) (w : List Bs) :
    66 SEq (.conc (.post f w) g) (.conc f (.pre w g))
    67 | pre_conc {A₁ A₂ : Ty} (w : List Bs) (f₁ : SimpleTerm Bs A₁) (f₂ : SimpleTerm Bs A₂) :
    68 SEq (.pre w (.conc f₁ f₂)) (.conc (.pre w f₁) f₂)
    69 | post_conc {A₁ A₂ : Ty} (w : List Bs) (f₁ : SimpleTerm Bs A₁) (f₂ : SimpleTerm Bs A₂) :
    70 SEq (.post (.conc f₁ f₂) w) (.conc f₁ (.post f₂ w))
    71 | move_empty (w : List Bs) :
    72 SEq (.post (.empty : SimpleTerm Bs Ty.unit) w) (.pre w .empty)
    73 -- (3) constants and copairing
    74 | pre_either {A₁ A₂ : Ty} (w : List Bs) (f₁ : SimpleTerm Bs A₁) (f₂ : SimpleTerm Bs A₂) :
    75 SEq (.pre w (.either f₁ f₂)) (.either (.pre w f₁) (.pre w f₂))
    76 | post_either {A₁ A₂ : Ty} (w : List Bs) (f₁ : SimpleTerm Bs A₁) (f₂ : SimpleTerm Bs A₂) :
    77 SEq (.post (.either f₁ f₂) w) (.either (.post f₁ w) (.post f₂ w))
    78 -- (4) case splitting
    79 | case_left {A₁ A₂ A : Ty} {f₁ g₁ : SimpleTerm Bs A₁} {f₂ g₂ : SimpleTerm Bs A₂}
    80 {h : SimpleTerm Bs A} :
    81 SEq (.either (.conc f₁ h) (.conc f₂ h)) (.either (.conc g₁ h) (.conc g₂ h)) →
    82 SEq (.conc (.either f₁ f₂) h) (.conc (.either g₁ g₂) h)
    83 | case_right {A₁ A₂ A : Ty} {f₁ g₁ : SimpleTerm Bs A₁} {f₂ g₂ : SimpleTerm Bs A₂}
    84 {h : SimpleTerm Bs A} :
    85 SEq (.either (.conc h f₁) (.conc h f₂)) (.either (.conc h g₁) (.conc h g₂)) →
    86 SEq (.conc h (.either f₁ f₂)) (.conc h (.either g₁ g₂))
    87 -- (5) conjugacy
    88 | conjugacy {A : Ty} {f g : SimpleTerm Bs A} (w : List Bs) :
    89 SEq (.post f w) (.pre w g) → SEq (.post (.hom f) w) (.pre w (.hom g))
    90
    91/-- Notation `f ≃ₛ g` for the equivalence of simple rational terms. -/
    92infix:50 " ≃ₛ " => SEq
    93
    94end SimpleTerm
    95
    96/-- **Theorem 2.6.** Two simple rational terms define the same function if and only if they
    97are equivalent. -/
    98axiom conjugacy_completeness {Bs : Type} {A : Ty} (f g : SimpleTerm Bs A) :
    99 f.den = g.den ↔ f ≃ₛ g
    100
    101end Lax149335.ConjugacyCompleteness
    102
    Show Proof
    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…