Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedIndexQuotient

Supporting results for pointwise provable equality.

The generated quotient of program indices is a monoid, with multiplication given by the compiler's composition operation. Interpreting indices as functional graphs gives a monoid equivalence to the generated graph quotient.

source
def PointwiseComposition.FailureOfComposition.ProgramIndices.GeneratedIndexQuotient (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
Type

Program indices modulo the generated composition congruence.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ProgramIndices.generatedIndexMk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) (e : ℕ) :
    GeneratedIndexQuotient A T

    The class of a program index.

    Equations
    Instances For
      source
      theorem PointwiseComposition.FailureOfComposition.ProgramIndices.realizationIndex_respects_generated (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] {F G : ProofSearch.FunctionalGraph} (h : GeneratedCongruence.Rel T F G) :
      GeneratedRel A T (realizationIndex A F) (realizationIndex A G)
      source
      noncomputable def PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientEquiv (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
      GeneratedIndexQuotient A T ≃ GeneratedCongruence.QuotientGraph T

      Graph interpretation and chosen PA realizers give inverse maps on the generated quotients.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientEquiv_mk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e : ℕ) :
        (generatedQuotientEquiv A T) (generatedIndexMk A T e) = GeneratedCongruence.quotientMk T ⟨A.graph e, ⋯⟩
        source
        @[simp]
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientEquiv_symm_mk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (F : ProofSearch.FunctionalGraph) :
        (generatedQuotientEquiv A T).symm (GeneratedCongruence.quotientMk T F) = generatedIndexMk A T (realizationIndex A F)
        source
        @[instance_reducible]
        instance PointwiseComposition.FailureOfComposition.ProgramIndices.instMulGeneratedIndexQuotient (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
        Mul (GeneratedIndexQuotient A T)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[instance_reducible]
        noncomputable instance PointwiseComposition.FailureOfComposition.ProgramIndices.instOneGeneratedIndexQuotient (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
        One (GeneratedIndexQuotient A T)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        @[simp]
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedIndexQuotient_mul_mk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) (e d : ℕ) :
        generatedIndexMk A T e * generatedIndexMk A T d = generatedIndexMk A T (A.compIndex e d)
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedIndexQuotient_one_mk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) :
        1 = generatedIndexMk A T (realizationIndex A GeneratedCongruence.identityGraph)
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientEquiv_mul (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (a b : GeneratedIndexQuotient A T) :
        (generatedQuotientEquiv A T) (a * b) = (generatedQuotientEquiv A T) a * (generatedQuotientEquiv A T) b
        source
        theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientEquiv_one (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        (generatedQuotientEquiv A T) 1 = 1
        source
        @[instance_reducible]
        noncomputable instance PointwiseComposition.FailureOfComposition.ProgramIndices.generatedIndexQuotientMonoid (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        Monoid (GeneratedIndexQuotient A T)
        Equations
        • One or more equations did not get rendered due to their size.
        source
        noncomputable def PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientMulEquiv (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
        GeneratedIndexQuotient A T ≃* GeneratedCongruence.QuotientGraph T

        The index and graph quotients are equivalent as monoids.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedQuotientMulEquiv_mk (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (e : ℕ) :
          (generatedQuotientMulEquiv A T) (generatedIndexMk A T e) = GeneratedCongruence.quotientMk T ⟨A.graph e, ⋯⟩
          source
          theorem PointwiseComposition.FailureOfComposition.ProgramIndices.generatedIndexQuotient_subsingleton_of_graph_universal (A : Arithmetization) (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] (h : ∀ (F G : ProofSearch.FunctionalGraph), GeneratedCongruence.Rel T F G) :
          Subsingleton (GeneratedIndexQuotient A T)

          Universality on functional graphs also collapses the index quotient.