The Czech-Slovak Olympiad problem: Exploring steps.

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.

The problem

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.

  1. $ m = (m*n)*n $
  2. $ n = (m*n)*((m*n)*n) $
  3. $ (m*n)*m = (m*n)*((m*n)*n) $
  4. $ ((m*n)*m))*m = m*n $
  5. $ (m*n)*m = n $
  6. $ ((m*n)*m)*m = n*m $
  7. $ (m*n)*n = m $
  8. $ (m*n)*((m*n)*n) = n$

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]:
import $cp.$                                              

import provingground._ , interface._, HoTT._, learning._ 

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]:
M: Typ[Term] = M
eqM: Func[Term, Func[Term, Typ[Term]]] = eqM
a: Term = a
b: Term = b
c: Term = c
m: Term = m
n: Term = n
mul: Func[Term, Func[Term, Term]] = mul

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]:
Thm: Typ[Term] = eqM(mul(m)(n))(mul(n)(m))
Lemmas: Map[Int, Typ[Term]] = Map(
  5 -> eqM(mul(mul(m)(n))(m))(n),
  1 -> eqM(m)(mul(mul(m)(n))(n)),
  6 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)),
  2 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
  7 -> eqM(mul(mul(m)(n))(n))(m),
  3 -> eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
  8 -> eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
  4 -> eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n))
)

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]:
claims: Set[Typ[Term]] = Set(
  eqM(mul(m)(n))(mul(n)(m)),
  eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)),
  eqM(mul(mul(m)(n))(n))(m),
  eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))),
  eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
  eqM(m)(mul(mul(m)(n))(n)),
  eqM(mul(mul(m)(n))(m))(n),
  eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n))
)
defined function results

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]:
refl: FuncLike[Term, Term] = refl
sym: FuncLike[Term, FuncLike[Term, Func[Term, Term]]] = sym
trans: FuncLike[Term, FuncLike[Term, FuncLike[Term, Func[Term, Func[Term, Term]]]]] = trans
leftMul: FuncLike[Term, FuncLike[Term, FuncLike[Term, Func[Term, Term]]]] = left-multiply
rightMul: FuncLike[Term, FuncLike[Term, FuncLike[Term, Func[Term, Term]]]] = right-multiply
ass1: FuncLike[Term, FuncLike[Term, Term]] = ass1
ass2: FuncLike[Term, FuncLike[Term, Term]] = ass2

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]:
ts0: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM, 0.2),
      Weighted(mul, 0.35),
      Weighted(m, 0.15),
      Weighted(n, 0.15),
      Weighted(mul(m)(n), 0.15)
    )
  ),
  FiniteDistribution(Vector(Weighted(M, 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
tg0: TermGenParams = TermGenParams(
  0.15,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.0,
  0.1,
  0.0,
  0.3,
  0.7,
  0.5,
  0.0,
  0.0,
  0.0,
  OrElse(
    OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
    <function1>
  )
)
lp0: LocalProver = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.2),
        Weighted(mul, 0.35),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...

In [7]:
val typsT = lp0.nextState.map(_.typs).memoize


Out[7]:
typsT: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)

In [8]:
import monix.execution.Scheduler.Implicits.global
val typsF = typsT.runToFuture



In [9]:
typsF.value


Out[9]:
res8: Option[scala.util.Try[FiniteDistribution[Typ[Term]]]] = Some(
  Success(
    FiniteDistribution(
      Vector(
        Weighted(eqM(mul(m)(n))(mul(mul(m)(n))(m)), 0.0019482628977741422),
        Weighted(eqM(m)(mul(m)(mul(mul(m)(n))(n))), 1.5513100356983803E-4),
        Weighted(eqM(m)(mul(m)(mul(n)(n))), 1.5513100356983803E-4),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(m)(mul(m)(n))),
          3.498052041280661E-4
        ),
        Weighted(eqM(mul(n)(m))(mul(m)(mul(m)(n))), 3.498052041280661E-4),
        Weighted(eqM(mul(mul(m)(n))(n))(n), 8.377074192771253E-4),
        Weighted(eqM(n)(mul(m)(mul(n)(m))), 1.5513100356983803E-4),
        Weighted(eqM(m)(mul(mul(m)(n))(mul(m)(n))), 0.0017840065410531375),
        Weighted(eqM(mul(m)(m))(mul(n)(mul(m)(n))), 3.498052041280661E-4),
        Weighted(eqM(mul(n)(m))(n), 8.377074192771253E-4),
        Weighted(eqM(mul(m)(n))(mul(m)(mul(m)(n))), 0.002133811745181203),
        Weighted(eqM(mul(n)(mul(m)(n)))(n), 8.377074192771253E-4),
        Weighted(
          eqM(mul(m)(mul(m)(n)))(mul(n)(mul(m)(n))),
          3.498052041280661E-4
        ),
        Weighted(
          eqM(mul(m)(n))(mul(m)(mul(mul(m)(n))(mul(m)(n)))),
          1.8554884740706117E-4
        ),
        Weighted(eqM(mul(m)(m))(m), 8.377074192771253E-4),
        Weighted(eqM(mul(m)(n))(mul(n)(m)), 0.0019482628977741422),
        Weighted(eqM(mul(n)(mul(m)(n)))(mul(m)(m)), 3.19387360290843E-4),
        Weighted(eqM(mul(n)(m))(mul(m)(n)), 0.0011570947795679681),
        Weighted(eqM(mul(n)(n))(mul(m)(mul(m)(n))), 3.498052041280661E-4),
        Weighted(eqM(n)(mul(mul(m)(n))(m)), 0.0016288755374832997),
        Weighted(eqM(mul(m)(m))(mul(m)(n)), 0.0011570947795679681),
        Weighted(eqM(mul(mul(m)(n))(m))(mul(n)(m)), 3.19387360290843E-4),
        Weighted(
          eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(m)(n))),
          3.498052041280661E-4
        ),
...

In [10]:
val cT = typsT.map(typs => claims.map(c => c -> typs(c)))


Out[10]:
cT: monix.eval.Task[Set[(Typ[Term], Double)]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd9$Helper$$Lambda$2890/294412784@555f2bd0,
  0
)

In [11]:
val cF = cT.runToFuture


First step

This is one of many variants tried. It ran quickly, but left three theorems with 0 weight. We now sharpen this and try again.


In [12]:
val lp1 = lp0.sharpen(4)
val typs1T = lp1.nextState.map(_.typs).memoize


Out[12]:
lp1: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.2),
        Weighted(mul, 0.35),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...
