notebook.community

Edit and run

We attempt to replicate the Monoid proof but with our new workflow and with the local provers, using only unified applications.



In [1]:

    
import $cp.bin.`provingground-core-jvm-3d48753.fat.jar`









    Out[1]:





import $cp.$



In [2]:

    
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}









    Out[2]:





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



In [3]:

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









    Out[3]:





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

import learning._

import library._, MonoidSimple._



In [4]:

    
val tg = TermGenParams.zero.copy(unAppW = 0.2)
val ts = TermState(dist1, dist1.map(_.typ))









    Out[4]:





tg: TermGenParams = TermGenParams(
  0.0,
  0.2,
  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
)
ts: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(e_l, 0.047619047619047616),
      Weighted(e_r, 0.047619047619047616),
      Weighted(mul, 0.047619047619047616),
      Weighted(eqM, 0.047619047619047616),
      Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
      Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
      Weighted(
        axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
        0.047619047619047616
      ),
      Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
      Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
      Weighted(eqM, 0.2857142857142857),
      Weighted(mul, 0.2857142857142857)
    )
  ),
  FiniteDistribution(
    Vector(
      Weighted(M, 0.047619047619047616),
      Weighted(M, 0.047619047619047616),
      Weighted((M → (M → M)), 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.047619047619047616),
      Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
      Weighted(
        ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
        0.047619047619047616
      ),
      Weighted(
        ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
        0.047619047619047616
      ),
      Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
      Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
      Weighted((M → (M → 𝒰 )), 0.2857142857142857),
      Weighted((M → (M → M)), 0.2857142857142857)
...



In [5]:

    
val lp = LocalProver(ts, tg)









    Out[5]:





lp: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e_l, 0.047619047619047616),
        Weighted(e_r, 0.047619047619047616),
        Weighted(mul, 0.047619047619047616),
        Weighted(eqM, 0.047619047619047616),
        Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.047619047619047616
        ),
        Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
        Weighted(eqM, 0.2857142857142857),
        Weighted(mul, 0.2857142857142857)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.047619047619047616),
        Weighted(M, 0.047619047619047616),
        Weighted((M → (M → M)), 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.047619047619047616),
        Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.047619047619047616
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.047619047619047616
        ),
        Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.2857142857142857),
...



In [6]:

    
import monix.execution.Scheduler.Implicits.global









    Out[6]:





import monix.execution.Scheduler.Implicits.global



In [7]:

    
val lemT = lp.lemmas









    Out[7]:





lemT: monix.eval.Task[Vector[(Typ[Term], Double)]] = Async(
  <function2>,
  false,
  true,
  true
)



In [8]:

    
val lemF = lemT.runToFuture









    





lemF: monix.execution.CancelableFuture[Vector[(Typ[Term], Double)]] = Success(
  Vector(
    (eqM(e_r)(e_r), 1.0578745194563616E-4),
    (eqM(e_l)(e_l), 1.0578745194563616E-4),
    (eqM(e_l)(mul(e_l)(e_r)), 3.9209752320968364E-5),
    (eqM(e_l)(mul(e_l)(e_l)), 3.9209752320968364E-5),
    (eqM(e_r)(mul(e_l)(e_r)), 3.9209752320968364E-5),
    (eqM(e_r)(mul(e_r)(e_r)), 3.9209752320968364E-5),
    (eqM(mul(e_l)(e_r))(e_l), 1.1673930754169824E-5),
    (eqM(mul(e_l)(e_l))(e_l), 1.1673930754169824E-5),
    (eqM(mul(e_l)(e_r))(e_r), 1.1673930754169824E-5),
    (eqM(mul(e_r)(e_r))(e_r), 1.1673930754169824E-5)
  )
)



In [9]:

    
val lem = eqM(l)(op(l)(r))
val tangS = ts.tangent("proof" :: lem)









    Out[9]:





lem: Typ[Term] = eqM(e_l)(mul(e_l)(e_r))
tangS: TermState = TermState(
  FiniteDistribution(Vector(Weighted(proof, 1.0))),
  FiniteDistribution(Vector()),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)



In [10]:

    
val goal = eqM(l)(r)
val lpTangT  = lp.distTangentProver(FiniteDistribution.unif("proof" :: lem))
val targGoalT = lpTangT.flatMap(lpt => lpt.theoremsByStatement).map(_(goal))









    Out[10]:





goal: Typ[Term] = eqM(e_l)(e_r)
lpTangT: monix.eval.Task[LocalTangentProver] = FlatMap(
  Map(
    Async(<function2>, false, true, true),
    provingground.learning.LocalProver$$Lambda$3055/1967470927@749bd4b2,
    0
  ),
  provingground.learning.LocalProver$$Lambda$3056/91428110@151a7801
)
targGoalT: monix.eval.Task[Double] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        provingground.learning.LocalProver$$Lambda$3055/1967470927@749bd4b2,
        0
      ),
      provingground.learning.LocalProver$$Lambda$3056/91428110@151a7801
    ),
    ammonite.$sess.cmd9$Helper$$Lambda$3057/2060264848@6f468bdc
  ),
  ammonite.$sess.cmd9$Helper$$Lambda$3058/1264621820@3985c81c,
  0
)



