Bot based Modus Ponens

We continue to explore the use of Bots. Here we prove Modus Ponens but without islands. Instead we use backward reasoning to introduce variables. This time we build a session and launch, generalizing both manual and automatic cases.

import $cp.bin.`provingground-core-jvm-ac7ee25c26.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}

import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 

Utils.logger = {
    import scribe._, writer._, Utils._
    logger.withHandler(writer = FileWriter().path(file.LogPath.simple("modus-ponens.log"))).replace()
}

First we set things up.

import provingground._ , learning._, interface._, translation._, HoTT._
import monix.execution.Scheduler.Implicits.global
val A = Type.sym
val B = Type.sym
val MP = A ~>: (B ~>: (A ->: (A ->: B) ->: B))
val ts = TermState(FiniteDistribution.unif(Type), FiniteDistribution.unif(Type))
val tg = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)
val lp = LocalProver(ts, tg)
import HoTTMessages._

import provingground._ , learning._, interface._, translation._, HoTT._

import monix.execution.Scheduler.Implicits.global

A: Typ[Term] = A
B: Typ[Term] = B
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
tg: TermGenParams = TermGenParams(
  0.1,
  0.1,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  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(𝒰 , 1.0))),
    FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.1,
    0.1,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    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>
    )
  ),
  1.0E-4,
  None,
  12 minutes,
  1.01,
...
import HoTTMessages._

Next we post stuff. Note that this is still manual bot mode, but a session will only have a couple of useless triggers.

val web = new HoTTPostWeb()
val ws = WebState[HoTTPostWeb, HoTTPostWeb.ID](web)
val ws1 = ws.post(lp, Set())
val ws2 = ws1.flatMap(w => w.postApex(SeekGoal(MP, Context.Empty)))

web: HoTTPostWeb = provingground.learning.HoTTPostWeb@189fa825
ws: WebState[HoTTPostWeb, (Int, Int)] = WebState(
  provingground.learning.HoTTPostWeb@189fa825,
  Vector()
)
ws1: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@189fa825,
    Vector(
      PostData(
        LocalProver(
          TermState(
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector(),
            FiniteDistribution(Vector()),
            FiniteDistribution(Vector()),
            Empty
          ),
          TermGenParams(
            0.1,
            0.1,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            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>
              ),
...
ws2: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@189fa825,
    Vector(
      PostData(
        SeekGoal(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, Empty, Set()),
        (2, 260968439)
      ),
      PostData(
        LocalProver(
          TermState(
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector(),
            FiniteDistribution(Vector()),
            FiniteDistribution(Vector()),
            Empty
          ),
          TermGenParams(
            0.1,
            0.1,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.3,
            0.7,
            0.5,
            0.0,
            0.0,
            0.0,
            OrElse(
...

import HoTTBot._
val sessF = ws2.map(w => HoTTWebSession.launch(w, Vector(fullGoalInContext , goalToProver(0.3, 0.7), lpToFinalState, reportSuccesses)))

import HoTTBot._

sessF: concurrent.Future[HoTTWebSession] = Success(provingground.learning.HoTTWebSession@768faa7a)

Utils.reportText

res5: String = Success: Vector(((``A : 𝒰 _0 ) ~> ((``B : 𝒰 _0 ) ~> ((`$a : ``A ) ~> ((`$b : (``A) → (``B) ) ~> (``B)))),1.0,[(``A :  𝒰 _0) ↦ ((``B :  𝒰 _0) ↦ ((``$a :  ``A) ↦ ((```$b :  (``A) → (``B)) ↦ ((```$b) (``$a))))) : 0.2]))

Conclusions

• Modus Ponens was easily proved by introducing variables.
• We could successfully blend manual setup with bots running.