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 $
In [1]:
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
}
)
}
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]:
Above are the ingredients for setting up the problem. Next we define the conclusion and some lemmas.
In [3]:
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)))
)
Out[3]:
In [4]:
val claims = Lemmas.values.toSet + Thm
def results(fd: FiniteDistribution[Term]) = {
val typs = fd.map(_.typ).flatten
claims.filter(t => typs(t) > 0)
}
Out[4]:
We define the axioms, both the properties of equalities and the specific assumptions here.
In [5]:
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))
Out[5]:
We first generate types.
In [6]:
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
Out[6]:
In [7]:
val typsT = lp0.nextState.map(_.typs).memoize
Out[7]:
In [8]:
import monix.execution.Scheduler.Implicits.global
val typsF = typsT.runToFuture
In [9]:
typsF.value
Out[9]:
In [10]:
val cT = typsT.map(typs => claims.map(c => c -> typs(c)))
Out[10]:
In [11]:
val cF = cT.runToFuture
In [12]:
val lp1 = lp0.sharpen(4)
val typs1T = lp1.nextState.map(_.typs).memoize
Out[12]:
In [13]:
val typs1F = typs1T.runToFuture
In [14]:
val c1T = typs1T.map(typs => claims.map(c => c -> typs(c)))
Out[14]:
In [15]:
val c1F = c1T.runToFuture
In [22]:
val lp2 = lp0.sharpen(8)
val typs2T = lp2.nextState.map(_.typs).memoize
Out[22]:
In [23]:
val c2T = typs2T.map(typs => claims.map(c => c -> typs(c)))
Out[23]:
In [24]:
val typs2F = typs2T.runToFuture
In [19]:
typs2F.value
Out[19]:
In [34]:
val c2F = c2T.runToFuture
In [29]:
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)
Out[29]:
In [30]:
val typs3T = lp3.nextState.map(_.typs).memoize
Out[30]:
In [31]:
val typs3F = typs3T.runToFuture
In [39]:
typs3F.value
Out[39]:
In [40]:
val c3T = typs3T.map(typs => claims.map(c => c -> typs(c)))
Out[40]:
In [41]:
val c3F = c3T.runToFuture
In [35]:
lp3
Out[35]:
In [36]:
val lp4 = lp3.sharpen(2)
Out[36]:
In [37]:
val typs4T = lp4.nextState.map(_.typs).memoize
Out[37]:
In [38]:
val typs4F = typs4T.runToFuture
In [45]:
val c4T = typs4T.map(typs => claims.map(c => c -> typs(c)))
Out[45]:
In [46]:
val c4F = c4T.runToFuture
In [47]:
c4F.value
Out[47]:
In [48]:
val lastF = typs4T.map(_.entropyVec.reverse).runToFuture
In [49]:
lastF.value
Out[49]:
In [52]:
val flipped = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))
Out[52]:
In [53]:
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.
In [54]:
val eqT = lp4.equations
Out[54]:
In [55]:
val eqF = eqT.runToFuture
In [56]:
import Expression._, TermRandomVars._
Out[56]:
In [57]:
import GeneratorVariables._
val lhs = FinalVal(Elem(flipped, Typs))
Out[57]:
In [58]:
val rhsT = eqT.map(eqs => eqs.find(_.lhs == lhs).map(_.rhs))
Out[58]:
In [59]:
rhsT.runToFuture
In [62]:
val lhs1 = FinalVal(Elem(flipped, Terms))
val rhs1T = eqT.map(eqs => eqs.find(_.lhs == lhs1).map(_.rhs))
Out[62]:
In [64]:
val rF = rhs1T.runToFuture
In [65]:
rF.value
Out[65]:
In [ ]: