This is the first pass at annotating Achal Kumar's solution to the Putnam problem. Here we will not explore alternative runs, but mostly add notes with a little cleaning up. Some general observations:
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-0b6bd9c864.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
import library._, MonoidSimple._
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 op = "mul" :: M ->: M ->: M
val pl = "plus" :: M ->: M ->: M
import FineDeducer.unif
We have imported from the Monoid library, which has many things in common with the current problem.
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)
The above is the basic generating model. This has no instantiations. It is not actually used, but is kept here as it is the most canonical. We have removed t
private 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 t3putn1 = t3putn.filter((t) => !Set(a, b, c).contains(t)).normalized()
We make the first local prover with the above. This has symmetry for equality, but not transitivity or $ap_f$.
import monix.execution.Scheduler.Implicits.global
val ts = TermState(t3putn1,t3putn1.map(_.typ))
val lp = LocalProver(ts, cutoff = 0.000005).noIsles
We run this, synchronously for now, and get lemmas.
val lem = lp.lemmas.runSyncUnsafe()
At this stage we make a choice, picking the second and eighth lemma for use. Only the second is used immediately, so we would clearly not get stuck here.
import provingground.{FiniteDistribution => FD}
val x = "lemma1" :: lem(1)._1
val y = "lemma2" :: lem(7)._1
x.typ
y.typ
The lemmas we have picked are:
private 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
We have set up our second local prover. This uses the lemma x, i.e. Lemma 1 and also transport of equality under left multiplication, but nothing else.
val lem2 = lp1.lemmas.runSyncUnsafe()
val z = "lemma3" :: lem2(0)._1
z.typ
In this case z, i.e. Lemma 3 is the overwhelmingly dominant lemma, so natural to pick. It has type:
private 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
We set up the next local prover. This has no lemmas proved along the way, but is focussed on using the given axioms without any properties of equality.
val lem3 = lp2.lemmas.runSyncUnsafe()
We note that this ran quickly, and all it gave was an instantiation of one of the properties (as we would expect). We pick up another lemma.
val w = "lemma4" :: lem3(0)._1
w.typ
The lemma we have obtained is
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
We are looking for consequences of our first three lemmas. This should give the crucial Lemma 5.
val lemI = lp4.lemmas.runSyncUnsafe()
val lI = "lemma5" :: lemI(0)._1
lI.typ
We obtain a crucial lemma. Note that this is not instantiation.
private 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
We setup yet another local prover. Here we are looking for consequences of Lemma 5, which was just discovered.
val lemI1 = lp5.lemmas.runSyncUnsafe()
val lI1 = "lemma6" :: lemI1(0)._1
lI1.typ
Note that the above ran almost instantly. The lemma we obtained is:
private 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
We set up our final step. This uses Lemmas 4 and 6 from earlier.
lp5.lemmas.runSyncUnsafe()
This is the conclusion.