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.



In [1]:

    
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
    }
  )
}









    Out[1]:





import $cp.$                                              

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



In [2]:

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









    Out[2]:





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)
...



In [3]:

    
import monix.execution.Scheduler.Implicits.global









    Out[3]:





import monix.execution.Scheduler.Implicits.global



In [4]:

    
val lp1 = LocalProver(ts, tg1)









    Out[4]:





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),
...



In [5]:

    
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)]] = 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)
  )
)



In [6]:

    
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]] = 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
      ),
...



In [7]:

    
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
      )
    )
  )
)



In [8]:

    
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))
)



In [9]:

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









    Out[9]:





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
)



In [10]:

    
val goal = eqM(l)(r)









    Out[10]:





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



In [11]:

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









    Out[11]:





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
)



In [12]:

    
targGoalT1.runToFuture









    





res11: monix.execution.CancelableFuture[Double] = Success(0.03607619269409383)

Interim Conclusion

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



In [13]:

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









    Out[13]:





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



In [14]:

    
eqsT.runToFuture









    





res13: monix.execution.CancelableFuture[Set[Equation]] = 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(
...



In [15]:

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









    Out[15]:





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



In [18]:

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









    Out[18]:





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



In [19]:

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









    Out[19]:





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



In [20]:

    
eqPfsT.runToFuture









    





res19: monix.execution.CancelableFuture[FiniteDistribution[Term]] = 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).