In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.1-SNAPSHOT`
Out[1]:
In [2]:
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
Out[2]:
In [3]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [4]:
val tg = TermGenParams(lmW=0, piW=0)
Out[4]:
In [5]:
val ts = TermState(dist1, dist1.map(_.typ))
Out[5]:
In [6]:
val mfd = tg.monixFD
Out[6]:
In [7]:
val tgT = mfd.nodeDist(ts)(tg.Gen.codomainNode(eqM(l)(r)), 0.0001)
Out[7]:
The above is looking at backward reasoning for $e_l = e_r$. We see that
In [8]:
import monix.execution.Scheduler.Implicits.global
val tgD = tgT.runSyncUnsafe()
Out[8]:
In [9]:
val tgT1 = mfd.nodeDist(ts)(tg.Gen.codomainNode(eqM(op(l)(r))(r)), 0.0001)
Out[9]:
We are next targeting $e_l * e_r = e_r$. Here the main thing we see is we get a proof with weight $0.3$ straightaway. We also get symmetry and transitivity as before.
In [10]:
val tgD1 = tgT1.runSyncUnsafe()
Out[10]:
In [11]:
ts.terms
Out[11]:
In [12]:
tgD1.filter(_.typ == eqM(op(l)(r))(r))
Out[12]:
In [13]:
val tgT2 = mfd.nodeDist(ts)(tg.Gen.codomainNode(eqM(r)(op(l)(r))), 0.0001)
Out[13]:
This is essentially the same as above. Just verifies that we get symmetry. If this is chained with the previous example, we get a proof directly.
In [14]:
val tgD2 = tgT2.runSyncUnsafe()
Out[14]:
In [15]:
val tgtT2 = mfd.nodeDist(ts)(tg.Gen.foldedTargetFunctionNode(eqM(r)(op(l)(r))), 0.0001)
Out[15]:
And indeed, here is a proof of the lemma.
In [16]:
val tgtD2 = tgtT2.runSyncUnsafe()
Out[16]:
In [17]:
import IdentityTyp._
symmTerm
Out[17]:
In [18]:
transTerm
Out[18]:
In [19]:
symmTerm (M) (l) (r)
Out[19]:
In [20]:
symmTerm(M)(l)(r).typ
Out[20]:
In [21]:
transTerm(M).typ
Out[21]:
In [22]:
val ts0 = TermState(FiniteDistribution.unif(symmTerm, transTerm, l, r), FiniteDistribution.unif(M))
Out[22]:
In [23]:
val tgT0 = mfd.nodeDist(ts0)(tg.Gen.codomainNode(l =:= r), 0.001)
Out[23]:
In [24]:
Unify.targetCodomain(symmTerm, l =:= r)
Out[24]: