Lax Lean Archive

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

Provable simplification of drops

Lax149335.DropsJointSimplification · concepts/Lax149335/DropsJointSimplification.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 7.3 (Provable simplification of drops). Let NN be a finite alphabet, and let f,g:A→N∗f, g : A \to N^* be drops. There is a lift π:A→C\pi : A \to C and its inverse π−1\pi^{-1} such that π−1;f\pi^{-1} \mathbin{;} f and π−1;g\pi^{-1} \mathbin{;} g are both equivalent to simple rational terms.

    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.LiftsAndDrops
    2import Lax149335.SimpleRationalWithinSyntax
    3
    4/-!
    5---
    6title: Provable simplification of drops
    7type: lemma
    8---
    9**Lemma 7.3 (Provable simplification of drops).** Let NN be a finite alphabet, and let
    10f,g:A→N∗f, g : A \to N^* be drops. There is a lift π:A→C\pi : A \to C and its inverse π−1\pi^{-1} such
    11that π−1;f\pi^{-1} \mathbin{;} f and π−1;g\pi^{-1} \mathbin{;} g are both equivalent to simple
    12rational terms.
    13
    14# Formalization notes
    15
    16The statement records that π−1\pi^{-1} is a drop and that π\pi and π−1\pi^{-1} are mutually
    17inverse.
    18-/
    19
    20namespace Lax149335.DropsJointSimplification
    21
    22open Lax149335.Types Lax149335.Terms Lax149335.EquationalTheory Lax149335.LiftsAndDrops
    23 Lax149335.SimpleRationalWithinSyntax
    24
    25/-- **Lemma 7.3.** Two drops `A → N*` into the lists over a finite alphabet become provably
    26equivalent to simple rational terms after precomposing with the inverse of a common lift. -/
    27axiom drops_to_simple {A B : Ty} (hB : Ty.IsFinAlph B) (f g : Term A B⋆)
    28 (hf : IsDrop f) (hg : IsDrop g) :
    29 ∃ (C : Ty) (l : Term A C) (π : Term C A),
    30 IsLift l ∧ IsDrop π ∧ (l ⨟ π) ≡ₜ Term.id A ∧ (π ⨟ l) ≡ₜ Term.id C ∧
    31 (∃ f' : Term C B⋆, IsSimple B f' ∧ (π ⨟ f) ≡ₜ f') ∧
    32 (∃ g' : Term C B⋆, IsSimple B g' ∧ (π ⨟ g) ≡ₜ g')
    33
    34end Lax149335.DropsJointSimplification
    35
    Show Proof
    Formalization notes

    The statement records that π−1\pi^{-1} is a drop and that π\pi and π−1\pi^{-1} are mutually inverse.

    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…