We attempt to replicate the Monoid proof but with our new workflow and with the local provers.
In [1]:
import $cp.bin.`provingground-core-jvm-3d48753.fat.jar`
Out[1]:
In [2]:
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[2]:
In [3]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
Out[3]:
In [4]:
val tg = TermGenParams(lmW=0, piW=0)
val ts = TermState(dist1, dist1.map(_.typ))
Out[4]:
In [5]:
import monix.execution.Scheduler.Implicits.global
Out[5]:
In [6]:
val lp = LocalProver(ts).noIsles.sharpen(10)
Out[6]:
In [7]:
val lemT = lp.lemmas
Out[7]:
In [8]:
val lemF = lemT.runToFuture
In [9]:
val tangLpT = lp.proofTangent()
Out[9]:
In [10]:
val thmsT = tangLpT.flatMap(_.theoremsByStatement)
Out[10]:
In [11]:
val thmsF = thmsT.runToFuture
In [12]:
thmsF.value
Out[12]:
In [13]:
val tangLpT0 = tangLpT.map(_.copy(cutoff = math.pow(10, -3)))
Out[13]:
In [14]:
val thmsT0 = tangLpT0.flatMap(_.theoremsByStatement)
Out[14]:
In [15]:
val thmsF0 = thmsT0.runToFuture
In [16]:
thmsF0.map(_(eqM(l)(r)))
In [17]:
val tangLpT1 = tangLpT.map(_.copy(cutoff = 5* math.pow(10, -3)))
val thmsT1 = tangLpT1.flatMap(_.theoremsByStatement)
val goal = eqM(l)(r)
val goalT = thmsT1.map(_(goal))
Out[17]:
In [18]:
val goalF = goalT.runToFuture
In [19]:
val tangLpT2 = tangLpT.map(_.copy(cutoff = math.pow(10, -4)))
val thmsT2 = tangLpT2.flatMap(_.theoremsByStatement)
val goalT2 = thmsT2.map(_(goal))
Out[19]:
In [20]:
val goalF2 = goalT2.runToFuture
In [21]:
val lem = eqM(l)(op(l)(r))
Out[21]:
In [22]:
val cmlT = lemT.map(_.filter(_._1 == lem)).runToFuture
In [23]:
val tangS = ts.tangent("proof" :: lem)
Out[23]:
In [24]:
val lpTangT = lp.distTangentProver(FiniteDistribution.unif("proof" :: lem))
Out[24]:
In [25]:
val targGoalT = lpTangT.flatMap(lpt => lpt.theoremsByStatement).map(_(goal))
Out[25]:
In [26]:
val targGoalF = targGoalT.runToFuture