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. 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, 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
In [8]:
val ax = fullTerms.support.find(_.typ == a ~>: (b~>: eqM(mul(mul(a)(b))(b))(a))).get
Out[8]:
In [9]:
val l = fold(ax)(m, n)
Out[9]:
We should look for the above instantiation at least.
In [10]:
val nsT = bT.map(_.get._2).memoize
val lpT = bT.map(_.get._3).memoize
Out[10]:
In [11]:
val lwT = nsT.map(_.terms(l))
Out[11]:
In [13]:
bF.value
Out[13]:
In [14]:
nsT.map(_.successes).runToFuture
In [15]:
val lemmaT = lpT.flatMap(_.lemmas).memoize
Out[15]:
In [16]:
lemmaT.runToFuture
In [17]:
val l1 = "assume" :: Lemma1
val lptT = lpT.flatMap(_.tangentProver(l1).map(_.copy(cutoff = math.pow(10, -4))))
Out[17]:
In [18]:
val s1T = lptT.flatMap(_.successes)
Out[18]:
In [19]:
val s1F = s1T.runToFuture
In [20]:
s1F.map(v => v.map(_._1))
This tangent did not give additional conclusions.
Final remarks: Enough stuff was not generated even after the corrections. We should redo this using only applications and unified applications.