typs1T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)

In [13]:
val typs1F = typs1T.runToFuture



In [14]:
val c1T = typs1T.map(typs => claims.map(c => c -> typs(c)))


Out[14]:
c1T: monix.eval.Task[Set[(Typ[Term], Double)]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd13$Helper$$Lambda$2921/144467445@1b15fd96,
  0
)

In [15]:
val c1F = c1T.runToFuture



In [22]:
val lp2 = lp0.sharpen(8)
val typs2T = lp2.nextState.map(_.typs).memoize


Out[22]:
lp2: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.2),
        Weighted(mul, 0.35),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...
typs2T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)

In [23]:
val c2T = typs2T.map(typs => claims.map(c => c -> typs(c)))


Out[23]:
c2T: monix.eval.Task[Set[(Typ[Term], Double)]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd22$Helper$$Lambda$2980/345857831@7b54ff09,
  0
)

In [24]:
val typs2F = typs2T.runToFuture



In [19]:
typs2F.value


Out[19]:
res18: Option[scala.util.Try[FiniteDistribution[Typ[Term]]]] = Some(
  Success(
    FiniteDistribution(
      Vector(
        Weighted(eqM(mul(m)(n))(mul(mul(m)(n))(m)), 9.217156749291046E-4),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(n)(mul(n)(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(m))(mul(mul(m)(n))(mul(n)(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(n)(mul(mul(m)(n))(m))),
          1.1628648290573092E-4
        ),
        Weighted(eqM(m)(mul(m)(mul(mul(m)(n))(n))), 2.5236640971030975E-4),
        Weighted(eqM(m)(mul(m)(mul(n)(n))), 2.5236640971030975E-4),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(m)(mul(m)(n))),
          4.0702901123907266E-4
        ),
        Weighted(
          eqM(mul(mul(m)(n))(n))(mul(n)(mul(mul(m)(n))(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(m)(m))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
          1.1628648290573092E-4
        ),
        Weighted(eqM(mul(n)(m))(mul(m)(mul(m)(n))), 4.0702901123907266E-4),
        Weighted(eqM(mul(m)(m))(mul(m)(mul(n)(m))), 1.1628648290573092E-4),
        Weighted(
          eqM(mul(n)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(m))(mul(mul(m)(n))(mul(n)(n))),
...

In [34]:
val c2F = c2T.runToFuture


Failure again

  • Even this misses out two cases.
  • Note that equality appears only once in a term, and if we look for typfamilies is the only choice, so we should downgrade this.
  • We will try again with mul having high priority, and equality very low.

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]:
ts3: TermState = TermState(
  FiniteDistribution(
    Vector(
      Weighted(eqM, 0.05),
      Weighted(mul, 0.5),
      Weighted(m, 0.15),
      Weighted(n, 0.15),
      Weighted(mul(m)(n), 0.15)
    )
  ),
  FiniteDistribution(Vector(Weighted(M, 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector()),
  Empty
)
lp3: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.05),
        Weighted(mul, 0.5),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...

In [30]:
val typs3T = lp3.nextState.map(_.typs).memoize


Out[30]:
typs3T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)

In [31]:
val typs3F = typs3T.runToFuture



In [39]:
typs3F.value


Out[39]:
res38: Option[scala.util.Try[FiniteDistribution[Typ[Term]]]] = Some(
  Success(
    FiniteDistribution(
      Vector(
        Weighted(eqM(mul(m)(n))(mul(mul(m)(n))(m)), 9.21715674929105E-4),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(n)(mul(n)(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(m))(mul(mul(m)(n))(mul(n)(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(n)(mul(mul(m)(n))(m))),
          1.1628648290573092E-4
        ),
        Weighted(eqM(m)(mul(m)(mul(mul(m)(n))(n))), 2.5236640971030975E-4),
        Weighted(eqM(m)(mul(m)(mul(n)(n))), 2.5236640971030975E-4),
        Weighted(
          eqM(mul(n)(mul(m)(n)))(mul(m)(mul(m)(n))),
          4.070290112390727E-4
        ),
        Weighted(
          eqM(mul(mul(m)(n))(n))(mul(n)(mul(mul(m)(n))(m))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(m)(m))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
          1.1628648290573092E-4
        ),
        Weighted(eqM(mul(n)(m))(mul(m)(mul(m)(n))), 4.070290112390727E-4),
        Weighted(eqM(mul(m)(m))(mul(m)(mul(n)(m))), 1.1628648290573092E-4),
        Weighted(
          eqM(mul(n)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(m)(n)))),
          1.1628648290573092E-4
        ),
        Weighted(
          eqM(mul(n)(m))(mul(mul(m)(n))(mul(n)(n))),
...

In [40]:
val c3T = typs3T.map(typs => claims.map(c => c -> typs(c)))


Out[40]:
c3T: monix.eval.Task[Set[(Typ[Term], Double)]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd39$Helper$$Lambda$3070/188202654@5ec53e3a,
  0
)

In [41]:
val c3F = c3T.runToFuture



In [35]:
lp3


Out[35]:
res34: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.05),
        Weighted(mul, 0.5),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...

In [36]:
val lp4 = lp3.sharpen(2)


Out[36]:
lp4: LocalProverStep = LocalProver(
  TermState(
    FiniteDistribution(
      Vector(
        Weighted(eqM, 0.05),
        Weighted(mul, 0.5),
        Weighted(m, 0.15),
        Weighted(n, 0.15),
        Weighted(mul(m)(n), 0.15)
      )
    ),
    FiniteDistribution(Vector(Weighted(M, 1.0))),
    Vector(),
    FiniteDistribution(Vector()),
    FiniteDistribution(Vector()),
    Empty
  ),
  TermGenParams(
    0.15,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.0,
    0.1,
    0.0,
    0.3,
    0.7,
    0.5,
    0.0,
    0.0,
    0.0,
    OrElse(
      OrElse(OrElse(OrElse(<function1>, <function1>), <function1>), <function1>),
...

In [37]:
val typs4T = lp4.nextState.map(_.typs).memoize


Out[37]:
typs4T: monix.eval.Task[FiniteDistribution[Typ[Term]]] = Async(
  <function2>,
  false,
  true,
  true
)

In [38]:
val typs4F = typs4T.runToFuture



In [45]:
val c4T = typs4T.map(typs => claims.map(c => c -> typs(c)))


Out[45]:
c4T: monix.eval.Task[Set[(Typ[Term], Double)]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd44$Helper$$Lambda$3105/112768889@459888bd,
  0
)

In [46]:
val c4F = c4T.runToFuture



In [47]:
c4F.value


Out[47]:
res46: Option[scala.util.Try[Set[(Typ[Term], Double)]]] = Some(
  Success(
    Set(
      (
        eqM(mul(mul(m)(n))(m))(mul(mul(m)(n))(mul(mul(m)(n))(n))),
        4.9883222572044254E-5
      ),
      (eqM(m)(mul(mul(m)(n))(n)), 4.729344879641796E-4),
      (eqM(n)(mul(mul(m)(n))(mul(mul(m)(n))(n))), 1.582960929619538E-4),
      (eqM(mul(mul(mul(m)(n))(m))(m))(mul(n)(m)), 0.0),
      (eqM(mul(m)(n))(mul(n)(m)), 5.18563243771282E-4),
      (eqM(mul(mul(m)(n))(m))(n), 9.09215288084965E-4),
      (eqM(mul(mul(mul(m)(n))(m))(m))(mul(m)(n)), 0.0),
      (eqM(mul(mul(m)(n))(n))(m), 9.09215288084965E-4)
    )
  )
)

Persistent failure

  • All the tweaks are not generating the given terms.
  • The only way I see to generate the two missed terms is to narrow/broaden - in one case drop $n$, in the other also include $n * m$.
  • We can combine all this generation using equations.

In [48]:
val lastF = typs4T.map(_.entropyVec.reverse).runToFuture



In [49]:
lastF.value


Out[49]:
res48: Option[scala.util.Try[Vector[Weighted[Typ[Term]]]]] = Some(
  Success(
    Vector(
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(n)(mul(mul(m)(n))(mul(m)(n))))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(n)(mul(n)(mul(m)(n))))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(n)(m)))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(m)(mul(n)(n)))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(n)(mul(m)(mul(m)(n))))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(m)))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(mul(m)(n))(mul(n)(n)))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(m)(mul(m)(m)))),
        15.94059049845905
      ),
      Weighted(
        eqM(mul(m)(n))(mul(mul(m)(n))(mul(m)(mul(mul(m)(n))(m)))),
        15.94059049845905
      ),
...

In [52]:
val flipped = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))


Out[52]:
flipped: Typ[Term] = eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m))

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]:
eqT: monix.eval.Task[Set[Equation]] = Async(<function2>, false, true, true)

In [55]:
val eqF = eqT.runToFuture



In [56]:
import Expression._, TermRandomVars._


Out[56]:
import Expression._, TermRandomVars._

In [57]:
import GeneratorVariables._
val lhs = FinalVal(Elem(flipped, Typs))


Out[57]:
import GeneratorVariables._

lhs: FinalVal[Typ[Term]] = FinalVal(
  Elem(eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m)), Typs)
)

In [58]:
val rhsT = eqT.map(eqs => eqs.find(_.lhs == lhs).map(_.rhs))


Out[58]:
rhsT: monix.eval.Task[Option[Expression]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd57$Helper$$Lambda$3408/195896456@c578994,
  0
)

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]:
lhs1: FinalVal[Term] = FinalVal(
  Elem(eqM(mul(m)(n))(mul(mul(mul(m)(n))(m))(m)), Terms)
)
rhs1T: monix.eval.Task[Option[Expression]] = Map(
  Async(<function2>, false, true, true),
  ammonite.$sess.cmd61$Helper$$Lambda$3433/908311445@6f71a048,
  0
)

In [64]:
val rF = rhs1T.runToFuture



In [65]:
rF.value


Out[65]:
res64: Option[scala.util.Try[Option[Expression]]] = Some(
  Success(
    Some(
      Sum(
        Product(
          Product(
            Coeff(
              BaseThenCondition(
                FiberProductMap(domOf, TermsWithTyp, Appln, TypFamilies, Terms),
                Typs,
                Restrict(TypOpt)
              )
            ),
            FinalVal(Elem(Wrap(eqM(mul(m)(n))), TypFamilies))
          ),
          FinalVal(
            Elem(mul(mul(mul(m)(n))(m))(m), AtCoord(TermsWithTyp, M :: HNil))
          )
        ),
        Product(
          Product(
            Coeff(FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms)),
            FinalVal(Elem(Wrap(eqM(mul(m)(n))), Funcs))
          ),
          FinalVal(
            Elem(mul(mul(mul(m)(n))(m))(m), AtCoord(TermsWithTyp, M :: HNil))
          )
        )
      )
    )
  )
)
  • The asymmetry seems to be because of targeting functions, terms with types etc.
  • This is possibly fixed by allowing reverse applications.
  • But finally, we clearly have to combine equations.

In [ ]: