We test a new feature -- a bound on depth in addition to cutoff.
import $cp.bin.`provingground-core-jvm-3ed16ecda4.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
val M = "M" :: Type
val eqM = "eqM" :: M ->: M ->: Type
val a = "a" :: M
val b = "b" :: M
val c = "c" :: M
val m = "m" :: M
val n = "n" :: M
val mul = "mul" :: M ->: M ->: M
val ts0 = TermState(FiniteDistribution(eqM -> 0.2, mul -> 0.35, m -> 0.15, n -> 0.15, mul(m)(n) -> 0.15), FiniteDistribution.unif(M))
val tg0 = TermGenParams.zero.copy(appW = 0.15, typAsCodW = 0.1)
val lp0 = LocalProver(ts0, tg = tg0, genMaxDepth = Some(3)).noIsles
val typs0T = lp0.nextState.map(_.typs).memoize
import monix.execution.Scheduler.Implicits.global
val typs0F = typs0T.runToFuture
val lp1 = LocalProver(ts0, tg = tg0, genMaxDepth = Some(1)).noIsles
val typs1T = lp1.nextState.map(_.typs).memoize
val typs1F = typs1T.runToFuture
val lp2 = LocalProver(ts0, tg = tg0, genMaxDepth = Some(2)).noIsles
val typs2T = lp2.nextState.map(_.typs).memoize
val typs2F = typs2T.runToFuture
val tg1 = TermGenParams.zero.copy(appW = 0.2, typAsCodW = 0.1, argAppW = 0.2)
val lp3 = LocalProver(ts0, tg = tg1, genMaxDepth = Some(3)).noIsles.sharpen(10)
val typs3T = lp3.nextState.map(_.typs).memoize
val typs3F = typs3T.runToFuture
With a bound on depth, this finishes in a couple of seconds even if sharpened.
val Thm = eqM(mul(m)(n))(mul(n)(m))
val Lemmas =
Map(
1 -> eqM(m)(mul(mul(m)(n))(n)),
2 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
3 -> eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
4 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)),
5 -> eqM(mul(mul(m)(n))(m))(n),
6 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)),
7 -> eqM(mul(mul(m)(n))(n))(m),
8 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n)))
)
val claims = Lemmas.values.toSet + Thm
val c3T = typs3T.map(typs => claims.map(c => c -> typs(c)))
val c3F = c3T.runToFuture
c3F.value
val lp4 = LocalProver(ts0, tg = tg1, genMaxDepth = Some(4)).noIsles.sharpen(10)
val typs4T = lp4.nextState.map(_.typs).memoize
val typs4F = typs4T.runToFuture
typs4F.value
val c4T = typs4T.map(typs => claims.map(c => c -> typs(c))).memoize
val c4F = c4T.runToFuture
val tg2 = TermGenParams.zero.copy(appW = 0.2, typAsCodW = 0.1)
val lp5 = LocalProver(ts0, tg = tg2, genMaxDepth = Some(5)).noIsles.sharpen(10)
val typs5T = lp5.nextState.map(_.typs).memoize
val typs5F = typs5T.runToFuture
typs5F.value
val c5T = typs5T.map(typs => claims.map(c => c -> typs(c))).memoize
val c5F = c5T.runToFuture
val flipped = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))
val pF = typs4T.map(_(flipped)).runToFuture
val flipped2 = eqM(mul(n)(m))(mul(mul(mul(m)(n))(m))(m))
val pF2 = typs4T.map(_(flipped2)).runToFuture
val eqFlip = a :-> (b :-> eqM(b)(a))
val ts1 = TermState(FiniteDistribution(eqM -> 0.1, eqFlip -> 0.1, mul -> 0.35, m -> 0.15, n -> 0.15, mul(m)(n) -> 0.15), FiniteDistribution.unif(M))
val tg2 = TermGenParams.zero.copy(appW = 0.2, typAsCodW = 0.1)
val lp6 = LocalProver(ts1, tg = tg2, genMaxDepth = Some(4)).noIsles.sharpen(10)
val typs6T = lp6.nextState.map(_.typs).memoize
val typs6F = typs6T.runToFuture
typs6F.value
val c6T = typs6T.map(typs => claims.map(c => c -> typs(c))).memoize
val c6F = c6T.runToFuture