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. This is a variant where we include $m * n$ as a generator.
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 $
In [1]:
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
}
)
}
Out[1]:
In [2]:
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
Out[2]:
In [3]:
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))
Out[3]:
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.
In [4]:
val fullTerms : FiniteDistribution[Term] = (unif(a,b,c)(m,n, mul(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()
Out[4]:
In [5]:
import monix.execution.Scheduler.Implicits.global
val ts = TermState(fullTerms,fullTerms.map(_.typ))
val lp0 = LocalProver(ts).addGoals(Lemma1 -> 0.1, Lemma2 -> 0.1, Lemma3 -> 0.1, Lemma4 -> 0.1, Lemma5 -> 0.1, Lemma6 -> 0.1, Thm -> 0.4).noIsles
def lp(n: Int) = lp0.sharpen(math.pow(2, n))
Out[5]:
In [6]:
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
Out[6]:
We have set up a task that refines up to timeout. We will run this asynchronously, and then use the final state.
In [7]:
import monix.execution.Scheduler.Implicits.global
val bF = bT.runToFuture
We should look for the above instantiation at least.
In [8]:
val nsT = bT.map(_.get._2).memoize
val lpT = bT.map(_.get._3).memoize
Out[8]:
In [10]:
bF.value
Out[10]:
In [11]:
nsT.map(_.successes).runToFuture
In [12]:
nsT.map(_.successes.map(_._1)).runToFuture
We see that three of the lemmas have been proved:
These are all instantiations, and indeed the ones we want. We should re-run with:
LocalProver used.