Documentation

LeanPool.PointwiseComposition.FailureOfComposition.GeneratedQuotient

Supporting results for pointwise provable equality.

Composition descends to the quotient by the generated congruence. The PA proofs of associativity and the identity laws make this quotient a monoid for every theory extending PA. A universal congruence gives a singleton quotient.

source
def PointwiseComposition.FailureOfComposition.GeneratedCongruence.QuotientGraph (T : FFL.FirstOrder.ArithmeticTheory) :
Type

PA-functional Sigma-one graphs modulo the generated composition congruence.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotientMk (T : FFL.FirstOrder.ArithmeticTheory) (F : ProofSearch.FunctionalGraph) :
    QuotientGraph T

    The class of a functional graph.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance PointwiseComposition.FailureOfComposition.GeneratedCongruence.instMulQuotientGraph (T : FFL.FirstOrder.ArithmeticTheory) :
      Mul (QuotientGraph T)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[instance_reducible]
      instance PointwiseComposition.FailureOfComposition.GeneratedCongruence.instOneQuotientGraph (T : FFL.FirstOrder.ArithmeticTheory) :
      One (QuotientGraph T)
      Equations
      source
      @[simp]
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotient_mul_mk (T : FFL.FirstOrder.ArithmeticTheory) (F G : ProofSearch.FunctionalGraph) :
      quotientMk T F * quotientMk T G = quotientMk T (ProofSearch.functionalComp F G)
      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.one_mk (T : FFL.FirstOrder.ArithmeticTheory) :
      1 = quotientMk T identityGraph
      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.comp_associative_uniform (F G H : ProofSearch.Graph) :
      ProofSearch.Uniform 𝐏𝐀 (ProofSearch.comp (ProofSearch.comp F G) H) (ProofSearch.comp F (ProofSearch.comp G H))

      Composition of graph formulas is associative already in PA.

      source
      @[instance_reducible]
      instance PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotientMonoid (T : FFL.FirstOrder.ArithmeticTheory) [𝐏𝐀 ≼ T] :
      Monoid (QuotientGraph T)
      Equations
      • One or more equations did not get rendered due to their size.
      source
      theorem PointwiseComposition.FailureOfComposition.GeneratedCongruence.quotient_subsingleton_of_universal (T : FFL.FirstOrder.ArithmeticTheory) (h : ∀ (F G : ProofSearch.FunctionalGraph), Rel T F G) :
      Subsingleton (QuotientGraph T)

      If all functional graphs are related, every two quotient elements are equal. Together with the identity element, this makes the quotient a singleton.