Proof propagation¶

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

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

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))
val lp1 = LocalProver(ts, tg1)

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

import monix.execution.Scheduler.Implicits.global 
val lemT1 = lp1.lemmas.memoize
lemT1.runToFuture

import monix.execution.Scheduler.Implicits.global 

lemT1: monix.eval.Task[Vector[(Typ[Term], Double)]] = Async(
  <function2>,
  false,
  true,
  true
)
res3_2: 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 pfsT = lp1.lemmaProofs
pfsT.runToFuture

pfsT: monix.eval.Task[FiniteDistribution[Term]] = FlatMap(
  Async(<function2>, false, true, true),
  provingground.learning.LocalProverStep$$Lambda$2953/810352088@4a685dd8
)
res4_1: monix.execution.CancelableFuture[FiniteDistribution[Term]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  FiniteDistribution(
    Vector(
      Weighted(axiom_{eqM(a)(a)}(e_r), 0.0025589063334613047),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)(e_r)(axiom_{eqM(a)(a)}(e_r)),
        1.920121138215279E-4
      ),
      Weighted(axiom_{eqM(a)(a)}(e_l), 0.0025589063334613047),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_l)(e_l)(axiom_{eqM(a)(a)}(e_l)),
        1.920121138215279E-4
      ),
      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)),
        0.0012526844961492322
      ),
      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)),
        0.0012526844961492322
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_r)(axiom_{eqM(mul(e_l)(a))(a)}(e_r)),
        0.0012526844961492322
      ),
      Weighted(
        axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_r)(e_r))(e_r)(axiom_{eqM(mul(a)(e_r))(a)}(e_r)),
        0.0012526844961492322
      )
    )
  )
)

val pfTermsT = lp1.proofTerms
pfTermsT.runToFuture

pfTermsT: monix.eval.Task[Vector[(Term, Double)]] = FlatMap(
  Map(
    FlatMap(
      Async(<function2>, false, true, true),
      provingground.learning.LocalProverStep$$Lambda$2953/810352088@4a685dd8
    ),
    provingground.learning.LocalProverStep$$Lambda$2975/1488281714@19136358,
    0
  ),
  provingground.learning.LocalProverStep$$Lambda$2976/661199252@209663db
)
res6_1: monix.execution.CancelableFuture[Vector[(Term, Double)]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Vector(
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_l))(e_l)(axiom_{eqM(mul(e_l)(a))(a)}(e_l)),
      0.0012526844961492322
    ),
    (axiom_{eqM(a)(a)}(e_r), 0.0025589063334613047),
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_r)(axiom_{eqM(mul(e_l)(a))(a)}(e_r)),
      0.0012526844961492322
    ),
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_r)(e_r)(axiom_{eqM(a)(a)}(e_r)),
      1.920121138215279E-4
    ),
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_l)(e_r))(e_l)(axiom_{eqM(mul(a)(e_r))(a)}(e_l)),
      0.0012526844961492322
    ),
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(e_l)(e_l)(axiom_{eqM(a)(a)}(e_l)),
      1.920121138215279E-4
    ),
    (axiom_{eqM(a)(a)}(e_l), 0.0025589063334613047),
    (
      axiom_{(eqM(a)(b) \to eqM(b)(a))}(mul(e_r)(e_r))(e_r)(axiom_{eqM(mul(a)(e_r))(a)}(e_r)),
      0.0012526844961492322
    )
  )
)

First conclusions¶

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

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.cmd7$Helper$$Lambda$3064/1171313393@13fe3d75,
  0
)
res7_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(
        ($aufv : M) ↦ axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(mul(e_r)(e_r))(e_r)($aufv)(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(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))}(e_r)(mul(e_r)(e_r)),
        1.4320425904260095E-5
      ),
      Weighted(eqM(e_r)(e_l), 0.00997538738813242),
...

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

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

pfsT: monix.eval.Task[FiniteDistribution[Term]] = Map(
  Async(<function2>, false, true, true),
  scala.Function1$$Lambda$276/1122130699@7268ee77,
  1
)
res9_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
      )
    )
  )
)
import Expression._, TermRandomVars._, GeneratorVariables._


res9_3: monix.eval.Task[Map[Expression, Double]] = FlatMap(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd9$Helper$$Lambda$3145/1974190932@2e4d5bd8
)

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

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

backT.runToFuture

res12: monix.execution.CancelableFuture[Map[Expression, Double]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Map(
    FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms)) -> 0.01263157894736842,
    FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)) -> 5.990977443609026E-4
  )
)

lp1.cutoff

res13: Double = 1.0E-4

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

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

rhsT.runToFuture

res15: monix.execution.CancelableFuture[Expression] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Sum(
    Sum(
      Product(
        Product(
          Coeff(
            BaseThenCondition(
              ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms),
              AtCoord(TermsWithTyp, M :: HNil),
              Filter(WithTyp(M))
            )
          ),
          FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
        ),
        FinalVal(Elem(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)(a))}), Funcs))
        ),
        FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms))
      )
    ),
    Product(
      Product(
        Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms)),
        FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs))
      ),
      FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms))
    )
  )
)

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

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

fullBackT.runToFuture

res17: monix.execution.CancelableFuture[Map[Expression, Double]] = @keyframes fadein { from { opacity: 0; } to { opacity: 1; } }Success(
  Map(
    FinalVal(Elem(axiom_{eqM(mul(a)(e_r))(a)}(e_l), Terms)) -> 0.01263157894736842,
    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
      )
    ) -> 1.0,
    FinalVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)) -> 5.990977443609024E-4,
    InitialVal(Elem(Wrap(axiom_{eqM(mul(a)(e_r))(a)}), Funcs)) -> 4.79278195488722E-4,
    InitialVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)) -> 4.792781954887222E-4,
    FinalVal(Elem(Wrap(axiom_{(eqM(a)(b) \to eqM(b)(a))}), Funcs)) -> 5.990977443609026E-4,
    FinalVal(Elem(e_l, AtCoord(TermsWithTyp, M :: HNil))) -> 1.5955678670360112E-4,
    FinalVal(Elem(e_l, Terms)) -> 1.5955678670360112E-4,
    InitialVal(Elem(e_l, Terms)) -> 1.276454293628809E-4
  )
)

Conclusions¶

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