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.
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.
Since we want to separate out symmetry, we have added two more.
Finally, we should get the desired result.
$ m*n = n*m $
import $cp.bin.`provingground-core-jvm-f6dcab932f.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
Above are the ingredients for setting up the problem. Next we define the conclusion and some lemmas.
val Thm = eqM(mul(m)(n))(mul(n)(m))
val Lemmas =
Map(
1 -> eqM(m)(mul(mul(m)(n))(n)),
2 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
3 -> eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
4 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)),
5 -> eqM(mul(mul(m)(n))(m))(n),
6 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)),
7 -> eqM(mul(mul(m)(n))(n))(m),
8 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n)))
)
val claims = Lemmas.values.toSet + Thm
def results(fd: FiniteDistribution[Term]) = {
val typs = fd.map(_.typ).flatten
claims.filter(t => typs(t) > 0)
}
We define the axioms, both the properties of equalities and the specific assumptions here.
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)))(a))
We first generate types.
val ts0 = TermState(FiniteDistribution(eqM -> 0.2, mul -> 0.35, m -> 0.15, n -> 0.15, mul(m)(n) -> 0.15), FiniteDistribution.unif(M))
val tg0 = TermGenParams.zero.copy(appW = 0.15, typAsCodW = 0.1)
val lp0 = LocalProver(ts0, tg = tg0).noIsles
val typsT = lp0.nextState.map(_.typs).memoize
import monix.execution.Scheduler.Implicits.global
val typsF = typsT.runToFuture
typsF.value
val cT = typsT.map(typs => claims.map(c => c -> typs(c)))
val cF = cT.runToFuture
This is one of many variants tried. It ran quickly, but left three theorems with 0 weight. We now sharpen this and try again.
val lp1 = lp0.sharpen(4)
val typs1T = lp1.nextState.map(_.typs).memoize
val typs1F = typs1T.runToFuture
val c1T = typs1T.map(typs => claims.map(c => c -> typs(c)))
val c1F = c1T.runToFuture
val lp2 = lp0.sharpen(8)
val typs2T = lp2.nextState.map(_.typs).memoize
val c2T = typs2T.map(typs => claims.map(c => c -> typs(c)))
val typs2F = typs2T.runToFuture
typs2F.value
val c2F = c2T.runToFuture
mul having high priority, and equality very low.val ts3 = TermState(FiniteDistribution(eqM -> 0.05, mul -> 0.5, m -> 0.15, n -> 0.15, mul(m)(n) -> 0.15), FiniteDistribution.unif(M))
val lp3 = LocalProver(ts3, tg = tg0).noIsles.sharpen(4)
val typs3T = lp3.nextState.map(_.typs).memoize
val typs3F = typs3T.runToFuture
typs3F.value
val c3T = typs3T.map(typs => claims.map(c => c -> typs(c)))
val c3F = c3T.runToFuture
lp3
val lp4 = lp3.sharpen(2)
val typs4T = lp4.nextState.map(_.typs).memoize
val typs4F = typs4T.runToFuture
val c4T = typs4T.map(typs => claims.map(c => c -> typs(c)))
val c4F = c4T.runToFuture
c4F.value
val lastF = typs4T.map(_.entropyVec.reverse).runToFuture
lastF.value
val flipped = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))
val pF = typs4T.map(_(flipped)).runToFuture
Note that the flipped form of a missing lemma is indeed generated. We can try to look for the equations.
val eqT = lp4.equations
val eqF = eqT.runToFuture
import Expression._, TermRandomVars._
import GeneratorVariables._
val lhs = FinalVal(Elem(flipped, Typs))
val rhsT = eqT.map(eqs => eqs.find(_.lhs == lhs).map(_.rhs))
rhsT.runToFuture
val lhs1 = FinalVal(Elem(flipped, Terms))
val rhs1T = eqT.map(eqs => eqs.find(_.lhs == lhs1).map(_.rhs))
val rF = rhs1T.runToFuture
rF.value