Proof propagation

We have used the proofs of lemmas, but not the terms in the proofs. We test these in the monoid case.


In [1]:
import $cp.bin.`provingground-core-jvm-2932e539da.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))
val lp1 = LocalProver(ts, tg1)


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)
...
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 [4]:
import monix.execution.Scheduler.Implicits.global 
val lemT1 = lp1.lemmas.memoize
lemT1.runToFuture



In [5]:
val pfsT = lp1.lemmaProofs
pfsT.runToFuture



In [7]:
val pfTermsT = lp1.proofTerms
pfTermsT.runToFuture


First conclusions

There seems to be no propagation at all of proofs. We should check individual back maps.


In [8]:
val lem = eqM(l)(op(l)(r))
val termsT = lp1.expressionEval.map(_.finalTerms)
termsT.runToFuture



In [10]:
val pfsT = termsT.map(_.filter(_.typ == lem))
pfsT.runToFuture

import Expression._, TermRandomVars._, GeneratorVariables._



In [12]:
val backT = for {
    ev <- lp1.expressionEval
    pfs <- pfsT
} yield ev.Final.backMap(FinalVal(Elem( pfs.support.head, Terms )))


Out[12]:
backT: monix.eval.Task[Map[Expression, Double]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd11$Helper$$Lambda$3165/1621996626@ac0c879
)

In [13]:
backT.runToFuture



In [14]:
lp1.cutoff


Out[14]:
res13: Double = 1.0E-4

In [15]:
val rhsT = for {
    ev <- lp1.expressionEval
    pfs <- pfsT
} yield ev.rhs(FinalVal(Elem( pfs.support.head, Terms )))


Out[15]:
rhsT: monix.eval.Task[Expression] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd14$Helper$$Lambda$3189/1250269153@75b509ff
)

In [16]:
rhsT.runToFuture



In [17]:
val fullBackT = for {
    ev <- lp1.expressionEval
    pfs <- pfsT
} yield ev.Final.fullBackMap(Map(FinalVal(Elem( pfs.support.head, Terms )) -> 1), lp1.cutoff)


Out[17]:
fullBackT: monix.eval.Task[Map[Expression, Double]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd16$Helper$$Lambda$3201/2056589288@4ea89daf
)

In [18]:
fullBackT.runToFuture


Conclusions

  • this is working fine.
  • the cutoff leads to all backward propagated terms disappearing.
  • we may need to propagate more strongly, or reduce cutoffs