Credits: This is work of Achal Kumar.
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$.
Here we try to solve the given problem by identifying the lemmas generated by the LocalProver. We can not add all the axioms in one single distribution because it would not be possible for the LocaProver to generate any relevant lemmas due to combinatorial explosion.
Thus we divide the whole set of axioms ,relevant with the proof into different parts, use the LocalProver on them to get a significant set of lemmas then create distribution which consist of the derrived lemmas and repeat the process until we get the desired result.
In the proof we would be generating following results :
These are the intermediate results that the prover proves and then using them finally proves the desired result
$ m*n = n*m $
import $cp.bin.`provingground-core-jvm-c30de0f4e0.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
import provingground._ , interface._, HoTT._
import learning._
import library._, MonoidSimple._
Here we add the different distributions with each distrtibution focusing attention on differtent thing then these are used in succession to generate lemmas
val M = "M" :: Type
val eqM = "eqM" :: M ->: M ->: Type
// val sym = IdentityTyp.symm(M)
//
// val trans = IdentityTyp.trans(M)
val a = "a" :: M
val b = "b" :: M
val c = "c" :: M
val m = "m" :: M
val n = "n" :: M
val op = "mul" :: M ->: M ->: M
val pl = "plus" :: M ->: M ->: M
import FineDeducer.unif
val putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
eqM(a)(a),
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(op(op(a)(b))(b))(a),
eqM(op(a)(op(a)(b)))(b),
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term) * 0.125) ++ (FiniteDistribution.unif(op : Term ) * 0.375)
val tputn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
eqM(a)(a),
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(op(op(a)(b))(b))(a),
eqM(op(a)(op(a)(b)))(b),
eqM(op(op(m)(n))(n))(m),
eqM(op(m)(op(m)(n)))(n)
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)
val t2putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op, eqM)(
eqM(a)(a),
eqM(a)(b) ->: eqM(b)(a),
eqM(op(op(a)(b))(b))(a),
eqM(op(a)(op(a)(b)))(b),
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)
val t3putn: FiniteDistribution[Term] = unif(a,b,c)(m,n, op,op(m)(n), eqM)(
eqM(a)(b) ->: eqM(b)(a),
eqM(op(op(a)(b))(b))(a),
eqM(op(a)(op(a)(b)))(b),
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)
val t0putn: FiniteDistribution[Term] = unif(a,b,c)(m,n,op, eqM)(
eqM(a)(a),
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
eqM(b)(c) ->: eqM(op(a)(b))(op(a)(c))
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op) * 0.5)
val t0putn1 = t0putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
val putn1 = putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
val tputn1 = tputn.filter((t) => !Set(a, b, c).contains(t)).normalized()
val t2putn1 = t2putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
val t3putn1 = t3putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
Here we use the distribution which focuses attention on terms $m$ , $n$ and $m*n$ to generate lemmas where $m$ , $n$ are the terms we would use to prove the result
import monix.execution.Scheduler.Implicits.global
val ts = TermState(t3putn1,t3putn1.map(_.typ))
val lp = LocalProver(ts, cutoff = 0.000005).noIsles
val lem = lp.lemmas.runSyncUnsafe()
import provingground.{FiniteDistribution => FD}
val x = "lemma1" :: lem(1)._1
val y = "lemma2" :: lem(7)._1
val tputin = FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(b)(c) ->: eqM(op(a)(b))(op(a)(c))
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x ,op(m)(n)) * 0.5)
val tputin1 = tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts1 = TermState(tputin1,tputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))( op(op(m)(n))(op(op(m)(n))(n)))))
val lp1 = LocalProver(ts1, cutoff = 0.000002).noIsles
val lem2 = lp1.lemmas.runSyncUnsafe()
val z = "lemma3" :: lem2(0)._1
val tt2putn = FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(op(op(a)(b))(b))(a),
eqM(op(a)(op(a)(b)))(b)
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, op(m)(n)) * 0.5)
val tt2putn1 = tt2putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts2 = TermState(tt2putn1,tt2putn1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(m)(n))))
val lp2 = LocalProver(ts2, cutoff = 0.00001).noIsles
val lem3 = lp2.lemmas.runSyncUnsafe()
val w = "lemma4" :: lem3(0)._1
val stputin = FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, x, y,z) * 0.5)
val stputin1 = stputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts4 = TermState(stputin1,stputin1.map(_.typ), goals = FD.unif(eqM(op(op(m)(n))(m))(n)) )
val lp4 = LocalProver(ts4, cutoff = 0.00001).noIsles
val lemI = lp4.lemmas.runSyncUnsafe()
val lI = "lemma5" :: lemI(0)._1
val s2tputin = FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(b)(c) ->: eqM(op(b)(a))(op(c)(a))
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, lI) * 0.5)
val s2tputin1 = s2tputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts5 = TermState(s2tputin1,s2tputin1.map(_.typ), goals = FD.unif(eqM(op(op(op(m)(n))(m))(m))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles
val lemI1 = lp5.lemmas.runSyncUnsafe()
val lI1 = "lemma6" :: lemI1(0)._1
val finalstputin = FineDeducer.unif(a,b,c)(m,n,op, eqM)(
eqM(a)(b) ->: eqM(b)(a),
eqM(a)(b) ->: eqM(b)(c) ->: eqM(a)(c),
) * 0.5 ++ (FiniteDistribution.unif(eqM: Term, w, lI1) * 0.5)
val finalstputin1 = finalstputin.filter((t) => !Set(a, b, c).contains(t)).normalized()
val ts5 = TermState(finalstputin1,finalstputin1.map(_.typ), goals = FD.unif(eqM(op(m)(n))(op(n)(m))))
val lp5 = LocalProver(ts5, cutoff = 0.00001).noIsles
lp5.lemmas.runSyncUnsafe()
$ m*n = n*m $ is generated as a lemma in the last LocalProver.