Documentation

Linglib.Theories.Syntax.Minimalism.Formal.MCB2023.FreeMagmaEquiv

The isomorphism #

source
def Minimalism.toFreeMagma :
SyntacticObject → FreeMagma LIToken

Map SO to FreeMagma: leaf ↦, node ↦ mul

Equations
Instances For
    source
    def Minimalism.fromFreeMagma :
    FreeMagma LIToken → SyntacticObject

    Map FreeMagma to SO: of ↦ leaf, mul ↦ node

    Equations
    Instances For
      source
      @[simp]
      theorem Minimalism.toFreeMagma_leaf (tok : LIToken) :
      toFreeMagma (SyntacticObject.leaf tok) = FreeMagma.of tok
      source
      @[simp]
      theorem Minimalism.toFreeMagma_node (a b : SyntacticObject) :
      toFreeMagma (a.node b) = toFreeMagma a * toFreeMagma b
      source
      @[simp]
      theorem Minimalism.fromFreeMagma_of (tok : LIToken) :
      fromFreeMagma (FreeMagma.of tok) = SyntacticObject.leaf tok
      source
      @[simp]
      theorem Minimalism.fromFreeMagma_mul (a b : FreeMagma LIToken) :
      fromFreeMagma (a * b) = (fromFreeMagma a).node (fromFreeMagma b)
      source
      theorem Minimalism.fromFreeMagma_toFreeMagma (so : SyntacticObject) :
      fromFreeMagma (toFreeMagma so) = so
      source
      theorem Minimalism.toFreeMagma_fromFreeMagma (fm : FreeMagma LIToken) :
      toFreeMagma (fromFreeMagma fm) = fm
      source
      def Minimalism.soFreeMagmaEquiv :
      SyntacticObject ≃ FreeMagma LIToken

      SyntacticObject ≃ FreeMagma LIToken — the core bridge

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Mul instance: Merge is the magma operation #

        source
        instance Minimalism.instMulSyntacticObject :
        Mul SyntacticObject
        Equations
        source
        theorem Minimalism.mul_eq_merge (x y : SyntacticObject) :
        x * y = merge x y
        source
        theorem Minimalism.mul_eq_node (x y : SyntacticObject) :
        x * y = x.node y
        source
        theorem Minimalism.merge_is_freeMagma_mul (x y : SyntacticObject) :
        toFreeMagma (merge x y) = toFreeMagma x * toFreeMagma y

        Merge is literally FreeMagma multiplication under the isomorphism (definitional)

        Magma homomorphism #

        source
        def Minimalism.toFreeMagmaMulHom :
        SyntacticObject →ₙ* FreeMagma LIToken

        toFreeMagma as a magma homomorphism

        Equations
        Instances For
          source
          def Minimalism.fromFreeMagmaMulHom :
          FreeMagma LIToken →ₙ* SyntacticObject

          fromFreeMagma as a magma homomorphism

          Equations
          Instances For

            Universal property #

            SyntacticObject satisfies the same universal property as FreeMagma: any function LIToken → M (where M is a magma) extends uniquely to a magma homomorphism SyntacticObject →ₙ* M.

            source
            def Minimalism.SyntacticObject.liftMagma {M : Type u_1} [Mul M] (f : LIToken → M) :
            SyntacticObject →ₙ* M

            Universal property: lift a function LIToken → M to a magma hom SO →ₙ* M

            Equations
            Instances For
              source
              theorem Minimalism.SyntacticObject.liftMagma_leaf {M : Type u_1} [Mul M] (f : LIToken → M) (tok : LIToken) :
              (liftMagma f) (leaf tok) = f tok
              source
              theorem Minimalism.SyntacticObject.liftMagma_node {M : Type u_1} [Mul M] (f : LIToken → M) (a b : SyntacticObject) :
              (liftMagma f) (a.node b) = (liftMagma f) a * (liftMagma f) b

              Containment ↔ proper subterm #

              Connect contains (Containment.lean) with subterm structure in the free magma.

              source
              inductive Minimalism.properSubterm :
              SyntacticObject → SyntacticObject → Prop

              An SO is a proper subterm of another iff it appears strictly within it

              Instances For
                source
                theorem Minimalism.immediatelyContains_implies_properSubterm {x y : SyntacticObject} (h : immediatelyContains x y) :
                properSubterm y x

                Immediate containment implies proper subterm

                source
                theorem Minimalism.contains_implies_properSubterm {x y : SyntacticObject} (h : contains x y) :
                properSubterm y x

                Containment implies proper subterm

                source
                theorem Minimalism.properSubterm_implies_contains {x y : SyntacticObject} (h : properSubterm x y) :
                contains y x

                Proper subterm implies containment

                source
                theorem Minimalism.contains_iff_properSubterm (x y : SyntacticObject) :
                contains x y ↔ properSubterm y x

                Containment = proper subterm (the key bridge theorem)

                source
                theorem Minimalism.toFreeMagma_injective :
                Function.Injective toFreeMagma

                toFreeMagma is injective

                source
                theorem Minimalism.toFreeMagma_preserves_structure (so : SyntacticObject) :
                so.leafCount = match toFreeMagma so with | FreeMagma.of a => 1 | a.mul b => (fromFreeMagma a).leafCount + (fromFreeMagma b).leafCount

                nodeCount is preserved by the isomorphism

                Bridge to FreeMagma.length #

                FreeMagma.length counts leaves (1 for .of, sum for .mul), matching SyntacticObject.leafCount exactly under the isomorphism. This gives access to mathlib's FreeMagma.length_pos for free.

                source
                theorem Minimalism.leafCount_eq_freeMagma_length (so : SyntacticObject) :
                so.leafCount = (toFreeMagma so).length

                SO.leafCount = FreeMagma.length under the isomorphism

                source
                theorem Minimalism.leafCount_pos (so : SyntacticObject) :
                0 < so.leafCount

                leafCount is always positive — derived from mathlib's FreeMagma.length_pos