InΒ [1]:
import $cp.bin.`provingground-core-jvm-27df14e69b.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[1]:
import $cp.$
import provingground._ , interface._, HoTT._, learning._
We set things up. Note that we avoid $\Sigma$-islands so the result is not proved directly.
InΒ [2]:
import provingground.{FiniteDistribution => FD}
val ts = TermState(FD.unif(One, Zero, Star, Type), FD.unif(One, Zero, Type))
val tg = TermGenParams(sigmaW = 0)
val lp = LocalProver(ts, tg)
Out[2]:
import provingground.{FiniteDistribution => FD}
ts: TermState = TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
)
tg: TermGenParams = TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
0.05,
0.0,
0.0,
0.0,
0.0,
0.0,
0.3,
0.7,
0.5,
0.0,
0.0,
0.0,
OrElse(
OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
<function1>
)
)
lp: LocalProver = LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
0.05,
0.0,
0.0,
0.0,
0.0,
0.0,
0.3,
0.7,
0.5,
...
InΒ [3]:
import HoTTMessages._
import HoTTBot._
val web = new HoTTPostWeb()
val ws = WebState[HoTTPostWeb, HoTTPostWeb.ID](web)
val ws1 = ws.post(lp, Set())
val A = Type.sym
val notAll = sigma(A)(A ->: Zero)
import monix.execution.Scheduler.Implicits.global
val ws2 = ws1.flatMap(w => w.postApex(SeekGoal(notAll, Context.Empty)))
val ws3 = ws2.flatMap(w => w.act(sigmaBackward))
val ws4 = ws3.flatMap(w => w.act(instanceFromLp))
val ws5 = ws4.flatMap(w => w.act(instanceToGoal))
val ws6 = ws5.flatMap(w => w.act(goalToProver(0.3, 0.7)))
val ws7 = ws6.flatMap(w => w.act(lpToFinalState))
val ws8 = ws7.flatMap(w => w.act(postProofs))
val ws9 = ws8.flatMap(w => w.act(deducedEquations ))
val pfs = ws9.flatMap(_.queryApex[Proved]())
2020.05.27 11:39:12 [INFO] provingground.learning.PostBuffer.$anon.post:244:22 - Post; tag: TypeTag[provingground.learning.LocalProver], id: (1,314072443), content:
LocalProver(TermState([Unit : 0.25, Zero : 0.25, Star : 0.25, π° _0 : 0.25],[Unit : 0.3333333333333333, Zero : 0.3333333333333333, π° _0 : 0.3333333333333333],Vector(),[],[],Empty),TermGenParams(0.1,0.1,0.1,0.1,0.1,0.0,0.05,0.05,0.0,0.0,0.0,0.0,0.0,0.3,0.7,0.5,0.0,0.0,0.0,<function1>),1.0E-4,None,12 minutes,1.01,1.0,10000,10,1.0,1.0,None,false,false,0.5,1.0)
import HoTTMessages._
import HoTTBot._
web: HoTTPostWeb = provingground.learning.HoTTPostWeb@52a7ce13
ws: WebState[HoTTPostWeb, (Int, Int)] = WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector()
)
ws1: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
0.05,
0.0,
0.0,
0.0,
...
A: Typ[Term] = A
notAll: Typ[AbsPair[Typ[Term], Func[Term, Term]]] = β(A : π° ){ (A β Zero) }
import monix.execution.Scheduler.Implicits.global
ws2: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
SeekGoal(β(A : π° ){ (A β Zero) }, Empty, Set()),
(2, -1120268393)
),
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
...
ws3: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
provingground.learning.HoTTMessages$SeekInstances$$anon$1@4568d1d3,
(3, 1164497363)
),
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
...
ws4: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(Instance(Zero, π° , Empty), (6, -589143408)),
PostData(Instance(Unit, π° , Empty), (7, -1890567806)),
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
0.05,
0.0,
...
ws5: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
SeekGoal((Zero β Zero), Empty, Set(β(A : π° ){ (A β Zero) })),
(10, 762905811)
),
PostData(
SeekGoal((Unit β Zero), Empty, Set(β(A : π° ){ (A β Zero) })),
(9, 762905811)
),
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector()),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
...
ws6: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
LocalProver(
TermState(
FiniteDistribution(
Vector(
Weighted(Unit, 0.25),
Weighted(Zero, 0.25),
Weighted(Star, 0.25),
Weighted(π° , 0.25)
)
),
FiniteDistribution(
Vector(
Weighted(Unit, 0.3333333333333333),
Weighted(Zero, 0.3333333333333333),
Weighted(π° , 0.3333333333333333)
)
),
Vector(),
FiniteDistribution(Vector()),
FiniteDistribution(Vector(Weighted((Zero β Zero), 1.0))),
Empty
),
TermGenParams(
0.1,
0.1,
0.1,
0.1,
0.1,
0.0,
0.05,
0.05,
0.0,
0.0,
0.0,
...
ws7: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
FinalState(
TermState(
FiniteDistribution(
Vector(
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @b, 4.8363310633542324E-4),
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @a, 3.3854317443479627E-4),
Weighted((@a : (Unit β Zero)) β¦ Star, 2.8255334173981077E-4),
Weighted((@a : (Zero β Zero)) β¦ Star, 2.8255334173981077E-4),
Weighted((@a : Unit) β¦ Star, 0.004654968648478449),
Weighted((@a : β(@a : π° ){ @a }) β¦ π° , 2.542980075658297E-4),
Weighted(π° , 0.19927965691954855),
Weighted((@a : Unit) β¦ (@a : π° ) β¦ @a, 3.3854317443479627E-4),
Weighted((@a : π° ) β¦ (@a : Unit) β¦ @a, 3.4982794691595616E-4),
Weighted((@a : (Unit β Zero)) β¦ @a, 4.84377157268247E-4),
Weighted((@a : (Zero β Zero)) β¦ @a, 4.84377157268247E-4),
Weighted((@a : (π° β Zero)) β¦ @a, 3.3906401008777293E-4),
Weighted((@a : Unit) β¦ (@a : Zero) β¦ @a, 4.8363310633542324E-4),
Weighted((@a : Zero) β¦ (@a : Unit) β¦ @a, 3.385431744347963E-4),
Weighted((@a : (Zero β Unit)) β¦ Unit, 2.8255334173981077E-4),
Weighted((@a : (Unit β Unit)) β¦ Unit, 2.8255334173981077E-4),
Weighted((@a : (Unit β Zero)) β¦ π° , 2.8255334173981077E-4),
Weighted((@a : (Zero β Zero)) β¦ π° , 2.8255334173981077E-4),
Weighted((@a : β(@a : π° ){ @a }) β¦ Star, 2.542980075658297E-4),
Weighted((@a : (Unit β Zero)) β¦ Zero, 2.8255334173981077E-4),
Weighted((@a : (Zero β Zero)) β¦ Zero, 2.8255334173981077E-4),
Weighted((@a : Zero) β¦ Unit, 0.0046549686484784495),
Weighted(
(@a : Unit) β¦ rec_{ Zero ; Zero },
0.002418165531677116
),
Weighted((@a : (Zero β π° )) β¦ π° , 2.8255334173981077E-4),
Weighted((@a : (Unit β π° )) β¦ π° , 2.8255334173981077E-4),
Weighted(rec_{ Zero ; Zero }, 0.019072350567437227),
Weighted(Zero, 0.21653559314722987),
...
ws8: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
Proved((Zero β Zero), Some(rec_{ Zero ; Zero }), Empty),
(14, 1730932590)
),
PostData(
Proved((Zero β Zero), Some((@a : Zero) β¦ @a), Empty),
(15, 183366453)
),
PostData(
FinalState(
TermState(
FiniteDistribution(
Vector(
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @a, 3.3734161337695227E-4),
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @b, 4.819165905385032E-4),
Weighted((@a : Unit) β¦ (@a : π° ) β¦ π° , 1.9678260780322211E-4),
Weighted((@a : Zero) β¦ (@a : π° ) β¦ π° , 1.967826078032221E-4),
Weighted((@a : (π° β Zero)) β¦ Star, 1.7602114000746932E-4),
Weighted((@a : (Zero β Zero)) β¦ Star, 2.514587714392419E-4),
Weighted((@a : (Unit β Zero)) β¦ Star, 2.514587714392419E-4),
Weighted((@a : Unit) β¦ Star, 0.004638447183933092),
Weighted((@a : β(@a : π° ){ @a }) β¦ π° , 2.263128942953177E-4),
Weighted(π° , 0.20067095432796372),
Weighted((@a : Unit) β¦ (@a : π° ) β¦ @a, 3.3734161337695227E-4),
Weighted((@a : π° ) β¦ (@a : Unit) β¦ @a, 3.5613456016732E-4),
Weighted((@a : Zero) β¦ (@a : π° ) β¦ Star, 1.967826078032221E-4),
Weighted((@a : (π° β Zero)) β¦ @a, 3.017505257270902E-4),
Weighted((@a : (Zero β Zero)) β¦ @a, 4.310721796101289E-4),
Weighted((@a : (Unit β Zero)) β¦ @a, 4.310721796101289E-4),
Weighted(rec_{ Zero ; Unit }, 7.918955595800889E-4),
Weighted((@a : Unit) β¦ (@a : Zero) β¦ @a, 4.819165905385032E-4),
Weighted((@a : Zero) β¦ (@a : Unit) β¦ @a, 3.3734161337695227E-4),
Weighted((@a : (Unit β Unit)) β¦ Unit, 2.514587714392419E-4),
Weighted((@a : (Zero β Unit)) β¦ Unit, 2.514587714392419E-4),
Weighted((@a : (π° β Unit)) β¦ Unit, 1.7602114000746932E-4),
...
ws9: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
WebState(
provingground.learning.HoTTPostWeb@52a7ce13,
Vector(
PostData(
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , (@a : Zero) β¦ @a)), Empty),
(17, 1778348471)
),
PostData(
Proved(
β(A : π° ){ (A β Zero) },
Some((Zero , rec_{ Zero ; Zero })),
Empty
),
(19, 1786040065)
),
PostData(
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , (@a : Zero) β¦ @a)), Empty),
(17, 1778348471)
),
PostData(
Proved(
β(A : π° ){ (A β Zero) },
Some((Zero , rec_{ Zero ; Zero })),
Empty
),
(18, 1786040065)
),
PostData(
FinalState(
TermState(
FiniteDistribution(
Vector(
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @a, 3.3734161337695227E-4),
Weighted((@a : Unit) β¦ (@b : Unit) β¦ @b, 4.819165905385032E-4),
Weighted((@a : Unit) β¦ (@a : π° ) β¦ π° , 1.9678260780322211E-4),
Weighted((@a : Zero) β¦ (@a : π° ) β¦ π° , 1.967826078032221E-4),
...
pfs: concurrent.Future[Vector[Proved]] = Success(
Vector(
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , (@a : Zero) β¦ @a)), Empty),
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , rec_{ Zero ; Zero })), Empty),
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , (@a : Zero) β¦ @a)), Empty),
Proved(β(A : π° ){ (A β Zero) }, Some((Zero , rec_{ Zero ; Zero })), Empty)
)
)
Content source: siddhartha-gadgil/ProvingGround
Similar notebooks: