Chained equations for the monoid case¶

We check whether the equations in the monoid case from the base and the tangent together generate the expected proof. We first replicate that case and check a few additional things.

import $cp.bin.`provingground-core-jvm-65045ead6d.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._

val tg1 = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)
import library._, MonoidSimple._
val ts = TermState(dist1, dist1.map(_.typ))

tg1: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0
)
import library._, MonoidSimple._

ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e_l, 0.047619047619047616),
      Weighted(e_r, 0.047619047619047616),
      Weighted(mul, 0.047619047619047616),
      Weighted(eqM, 0.047619047619047616),
      Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.047619047619047616
      ),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
      Weighted(eqM, 0.2857142857142857),
      Weighted(mul, 0.2857142857142857)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.047619047619047616),
      Weighted(M, 0.047619047619047616),
      Weighted((M → (M → M)), 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.047619047619047616),
      Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.047619047619047616
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.047619047619047616
      ),
      Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.2857142857142857),
      Weighted((M → (M → M)), 0.2857142857142857)
...

import monix.execution.Scheduler.Implicits.global

import monix.execution.Scheduler.Implicits.global

val lp1 = LocalProver(ts, tg1)

lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e_l, 0.047619047619047616),
        Weighted(e_r, 0.047619047619047616),
        Weighted(mul, 0.047619047619047616),
        Weighted(eqM, 0.047619047619047616),
        Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.047619047619047616
        ),
        Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
        Weighted(eqM, 0.2857142857142857),
        Weighted(mul, 0.2857142857142857)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.047619047619047616),
        Weighted(M, 0.047619047619047616),
        Weighted((M → (M → M)), 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.047619047619047616),
        Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.047619047619047616
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.047619047619047616
        ),
        Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.2857142857142857),
...

val lemT1 = lp1.lemmas
lemT1.runToFuture

lemT1: monix.eval.Task[Vector[(Typ[Term], Double)]] = Async(
  <function2>,
  false,
  true,
  true
)
res4_1: monix.execution.CancelableFuture[Vector[(Typ[Term], Double)]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Vector(
    (eqM(e_r)(e_r), 0.0027509184472828325),
    (eqM(e_l)(e_l), 0.0027509184472828325),
    (eqM(e_l)(mul(e_l)(e_r)), 0.0012526844961492322),
    (eqM(e_l)(mul(e_l)(e_l)), 0.0012526844961492322),
    (eqM(e_r)(mul(e_l)(e_r)), 0.0012526844961492322),
    (eqM(e_r)(mul(e_r)(e_r)), 0.0012526844961492322)
  )
)

val lem = eqM(l)(op(l)(r))
val termsT = lp1.expressionEval.map(_.finalTerms)
termsT.runToFuture

lem: Typ[Term] = eqM(e_l)(mul(e_l)(e_r))
termsT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd5$Helper$$Lambda$2963/1340067789@13139dd5,
  0
)
res5_2: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{eqM(mul(e_l)(a))(a)}(mul(e_r)(e_l)),
        1.0211226571848244E-4
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)(mul(e_l)(e_l)),
        1.43204259042601E-5
      ),
      Weighted(
        ($auni : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_r))(e_r)($auni)(axiom_{eqM(mul(a)(e_r))(a)}(e_r)),
        2.5311163260347958E-5
      ),
      Weighted(mul, 0.26757575953354795),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)(mul(e_r)(e_l)),
        1.4320425904260095E-5
      ),
      Weighted(eqM(e_r)(mul(e_l)(e_l)), 6.21690603886337E-4),
      Weighted(e_r, 0.03822510850479257),
      Weighted(eqM(e_r)(mul(e_r)(e_l)), 6.216906038863368E-4),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_r)(e_l)),
        1.0211226571848244E-4
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_l))(e_l)(axiom_{eqM(mul(e_l)(a))(a)}(e_l)),
        2.5311163260347958E-5
      ),
      Weighted(axiom_{eqM(a)(a)}, 0.03822510850479257),
      Weighted(
        ($ecdz : eqM(e_r)($ecdb)) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)(mul(e_l)(e_l))(e_l)($ecdz)(axiom_{eqM(mul(e_l)(a))(a)}(e_l)),
        1.1832291823450562E-6
      ),
...

val pfsT = termsT.map(_.filter(_.typ == lem))
pfsT.runToFuture

pfsT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$312/951031848@51772539,
  1
)
res6_1: monix.execution.CancelableFuture[FiniteDistribution[Term]] = Success(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
        2.5311163260347958E-5
      )
    )
  )
)

val pfT = pfsT.map(_.supp.head)
pfT.runToFuture

pfT: monix.eval.Task[Term] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$312/951031848@3bc356a5,
  2
)
res7_1: monix.execution.CancelableFuture[Term] = Success(
  axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l))
)

val lpTangT1  = pfT.flatMap(pf => lp1.distTangentProver(FiniteDistribution.unif(pf)))

lpTangT1: monix.eval.Task[LocalTangentProver] = FlatMap(
  Map(
    Async(<function2>, false, true, true),
    scala.Function1$$Lambda$312/951031848@3bc356a5,
    2
  ),
  ammonite.$sess.cmd8$Helper$$Lambda$3047/1835419271@7352ce49
)

val goal = eqM(l)(r)

goal: Typ[Term] = eqM(e_l)(e_r)

val targGoalT1 = lpTangT1.flatMap(lpt => lpt.theoremsByStatement).map(_(goal))

targGoalT1: monix.eval.Task[Double] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        scala.Function1$$Lambda$312/951031848@3bc356a5,
        2
      ),
      ammonite.$sess.cmd8$Helper$$Lambda$3047/1835419271@7352ce49
    ),
    ammonite.$sess.cmd10$Helper$$Lambda$3054/1604136391@549e05e5
  ),
  ammonite.$sess.cmd10$Helper$$Lambda$3055/786027227@6a255aa9,
  0
)

targGoalT1.runToFuture

res11: monix.execution.CancelableFuture[Double] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(0.03607619269409383)

Interim Conclusion¶

We replicated the tangent result using an actual proof, so nothing formal

val eqsT = for{
    eq1 <- lp1.equations
    lp2 <- lpTangT1
    eq2 <- lp2.equations
} yield Equation.merge(eq1, eq2)

eqsT: monix.eval.Task[Set[Equation]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd12$Helper$$Lambda$3166/539388556@3a3fa598
)

eqsT.runToFuture

res13: monix.execution.CancelableFuture[Set[Equation]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Set(
    Equation(
      FinalVal(
        Elem(
          ($feduk : eqM(mul(e_r)(e_l))($fedtg)) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_l))(e_l)(mul(e_l)(e_r))($feduk)(axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l))),
          Terms
        )
      ),
      Product(
        Product(
          Coeff(
            BaseThenCondition(
              ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
              Funcs,
              Restrict(FuncOpt)
            )
          ),
          FinalVal(
            Elem(
              Wrap(
                axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_l))
              ),
              Funcs
            )
          )
        ),
        FinalVal(
          Elem(
            axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
            Terms
          )
        )
      )
    ),
    Equation(
...

val evT = eqsT.map(eqs => ExpressionEval.fromInitEqs(ts, eqs, tg1)).memoize

evT: monix.eval.Task[ExpressionEval] = Async(<function2>, false, true, true)

val terms2T = evT.map(_.finalTerms).memoize

terms2T: monix.eval.Task[FiniteDistribution[Term]] = Async(
  <function2>,
  false,
  true,
  true
)

val eqPfsT = terms2T.map(ts => ts.filter(_.typ == goal))

eqPfsT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd18$Helper$$Lambda$3220/927326813@6904ba30,
  0
)

eqPfsT.runToFuture

res19: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  FiniteDistribution(
    Vector(
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_l)(mul(e_l)(e_r))(e_r)(axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)))(axiom_{eqM(mul(e_l)(a))(a)}(e_r)),
        6.526548906054404E-6
      )
    )
  )
)

Conclusion¶

This was fully successful, with the grouped equations giving a proof from the initial state.
Further, the proof weight is very low, so it should be identified as very non-trivial.
Thus, this part of the accumulation of equations approach works (the other part of using formal equations for goals was previously tested).