Instantiation and proving with Bots

We take a $\Sigma$-type as a goal, and see that this is obtained by backward reasoning involving choosing instantiations and propagating proofs.

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)

Conclusion

Two proofs were obtained, based on two proofs of $\mathbb{0} \to \mathbb{0}$.