We visit the problem once more. This time we are looking for whether things work following heuristics implemented by hand. We will also be more explicit in naming stuff. We will also have a few more steps, which are flips of the earlier steps. In some cases we only consider the flips. This time we will not try to generate statements of lemmas, as this was (barely) successful last time.
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 derive the following results.
In this notebook we do not consider selection of the correct lemmas, but just the generation.
import $cp.bin.`provingground-core-jvm-a09844e8fb.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
We first make all the statements.
val results = Vector(
eqM(mul(m)(n))(mul(n)(m)),
eqM(mul(mul(m)(n))(n))(m),
eqM(mul(mul(m)(n))(mul(mul(m)(n))(n)))(n),
eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
eqM(mul(mul(m)(n))(mul(mul(m)(n))(n)))(mul(mul(m)(n))(m)),
eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)),
eqM(n)(mul(mul(m)(n))(m)),
eqM(mul(n)(m))(mul(mul(mul(m)(n))(m))(m)),
eqM(mul(n)(m))(mul(m)(n))
)
We shall now introduce all the axioms.
val refl = "refl" :: a ~>: (eqM(a)(a))
val sym = "sym" :: a ~>: (b ~>: (eqM(a)(b) ->: eqM(b)(a)))
val trans =
"trans" :: a ~>:
(b ~>: (c ~>: ((eqM(a)(b)) ->: (eqM(b)(c)) ->: (eqM(a)(c)))))
val leftMul = "left-multiply" :: a ~>: (b ~>: (c ~>: (eqM(b)(c) ->: eqM(mul(a)(b))(mul(a)(c)))))
val rightMul = "right-multiply" :: a ~>: (b ~>: (c ~>: (eqM(b)(c) ->: eqM(mul(b)(a))(mul(c)(a)))))
val ass1 = "ass1" :: a ~>: (b ~>: eqM(mul(mul(a)(b))(b))(a))
val ass2 = "ass2" :: a ~>: (b ~>: eqM(mul(a)(mul(a)(b)))(b))
Before considering proof discovery, we look for proof representation.
val pf1 = ass1(m)(n)
pf1.typ
pf1.typ == results(1)
val mn = mul(m)(n)
val pf2 = ass2(mn)(n)
pf2.typ
pf2.typ == results(2)
Unify.appln(sym, pf2)
val pf3 = Unify.appln(sym, pf2).get
pf3.typ
pf3.typ == results(3)
Unify.appln(leftMul(mn), pf1)
val pf4 = Unify.appln(leftMul(mn), pf1).get
pf4.typ
pf4.typ == results(4)
val pf5 = ass1(mn)(m)
pf5.typ
pf5.typ == results(5)
Unify.appln(trans, pf3)
val step6 = Unify.appln(trans, pf3).get
Unify.appln(step6, pf4)
val pf6 = Unify.appln(step6, pf4).get
pf6.typ
pf6.typ == results(6)
val pf7 = Unify.appln(rightMul(m),pf6).get
pf7.typ
pf7.typ == results(7)
val step8 = Unify.appln(trans, pf7).get
val pf8 = Unify.appln(step8, pf5).get
pf8.typ
pf8.typ == results(8)
val pf = Unify.appln(sym, pf8).get
pf.typ
pf.typ == results(0)
val lp1 = LocalProver(TermState(FiniteDistribution.unif(ass1, ass2, m, n, mn), FiniteDistribution.empty)).noIsles.sharpen(10)
val terms1T = lp1.nextState.map(_.terms).memoize
val r1 = terms1T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
import monix.execution.Scheduler.Implicits.global
terms1T.runToFuture
val f1 = r1.runToFuture
We see that all the instantiation lemmas have been obtained.
val lp2 = LocalProver(TermState(FiniteDistribution.unif(pf1, pf2, sym, leftMul, m, n, mn), FiniteDistribution.empty)).noIsles.sharpen(10)
val terms2T = lp2.nextState.map(_.terms).memoize
val r2 = terms2T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
terms2T.runToFuture
// val r2 = terms2T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
val f2 = r2.runToFuture
The consequences 3 and 4 were found with moderately focussed generation. We next try using transitivity. This will be very focussed but with a lower cutoff.
val lp3 = LocalProver(TermState(FiniteDistribution.unif(pf3, pf4, trans), FiniteDistribution.empty)).noIsles
val terms3T = lp3.nextState.map(_.terms).memoize
val r3 = terms3T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
terms3T.runToFuture
val f3 = r3.runToFuture
This worked, with a very narrow focus but quickly. We now aim for Lemma 7, which is again right multiplication.
val lp4 = LocalProver(TermState(FiniteDistribution.unif(pf6, rightMul, m, n, mn), FiniteDistribution.empty)).noIsles
val terms4T = lp4.nextState.map(_.terms).memoize
val r4 = terms4T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
terms4T.runToFuture
val f4 = r4.runToFuture
f4.value
The Lemma 7 was obtained with a fairly focus, but with the default cutoff. We now look for Lemma 8 and the Theorem. It will probably take two steps.
val lp5 = LocalProver(TermState(FiniteDistribution.unif(pf5, pf7, sym, trans), FiniteDistribution.empty)).noIsles.sharpen(10)
val terms5T = lp5.nextState.map(_.terms).memoize
val r5 = terms5T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
terms5T.runToFuture
val f5 = r5.runToFuture
f5.value
We got the theorem with symmetry and transitivity working together.