Our goal is to explore the solution of Achal Kumar. Specifically, we will start with all axioms and the constants $m$ and $n$ and then look for lemmas. The difference from the other notebook is we only use (unified) applications. Recall the problem:
Let ⋆ be a binary operation on a nonempty set $M$. That is, every pair $(a,b) \in M$ is assigned an element $a$ ⋆$ b$ in $M$. Suppose that ⋆ has the additional property that $(a $ ⋆ $b) $ ⋆$ b= a$ and $a$ ⋆ $(a$ ⋆$ b)= b$ for all $a,b \in M$. Show that $a$ ⋆ $b = b$ ⋆ $a$ for all $a,b \in M$.
We should derive the following lemmas.
Finally, we should get the desired result.
$ m*n = n*m $
import $cp.bin.`provingground-core-jvm-6b59061b0d.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
val M = "M" :: Type
val eqM = "eqM" :: M ->: M ->: Type
val a = "a" :: M
val b = "b" :: M
val c = "c" :: M
val m = "m" :: M
val n = "n" :: M
val mul = "mul" :: M ->: M ->: M
import FineDeducer.unif
val Thm = eqM(mul(m)(n))(mul(n)(m))
val Lemma1 = eqM(m)(mul(mul(m)(n))(n))
val Lemma2 = eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n)))
val Lemma3 = eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n)))
val Lemma4 = eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n))
val Lemma5 = eqM(mul(mul(m)(n))(m))(n)
val Lemma6 = eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m))
Note that the above are defined just by using copy-paste (this is why we changed op to mul). We set up a local prover with all the axioms we use.
val fullTerms : FiniteDistribution[Term] = (unif(a,b,c)(m,n, mul, eqM)(
eqM(a)(a),
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(mul(mul(a)(b))(b))(a),
eqM(mul(a)(mul(a)(b)))(b),
eqM(b)(c) ->: eqM(mul(b)(a))(mul(c)(a))
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term) * 0.125) ++ (FiniteDistribution.unif(mul : Term ) * 0.375)).filter((t) => !Set(a, b, c).contains(t)).normalized()
import monix.execution.Scheduler.Implicits.global
val ts = TermState(fullTerms,fullTerms.map(_.typ))
val lp0 = LocalProver(ts, tg = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1)).addGoals(
Lemma1 -> 0.1, Lemma2 -> 0.1, Lemma3 -> 0.1, Lemma4 -> 0.1, Lemma5 -> 0.1, Lemma6 -> 0.1, Thm -> 0.4)
def lp(n: Int) = lp0.sharpen(math.pow(2, n))
def nslp(n: Int) = {
val lpc = lp(n)
lpc.nextState.map{ns => (n, ns, lpc)}
}
val bT = Utils.bestTask((1 to 30).map(nslp)).memoize
We have set up a task that refines up to timeout. We will run this asynchronously, and then use the final state.
import monix.execution.Scheduler.Implicits.global
val bF = bT.runToFuture
val ax = fullTerms.support.find(_.typ == a ~>: (b~>: eqM(mul(mul(a)(b))(b))(a))).get
val l = fold(ax)(m, n)
We should look for the above instantiation at least.
val nsT = bT.map(_.get._2).memoize
val lpT = bT.map(_.get._3).memoize
val lwT = nsT.map(_.terms(l))
bF.value
nsT.map(_.successes).runToFuture
We see that two of the lemmas have been proved:
Both these are simple instantiations, but they get us started. The basic statement missing in Lemma 2. We should look at all the generated lemmas.
val lemmaT = lpT.flatMap(_.lemmas).memoize
lemmaT.runToFuture
Final remarks: Even less was generated when there were fewer generators, which is expected as we went to 5 steps both times.