In [11]:

    
val targGoalF = targGoalT.runToFuture









    





targGoalF: monix.execution.CancelableFuture[Double] = Success(0.0358205554070143)

Conclusions

When we draw attention to what we want in an extreme way, at least then we get the result.
A warning is that lemmas were misidentified here.



In [18]:

    
val tg1 = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)









    Out[18]:





tg1: 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.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0
)



In [19]:

    
val lp1 = LocalProver(ts, tg1)









    Out[19]:





lp1: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(e_l, 0.047619047619047616),
        Weighted(e_r, 0.047619047619047616),
        Weighted(mul, 0.047619047619047616),
        Weighted(eqM, 0.047619047619047616),
        Weighted(axiom_{eqM(a)(a)}, 0.047619047619047616),
        Weighted(axiom_{(eqM(a)(b) \to eqM(b)(a))}, 0.047619047619047616),
        Weighted(
          axiom_{(eqM(a)(b) \to (eqM(b)(c) \to eqM(a)(c)))},
          0.047619047619047616
        ),
        Weighted(axiom_{eqM(mul(e_l)(a))(a)}, 0.047619047619047616),
        Weighted(axiom_{eqM(mul(a)(e_r))(a)}, 0.047619047619047616),
        Weighted(eqM, 0.2857142857142857),
        Weighted(mul, 0.2857142857142857)
      )
    ),
    FiniteDistribution(
      Vector(
        Weighted(M, 0.047619047619047616),
        Weighted(M, 0.047619047619047616),
        Weighted((M → (M → M)), 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.047619047619047616),
        Weighted(∏(a : M){ eqM(a)(a) }, 0.047619047619047616),
        Weighted(
          ∏(a : M){ ∏(b : M){ (eqM(a)(b) → eqM(b)(a)) } },
          0.047619047619047616
        ),
        Weighted(
          ∏(a : M){ ∏(b : M){ ∏(c : M){ (eqM(a)(b) → (eqM(b)(c) → eqM(a)(c))) } } },
          0.047619047619047616
        ),
        Weighted(∏(a : M){ eqM(mul(e_l)(a))(a) }, 0.047619047619047616),
        Weighted(∏(a : M){ eqM(mul(a)(e_r))(a) }, 0.047619047619047616),
        Weighted((M → (M → 𝒰 )), 0.2857142857142857),
...



In [20]:

    
val lemT1 = lp1.lemmas









    Out[20]:





lemT1: monix.eval.Task[Vector[(Typ[Term], Double)]] = Async(
  <function2>,
  false,
  true,
  true
)



In [21]:

    
val lemF1 = lemT1.runToFuture









    





lemF1: monix.execution.CancelableFuture[Vector[(Typ[Term], Double)]] = Success(
  Vector(
    (eqM(e_r)(e_r), 0.0027509184472828325),
    (eqM(e_l)(e_l), 0.0027509184472828325),
    (eqM(e_l)(mul(e_l)(e_r)), 0.0012526844961492322),
    (eqM(e_l)(mul(e_l)(e_l)), 0.0012526844961492322),
    (eqM(e_r)(mul(e_l)(e_r)), 0.0012526844961492322),
    (eqM(e_r)(mul(e_r)(e_r)), 0.0012526844961492322)
  )
)



In [22]:

    
val lpTangT1  = lp1.distTangentProver(FiniteDistribution.unif("proof" :: lem))
val targGoalT1 = lpTangT1.flatMap(lpt => lpt.theoremsByStatement).map(_(goal))









    Out[22]:





lpTangT1: monix.eval.Task[LocalTangentProver] = FlatMap(
  Map(
    Async(<function2>, false, true, true),
    provingground.learning.LocalProver$$Lambda$3055/1967470927@383b4579,
    0
  ),
  provingground.learning.LocalProver$$Lambda$3056/91428110@54a814f7
)
targGoalT1: monix.eval.Task[Double] = Map(
  FlatMap(
    FlatMap(
      Map(
        Async(<function2>, false, true, true),
        provingground.learning.LocalProver$$Lambda$3055/1967470927@383b4579,
        0
      ),
      provingground.learning.LocalProver$$Lambda$3056/91428110@54a814f7
    ),
    ammonite.$sess.cmd21$Helper$$Lambda$3234/916371667@3e84a7d0
  ),
  ammonite.$sess.cmd21$Helper$$Lambda$3235/315745996@3dbbc5b4,
  0
)



In [23]:

    
val targGoalF1 = targGoalT1.runToFuture









    





targGoalF1: monix.execution.CancelableFuture[Double] = Success(0.03607619269409383)

Conclusions: round two

Having both applications and unified ones is a reasonable thing to try.
The theorem was proved in this case.
However lemmas were again not identified properly