In [1]:
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
}
)
}
Out[1]:
In [2]:
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
Out[2]:
In [3]:
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
Out[3]:
In [4]:
val typs0T = lp0.nextState.map(_.typs).memoize
Out[4]:
In [5]:
import monix.execution.Scheduler.Implicits.global
val typs0F = typs0T.runToFuture
In [6]:
val lp1 = LocalProver(ts0, tg = tg0, genMaxDepth = Some(1)).noIsles
val typs1T = lp1.nextState.map(_.typs).memoize
Out[6]:
In [7]:
val typs1F = typs1T.runToFuture
In [8]:
val lp2 = LocalProver(ts0, tg = tg0, genMaxDepth = Some(2)).noIsles
val typs2T = lp2.nextState.map(_.typs).memoize
Out[8]:
In [9]:
val typs2F = typs2T.runToFuture
In [13]:
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)
Out[13]:
In [14]:
val typs3T = lp3.nextState.map(_.typs).memoize
Out[14]:
In [15]:
val typs3F = typs3T.runToFuture
In [16]:
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
Out[16]:
In [17]:
val c3T = typs3T.map(typs => claims.map(c => c -> typs(c)))
Out[17]:
In [18]:
val c3F = c3T.runToFuture
In [19]:
c3F.value
Out[19]:
In [20]:
val lp4 = LocalProver(ts0, tg = tg1, genMaxDepth = Some(4)).noIsles.sharpen(10)
val typs4T = lp4.nextState.map(_.typs).memoize
Out[20]:
In [21]:
val typs4F = typs4T.runToFuture
In [24]:
typs4F.value
Out[24]:
In [25]:
val c4T = typs4T.map(typs => claims.map(c => c -> typs(c))).memoize
Out[25]:
In [26]:
val c4F = c4T.runToFuture
In [27]:
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
Out[27]:
In [28]:
val typs5F = typs5T.runToFuture
In [31]:
typs5F.value
Out[31]:
In [33]:
val c5T = typs5T.map(typs => claims.map(c => c -> typs(c))).memoize
Out[33]:
In [34]:
val c5F = c5T.runToFuture
In [35]:
val flipped = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))
Out[35]:
In [36]:
val pF = typs4T.map(_(flipped)).runToFuture
In [37]:
val flipped2 = eqM(mul(n)(m))(mul(mul(mul(m)(n))(m))(m))
Out[37]:
In [38]:
val pF2 = typs4T.map(_(flipped2)).runToFuture
In [39]:
val eqFlip = a :-> (b :-> eqM(b)(a))
Out[39]:
In [40]:
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))
Out[40]:
In [41]:
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
Out[41]:
In [42]:
val typs6F = typs6T.runToFuture
In [46]:
typs6F.value
Out[46]:
In [47]:
val c6T = typs6T.map(typs => claims.map(c => c -> typs(c))).memoize
Out[47]:
In [48]:
val c6F = c6T.runToFuture