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.
In [1]:
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
}
)
}
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
Out[2]:
We first make all the statements.
In [3]:
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))
)
Out[3]:
We shall now introduce all the axioms.
In [4]:
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))
Out[4]:
In [5]:
val pf1 = ass1(m)(n)
pf1.typ
Out[5]:
In [6]:
pf1.typ == results(1)
Out[6]:
In [7]:
val mn = mul(m)(n)
val pf2 = ass2(mn)(n)
Out[7]:
In [8]:
pf2.typ
Out[8]:
In [9]:
pf2.typ == results(2)
Out[9]:
In [10]:
Unify.appln(sym, pf2)
Out[10]:
In [11]:
val pf3 = Unify.appln(sym, pf2).get
pf3.typ
Out[11]:
In [12]:
pf3.typ == results(3)
Out[12]:
In [13]:
Unify.appln(leftMul(mn), pf1)
Out[13]:
In [14]:
val pf4 = Unify.appln(leftMul(mn), pf1).get
pf4.typ
pf4.typ == results(4)
Out[14]:
In [15]:
val pf5 = ass1(mn)(m)
pf5.typ
pf5.typ == results(5)
Out[15]:
In [16]:
Unify.appln(trans, pf3)
Out[16]:
In [17]:
val step6 = Unify.appln(trans, pf3).get
Unify.appln(step6, pf4)
Out[17]:
In [18]:
val pf6 = Unify.appln(step6, pf4).get
pf6.typ
pf6.typ == results(6)
Out[18]:
In [19]:
val pf7 = Unify.appln(rightMul(m),pf6).get
pf7.typ
pf7.typ == results(7)
Out[19]:
In [20]:
val step8 = Unify.appln(trans, pf7).get
Out[20]:
In [21]:
val pf8 = Unify.appln(step8, pf5).get
Out[21]:
In [22]:
pf8.typ
pf8.typ == results(8)
Out[22]:
In [23]:
val pf = Unify.appln(sym, pf8).get
pf.typ
pf.typ == results(0)
Out[23]:
In [24]:
val lp1 = LocalProver(TermState(FiniteDistribution.unif(ass1, ass2, m, n, mn), FiniteDistribution.empty)).noIsles.sharpen(10)
Out[24]:
In [25]:
val terms1T = lp1.nextState.map(_.terms).memoize
val r1 = terms1T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
Out[25]:
In [26]:
import monix.execution.Scheduler.Implicits.global
terms1T.runToFuture
In [28]:
val f1 = r1.runToFuture
In [35]:
val lp2 = LocalProver(TermState(FiniteDistribution.unif(pf1, pf2, sym, leftMul, m, n, mn), FiniteDistribution.empty)).noIsles.sharpen(10)
Out[35]:
In [36]:
val terms2T = lp2.nextState.map(_.terms).memoize
val r2 = terms2T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
Out[36]:
In [37]:
terms2T.runToFuture
In [38]:
// 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.
In [39]:
val lp3 = LocalProver(TermState(FiniteDistribution.unif(pf3, pf4, trans), FiniteDistribution.empty)).noIsles
Out[39]:
In [40]:
val terms3T = lp3.nextState.map(_.terms).memoize
val r3 = terms3T.map(fd => results.zipWithIndex.filter{case (tp, n) => fd.map(_.typ)(tp) > 0}).memoize
Out[40]:
In [41]:
terms3T.runToFuture
In [42]:
val f3 = r3.runToFuture
This worked, with a very narrow focus but quickly. We now aim for Lemma 7, which is again right multiplication.
In [43]:
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
Out[43]:
In [44]:
terms4T.runToFuture
In [45]:
val f4 = r4.runToFuture
In [46]:
f4.value
Out[46]:
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.
In [47]:
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
Out[47]:
In [48]:
terms5T.runToFuture
In [49]:
val f5 = r5.runToFuture
In [50]:
f5.value
Out[50]:
We got the theorem with symmetry and transitivity working together.