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.



In [1]:

    
import $cp.bin.`provingground-core-jvm-6a7a553306.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._



In [2]:

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

First we set things up.



In [3]:

    
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), goals = FiniteDistribution.unif(MP))
val tg = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)
val lp = LocalProver(ts, tg)
import HoTTMessages._









    Out[3]:





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(Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0))
  ),
  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(Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0))
    ),
    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,
...
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.



In [4]:

    
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)))
val ws3 = ws2.flatMap(w => w.act(HoTTBot.fullGoalInContext ))
val ws4 = ws3.flatMap(w => w.act(HoTTBot.goalToProver(0.3, 0.7)))
val ws5 = ws4.flatMap(w => w.act(HoTTBot.lpToFinalState ))
val ws6 = ws5.flatMap(w => w.act(HoTTBot.reportSuccesses ))









    





web: HoTTPostWeb = provingground.learning.HoTTPostWeb@2f96de42
ws: WebState[HoTTPostWeb, (Int, Int)] = WebState(
  provingground.learning.HoTTPostWeb@2f96de42,
  Vector()
)
ws1: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    Vector(
      PostData(
        LocalProver(
          TermState(
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector(),
            FiniteDistribution(Vector()),
            FiniteDistribution(
              Vector(
                Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0)
              )
            ),
            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(
...
ws2: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    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(
                Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0)
              )
            ),
            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,
...
ws3: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    Vector(
      PostData(
        SeekGoal(
          B,
          AppendVariable(
            AppendVariable(AppendVariable(AppendVariable(Empty, A), B), $a),
            $b
          ),
          Set()
        ),
        (3, -424370462)
      ),
      PostData(
        LocalProver(
          TermState(
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector(),
            FiniteDistribution(Vector()),
            FiniteDistribution(
              Vector(
                Weighted(∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } }, 1.0)
              )
            ),
            Empty
          ),
          TermGenParams(
            0.1,
            0.1,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
            0.0,
...
ws4: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    Vector(
      PostData(
        LocalProver(
          TermState(
            FiniteDistribution(
              Vector(
                Weighted(𝒰 , 0.24009999999999995),
                Weighted(A, 0.1029),
                Weighted(B, 0.14700000000000002),
                Weighted($a, 0.21000000000000002),
                Weighted($b, 0.3)
              )
            ),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector($b, $a, B, A),
            FiniteDistribution(Vector()),
            FiniteDistribution(
              Vector(
                Weighted(
                  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } },
                  0.30000000000000004
                ),
                Weighted(B, 0.7)
              )
            ),
            AppendVariable(
              AppendVariable(AppendVariable(AppendVariable(Empty, A), B), $a),
              $b
            )
          ),
          TermGenParams(
            0.1,
            0.1,
            0.0,
            0.0,
            0.0,
...
ws5: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    Vector(
      PostData(
        FinalState(
          TermState(
            FiniteDistribution(
              Vector(
                Weighted($b, 0.24000000000000005),
                Weighted(𝒰 , 0.19208000000000003),
                Weighted(B, 0.11760000000000005),
                Weighted(A, 0.08232000000000002),
                Weighted($b($a), 0.20000000000000007),
                Weighted($a, 0.16800000000000007)
              )
            ),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector($b, $a, B, A),
            FiniteDistribution(Vector()),
            FiniteDistribution(
              Vector(
                Weighted(
                  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } },
                  0.30000000000000004
                ),
                Weighted(B, 0.7)
              )
            ),
            AppendVariable(
              AppendVariable(AppendVariable(AppendVariable(Empty, A), B), $a),
              $b
            )
          )
        ),
        (6, -1306168695)
      ),
      PostData(
        FinalState(
...
ws6: concurrent.Future[WebState[HoTTPostWeb, (Int, Int)]] = Success(
  WebState(
    provingground.learning.HoTTPostWeb@2f96de42,
    Vector(
      PostData(
        FinalState(
          TermState(
            FiniteDistribution(
              Vector(
                Weighted($b, 0.24000000000000005),
                Weighted(𝒰 , 0.19208000000000003),
                Weighted(B, 0.11760000000000005),
                Weighted(A, 0.08232000000000002),
                Weighted($b($a), 0.20000000000000007),
                Weighted($a, 0.16800000000000007)
              )
            ),
            FiniteDistribution(Vector(Weighted(𝒰 , 1.0))),
            Vector($b, $a, B, A),
            FiniteDistribution(Vector()),
            FiniteDistribution(
              Vector(
                Weighted(
                  ∏(A : 𝒰 ){ ∏(B : 𝒰 ){ (A → ((A → B) → B)) } },
                  0.30000000000000004
                ),
                Weighted(B, 0.7)
              )
            ),
            AppendVariable(
              AppendVariable(AppendVariable(AppendVariable(Empty, A), B), $a),
              $b
            )
          )
        ),
        (6, -1306168695)
      ),
      PostData(
        FinalState(
...



In [5]:

    
Utils.reportText









    Out[5]:





res4: String = Success: Vector(((``A : 𝒰 _0 ) ~> ((``B : 𝒰 _0 ) ~> ((`$a : ``A ) ~> ((`$b : (``A) → (``B) ) ~> (``B)))),0.7,[(``A :  𝒰 _0) ↦ ((``B :  𝒰 _0) ↦ ((``$a :  ``A) ↦ ((```$b :  (``A) → (``B)) ↦ ((```$b) (``$a))))) : 0.20000000000000007]))

Conclusion

Modus Ponens was easily proved by introducing variables.