In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.1-SNAPSHOT`
Out[1]:
import $ivy.$

Symbolic Algebra for natural numbers

To efficiently manipulate expressions in natural numbers, or more generally rings (and fields), proving-ground has special HoTT types wrapping scala types that are Rings, Rigs, Fields etc in the spire library. As a consequence:

  • Symbolic expressions that are equal become definitionally equal, i.e., equal as scala objects.
  • We define recursion which expands for (sums with) literals
  • Expressions involving literals and variables are simplified as much as possible.

The ring of natural numbers is an object NatRing. This has

  • a HoTT type NatTyp,
  • a scala type Nat
  • a scala representation
  • a (spire) ring structure on the underlying terms.
In [2]:
import provingground._, induction._, scalahott._
import NatRing._
Out[2]:
import provingground._, induction._, scalahott._

import NatRing._
In [3]:
val n = "n" :: NatTyp
val m = "m" :: NatTyp
val k = "k" :: NatTyp
Out[3]:
n: RepTerm[spire.math.SafeLong] = RepSymbObj(Name("n"), Nat.Typ)
m: RepTerm[spire.math.SafeLong] = RepSymbObj(Name("m"), Nat.Typ)
k: RepTerm[spire.math.SafeLong] = RepSymbObj(Name("k"), Nat.Typ)

Spire implicits let us use the addition and multiplication operations.

In [4]:
import spire.math._
import spire.algebra._
import spire.implicits._
Out[4]:
import spire.math._

import spire.algebra._

import spire.implicits._

Addition and multiplication

A sum gives a SigmaTerm, which only stores a set of terms being added.

In [5]:
n + m
Out[5]:
res4: LocalTerm = SigmaTerm(
  Set(RepSymbObj(Name("n"), Nat.Typ), RepSymbObj(Name("m"), Nat.Typ))
)
In [6]:
(n + m) + n
Out[6]:
res5: LocalTerm = SigmaTerm(
  Set(
    RepSymbObj(Name("m"), Nat.Typ),
    RepSymbObj(
      ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj(Name("n"), Nat.Typ)),
      Nat.Typ
    )
  )
)

Addition is commutative and associative, even when it involves repeated terms.

In [7]:
n + m == m + n
(n + m) + k == n + (m + k)
Out[7]:
res6_0: Boolean = true
res6_1: Boolean = true
In [8]:
(n + n) + m == (n + m) + n
Out[8]:
res7: Boolean = true

Similarly, multiplication is commutative and associative, and distributes over addition. Multiplication gives Pi-terms with parameter a map to exponents.

In [9]:
n * m == m * n
Out[9]:
res8: Boolean = true
In [10]:
n * (m * k)
Out[10]:
res9: LocalTerm = PiTerm(
  Map(
    RepSymbObj(Name("k"), Nat.Typ) -> 1,
    RepSymbObj(Name("n"), Nat.Typ) -> 1,
    RepSymbObj(Name("m"), Nat.Typ) -> 1
  )
)
In [11]:
(n * m) * k
Out[11]:
res10: LocalTerm = PiTerm(
  Map(
    RepSymbObj(Name("k"), Nat.Typ) -> 1,
    RepSymbObj(Name("n"), Nat.Typ) -> 1,
    RepSymbObj(Name("m"), Nat.Typ) -> 1
  )
)
In [12]:
n * (m + k)
Out[12]:
res11: LocalTerm = SigmaTerm(
  Set(
    PiTerm(
      Map(
        RepSymbObj(Name("n"), Nat.Typ) -> 1,
        RepSymbObj(Name("m"), Nat.Typ) -> 1
      )
    ),
    PiTerm(
      Map(
        RepSymbObj(Name("k"), Nat.Typ) -> 1,
        RepSymbObj(Name("n"), Nat.Typ) -> 1
      )
    )
  )
)
In [13]:
n *(m + k) == (n * m) + (n * k)
Out[13]:
res12: Boolean = true
In [14]:
n + 1
Out[14]:
res13: LocalTerm = RepSymbObj(
  ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(Name("n"), Nat.Typ)),
  Nat.Typ
)
In [15]:
1 + n
Out[15]:
res14: RepTerm[SafeLong] = RepSymbObj(
  ApplnSym(AddLiteral(SafeLongLong(1L)), RepSymbObj(Name("n"), Nat.Typ)),
  Nat.Typ
)
In [16]:
(1 + n) + 2
Out[16]:
res15: LocalTerm = RepSymbObj(
  ApplnSym(AddLiteral(SafeLongLong(3L)), RepSymbObj(Name("n"), Nat.Typ)),
  Nat.Typ
)
In [17]:
n * n
Out[17]:
res16: LocalTerm = PiTerm(Map(RepSymbObj(Name("n"), Nat.Typ) -> 2))

Symbolic definitions

We can use the expressions from these functions in lambdas. For this we need correct substitution.

In [18]:
import HoTT._
val fn = lmbda(n)(n * n)
Out[18]:
import HoTT._

fn: Func[RepTerm[SafeLong], LocalTerm] = LambdaFixed(
  RepSymbObj(n, Nat.Typ),
  PiTerm(Map(RepSymbObj(n, Nat.Typ) -> 2))
)
In [19]:
fn(3)
Out[19]:
res18: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(9L)), Nat.Typ)
In [20]:
fn(k)
Out[20]:
res19: LocalTerm = PiTerm(Map(RepSymbObj(Name("k"), Nat.Typ) -> 2))

Recursive definitions

We can define a function f recursively on natural numbers, given the value f(0) and given f(n+1) as a (curryed) function of (n+1) and f(n). This expands for literals.

In [21]:
val m = lmbda(n)(prod(n + 1))
val factorial = Rec(1: Nat, m)
Out[21]:
m: Func[RepTerm[SafeLong], Func[LocalTerm, LocalTerm]] = LambdaFixed(
  RepSymbObj(n, Nat.Typ),
  LambdaFixed(
    RepSymbObj($n, Nat.Typ),
    SigmaTerm(
      Set(
        RepSymbObj($n, Nat.Typ),
        PiTerm(Map(RepSymbObj($n, Nat.Typ) -> 1, RepSymbObj(n, Nat.Typ) -> 1))
      )
    )
  )
)
factorial: Rec[LocalTerm] = Rec(
  RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
  LambdaFixed(
    RepSymbObj(n, Nat.Typ),
    LambdaFixed(
      RepSymbObj($n, Nat.Typ),
      SigmaTerm(
        Set(
          RepSymbObj($n, Nat.Typ),
          PiTerm(Map(RepSymbObj($n, Nat.Typ) -> 1, RepSymbObj(n, Nat.Typ) -> 1))
        )
      )
    )
  )
)
In [22]:
factorial(3)
Out[22]:
res21: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(6L)), Nat.Typ)
In [23]:
factorial(5)
Out[23]:
res22: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(120L)), Nat.Typ)
In [24]:
factorial(n)
Out[24]:
res23: LocalTerm = RepSymbObj(
  ApplnSym(
    Rec(
      RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
      LambdaFixed(
        RepSymbObj(n, Nat.Typ),
        LambdaFixed(
          RepSymbObj($n, Nat.Typ),
          SigmaTerm(
            Set(
              RepSymbObj($n, Nat.Typ),
              PiTerm(
                Map(RepSymbObj($n, Nat.Typ) -> 1, RepSymbObj(n, Nat.Typ) -> 1)
              )
            )
          )
        )
      )
    ),
    RepSymbObj(Name("n"), Nat.Typ)
  ),
  Nat.Typ
)
In [25]:
val g = lmbda(k)(factorial(k * k))
Out[25]:
g: Func[RepTerm[SafeLong], LocalTerm] = LambdaFixed(
  RepSymbObj(k, Nat.Typ),
  RepSymbObj(
    ApplnSym(
      Rec(
        RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
        LambdaFixed(
          RepSymbObj(n, Nat.Typ),
          LambdaFixed(
            RepSymbObj($n, Nat.Typ),
            SigmaTerm(
              Set(
                RepSymbObj($n, Nat.Typ),
                PiTerm(
                  Map(RepSymbObj($n, Nat.Typ) -> 1, RepSymbObj(n, Nat.Typ) -> 1)
                )
              )
            )
          )
        )
      ),
      PiTerm(Map(RepSymbObj(k, Nat.Typ) -> 2))
    ),
    Nat.Typ
  )
)
In [26]:
g(3)
Out[26]:
res25: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(362880L)), Nat.Typ)
In [27]:
factorial(9)
Out[27]:
res26: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(362880L)), Nat.Typ)

Simplifying recursive functions

If we apply a recursive function to a sum n+k with k a literal (say k = 2), then the result simplifies as much as possible by expanding tail recursively in the literal.

In [28]:
factorial(n + 1)
Out[28]:
res27: LocalTerm = SigmaTerm(
  Set(
    RepSymbObj(
      ApplnSym(
        Rec(
          RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
          LambdaFixed(
            RepSymbObj(n, Nat.Typ),
            LambdaFixed(
              RepSymbObj($n, Nat.Typ),
              SigmaTerm(
                Set(
                  RepSymbObj($n, Nat.Typ),
                  PiTerm(
                    Map(
                      RepSymbObj($n, Nat.Typ) -> 1,
                      RepSymbObj(n, Nat.Typ) -> 1
                    )
                  )
                )
              )
            )
          )
        ),
        RepSymbObj(Name("n"), Nat.Typ)
      ),
      Nat.Typ
    ),
    PiTerm(
      Map(
        RepSymbObj(Name("n"), Nat.Typ) -> 1,
        RepSymbObj(
          ApplnSym(
            Rec(
              RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
              LambdaFixed(
                RepSymbObj(n, Nat.Typ),
                LambdaFixed(
                  RepSymbObj($n, Nat.Typ),
...
In [29]:
val fn = lmbda(n)(factorial(n + 1))
Out[29]:
fn: Func[RepTerm[SafeLong], LocalTerm] = LambdaFixed(
  RepSymbObj(n, Nat.Typ),
  SigmaTerm(
    Set(
      RepSymbObj(
        ApplnSym(
          Rec(
            RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
            LambdaFixed(
              RepSymbObj(n, Nat.Typ),
              LambdaFixed(
                RepSymbObj($n, Nat.Typ),
                SigmaTerm(
                  Set(
                    RepSymbObj($n, Nat.Typ),
                    PiTerm(
                      Map(
                        RepSymbObj($n, Nat.Typ) -> 1,
                        RepSymbObj(n, Nat.Typ) -> 1
                      )
                    )
                  )
                )
              )
            )
          ),
          RepSymbObj(n, Nat.Typ)
        ),
        Nat.Typ
      ),
      PiTerm(
        Map(
          RepSymbObj(n, Nat.Typ) -> 1,
          RepSymbObj(
            ApplnSym(
              Rec(
                RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
                LambdaFixed(
                  RepSymbObj(n, Nat.Typ),
...
In [30]:
fn(1)
Out[30]:
res29: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ)
In [31]:
fn(4)
Out[31]:
res30: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(120L)), Nat.Typ)
In [32]:
(n + 2) * (n + 1)
Out[32]:
res31: LocalTerm = RepSymbObj(
  ApplnSym(
    AddLiteral(SafeLongLong(2L)),
    SigmaTerm(
      Set(
        PiTerm(Map(RepSymbObj(Name("n"), Nat.Typ) -> 2)),
        RepSymbObj(
          ApplnSym(
            multLiteral(SafeLongLong(3L)),
            RepSymbObj(Name("n"), Nat.Typ)
          ),
          Nat.Typ
        )
      )
    )
  ),
  Nat.Typ
)
In [33]:
(3 * n) * n
Out[33]:
res32: LocalTerm = RepSymbObj(
  ApplnSym(
    multLiteral(SafeLongLong(3L)),
    PiTerm(Map(RepSymbObj(Name("n"), Nat.Typ) -> 2))
  ),
  Nat.Typ
)
In [34]:
n * (n * n)
Out[34]:
res33: LocalTerm = PiTerm(Map(RepSymbObj(Name("n"), Nat.Typ) -> 3))
In [35]:
(n * k) * k
Out[35]:
res34: LocalTerm = PiTerm(
  Map(RepSymbObj(Name("k"), Nat.Typ) -> 2, RepSymbObj(Name("n"), Nat.Typ) -> 1)
)
In [36]:
k * (n * k)
Out[36]:
res35: LocalTerm = PiTerm(
  Map(RepSymbObj(Name("k"), Nat.Typ) -> 2, RepSymbObj(Name("n"), Nat.Typ) -> 1)
)
In [37]:
(n * n) * n
Out[37]:
res36: LocalTerm = PiTerm(Map(RepSymbObj(Name("n"), Nat.Typ) -> 3))
In [38]:
factorial(n + 2)
Out[38]:
res37: LocalTerm = SigmaTerm(
  Set(
    RepSymbObj(
      ApplnSym(
        multLiteral(SafeLongLong(2L)),
        RepSymbObj(
          ApplnSym(
            Rec(
              RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
              LambdaFixed(
                RepSymbObj(n, Nat.Typ),
                LambdaFixed(
                  RepSymbObj($n, Nat.Typ),
                  SigmaTerm(
                    Set(
                      RepSymbObj($n, Nat.Typ),
                      PiTerm(
                        Map(
                          RepSymbObj($n, Nat.Typ) -> 1,
                          RepSymbObj(n, Nat.Typ) -> 1
                        )
                      )
                    )
                  )
                )
              )
            ),
            RepSymbObj(Name("n"), Nat.Typ)
          ),
          Nat.Typ
        )
      ),
      Nat.Typ
    ),
    PiTerm(
      Map(
        RepSymbObj(Name("n"), Nat.Typ) -> 2,
        RepSymbObj(
          ApplnSym(
...

Recursive expansion: We see an example of expansion as much as possible.

In [39]:
val func = lmbda(n)(factorial(n+ 2))
func(3)
Out[39]:
func: Func[RepTerm[SafeLong], LocalTerm] = LambdaFixed(
  RepSymbObj(n, Nat.Typ),
  SigmaTerm(
    Set(
      PiTerm(
        Map(
          RepSymbObj(
            ApplnSym(
              Rec(
                RepSymbObj(ScalaSymbol(SafeLongLong(1L)), Nat.Typ),
                LambdaFixed(
                  RepSymbObj(n, Nat.Typ),
                  LambdaFixed(
                    RepSymbObj($n, Nat.Typ),
                    SigmaTerm(
                      Set(
                        RepSymbObj($n, Nat.Typ),
                        PiTerm(
                          Map(
                            RepSymbObj($n, Nat.Typ) -> 1,
                            RepSymbObj(n, Nat.Typ) -> 1
                          )
                        )
                      )
                    )
                  )
                )
              ),
              RepSymbObj(n, Nat.Typ)
            ),
            Nat.Typ
          ) -> 1,
          RepSymbObj(n, Nat.Typ) -> 2
        )
      ),
      RepSymbObj(
        ApplnSym(
          multLiteral(SafeLongLong(3L)),
          PiTerm(
...
res38_1: LocalTerm = RepSymbObj(ScalaSymbol(SafeLongLong(120L)), Nat.Typ)
In [40]:
func(k) == factorial(k) * (k + 2) * (k + 1)
Out[40]:
res39: Boolean = true
In [41]:
1 + 2
Out[41]:
res40: Int = 3
In [42]:
findFactor(Literal(2), Literal(4))
Out[42]:
res41: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [43]:
findDivisibilty(Literal(2), Literal(4))
Out[43]:
res42: Option[AbsPair[Nat, Equality[Nat]]] = Some(
  DepPair(
    RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ),
    Refl(Nat.Typ, RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)),
    LambdaFixed(
      RepSymbObj($c, Nat.Typ),
      IdentityTyp(
        Nat.Typ,
        RepSymbObj(
          ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj($c, Nat.Typ)),
          Nat.Typ
        ),
        RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
      )
    )
  )
)
In [44]:
findDivisibilty(Literal(2), Literal(4)).map(_.typ)
Out[44]:
res43: Option[Typ[U] forSome { type U >: x$1 <: Term with Subs[U]; val x$1: AbsPair[Nat, Equality[Nat]] }] = Some(
  SigmaTyp(
    LambdaFixed(
      RepSymbObj($c, Nat.Typ),
      IdentityTyp(
        Nat.Typ,
        RepSymbObj(
          ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj($c, Nat.Typ)),
          Nat.Typ
        ),
        RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
      )
    )
  )
)
In [45]:
findFactor(n *2, n* 4)
Out[45]:
res44: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [46]:
findFactor(n * 2, n * 2 * k)
Out[46]:
res45: Option[Nat] = Some(RepSymbObj(Name("k"), Nat.Typ))
In [47]:
findFactor(n * k, n * n * k)
Out[47]:
res46: Option[Nat] = Some(RepSymbObj(Name("n"), Nat.Typ))
In [48]:
findFactor(n * 2, n * 4 * k)
Out[48]:
res47: Option[Nat] = Some(
  RepSymbObj(
    ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj(Name("k"), Nat.Typ)),
    Nat.Typ
  )
)
In [49]:
findFactor(n * 2, n * 7 * k)
Out[49]:
res48: Option[Nat] = None
In [50]:
findFactor(n * 2, n * 4 * k) == Some(k * 2)
Out[50]:
res49: Boolean = true
In [51]:
findDivisibilty(n * 2, n * 4 * k)
Out[51]:
res50: Option[AbsPair[Nat, Equality[Nat]]] = Some(
  DepPair(
    RepSymbObj(
      ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj(Name("k"), Nat.Typ)),
      Nat.Typ
    ),
    Refl(
      Nat.Typ,
      RepSymbObj(
        ApplnSym(
          multLiteral(SafeLongLong(4L)),
          PiTerm(
            Map(
              RepSymbObj(Name("k"), Nat.Typ) -> 1,
              RepSymbObj(Name("n"), Nat.Typ) -> 1
            )
          )
        ),
        Nat.Typ
      )
    ),
    LambdaFixed(
      RepSymbObj($c, Nat.Typ),
      IdentityTyp(
        Nat.Typ,
        RepSymbObj(
          ApplnSym(
            multLiteral(SafeLongLong(2L)),
            PiTerm(
              Map(
                RepSymbObj(Name("n"), Nat.Typ) -> 1,
                RepSymbObj($c, Nat.Typ) -> 1
              )
            )
          ),
          Nat.Typ
        ),
        RepSymbObj(
          ApplnSym(
...
In [52]:
divides(Literal(2))(Literal(3))
Out[52]:
res51: SigmaTyp[LocalTerm, Equality[LocalTerm]] = SigmaTyp(
  LambdaFixed(
    RepSymbObj($c, Nat.Typ),
    IdentityTyp(
      Nat.Typ,
      RepSymbObj(
        ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj($c, Nat.Typ)),
        Nat.Typ
      ),
      RepSymbObj(ScalaSymbol(SafeLongLong(3L)), Nat.Typ)
    )
  )
)
In [53]:
findDivisibilty(2, 4)
Out[53]:
res52: Option[AbsPair[Nat, Equality[Nat]]] = Some(
  DepPair(
    RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ),
    Refl(Nat.Typ, RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)),
    LambdaFixed(
      RepSymbObj($c, Nat.Typ),
      IdentityTyp(
        Nat.Typ,
        RepSymbObj(
          ApplnSym(multLiteral(SafeLongLong(2L)), RepSymbObj($c, Nat.Typ)),
          Nat.Typ
        ),
        RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
      )
    )
  )
)
In [54]:
findDifference(n+ 4, n + 2)
Out[54]:
res53: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [55]:
findDifference(4, 2)
Out[55]:
res54: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [56]:
findDifferenceFlip(4, 2)
Out[56]:
res55: Option[Nat] = None
In [57]:
findLEQ(2, 4)
Out[57]:
res56: Option[DepPair[Nat, Equality[Nat]]] = Some(
  DepPair(
    RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ),
    Refl(Nat.Typ, RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)),
    LambdaFixed(
      RepSymbObj($g, Nat.Typ),
      IdentityTyp(
        Nat.Typ,
        RepSymbObj(
          ApplnSym(AddLiteral(SafeLongLong(2L)), RepSymbObj($g, Nat.Typ)),
          Nat.Typ
        ),
        RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
      )
    )
  )
)
In [58]:
LEQ.unapply(leq(n)(k))
Out[58]:
res57: Option[(Nat, Nat)] = Some(
  (RepSymbObj(Name("n"), Nat.Typ), RepSymbObj(Name("k"), Nat.Typ))
)
In [59]:
LEQ.unapply(leq(Literal(2))(Literal(4)))
Out[59]:
res58: Option[(Nat, Nat)] = Some(
  (
    RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ),
    RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
  )
)
In [60]:
val sg = leq(Literal(2))(Literal(4))
Out[60]:
sg: SigmaTyp[Nat, Equality[Nat]] = SigmaTyp(
  LambdaFixed(
    RepSymbObj($g, Nat.Typ),
    IdentityTyp(
      Nat.Typ,
      RepSymbObj(
        ApplnSym(AddLiteral(SafeLongLong(2L)), RepSymbObj($g, Nat.Typ)),
        Nat.Typ
      ),
      RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
    )
  )
)
In [61]:
findDifference(n + 2, 2)
Out[61]:
res60: Option[Nat] = Some(RepSymbObj(Name("n"), Nat.Typ))
In [62]:
val x = NatTyp.Var
Out[62]:
x: RepTerm[SafeLong] = RepSymbObj(Name("$zr"), Nat.Typ)
In [63]:
val eqn = sg.fibers(x).asInstanceOf[IdentityTyp[Nat]]
Out[63]:
eqn: IdentityTyp[Nat] = IdentityTyp(
  Nat.Typ,
  RepSymbObj(
    ApplnSym(AddLiteral(SafeLongLong(2L)), RepSymbObj(Name("$zr"), Nat.Typ)),
    Nat.Typ
  ),
  RepSymbObj(ScalaSymbol(SafeLongLong(4L)), Nat.Typ)
)
In [64]:
eqn.dom == NatTyp
Out[64]:
res63: Boolean = true
In [65]:
eqn.lhs
Out[65]:
res64: Nat = RepSymbObj(
  ApplnSym(AddLiteral(SafeLongLong(2L)), RepSymbObj(Name("$zr"), Nat.Typ)),
  Nat.Typ
)
In [66]:
findDifference(eqn.lhs, x)
Out[66]:
res65: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [67]:
x + 2
Out[67]:
res66: LocalTerm = RepSymbObj(
  ApplnSym(AddLiteral(SafeLongLong(2L)), RepSymbObj(Name("$zr"), Nat.Typ)),
  Nat.Typ
)
In [68]:
findDifference(x + 2, 2)
Out[68]:
res67: Option[Nat] = Some(RepSymbObj(Name("$zr"), Nat.Typ))
In [69]:
eqn.lhs == x + 2
Out[69]:
res68: Boolean = true
In [70]:
findDifference(x + 2, x)
Out[70]:
res69: Option[Nat] = Some(RepSymbObj(ScalaSymbol(SafeLongLong(2L)), Nat.Typ))
In [71]:
DIV.unapply(divides(n)(k))
Out[71]:
res70: Option[(Nat, Nat)] = Some(
  (RepSymbObj(Name("n"), Nat.Typ), RepSymbObj(Name("k"), Nat.Typ))
)
In [72]:
divides(n)(k)
Out[72]:
res71: SigmaTyp[LocalTerm, Equality[LocalTerm]] = SigmaTyp(
  LambdaFixed(
    RepSymbObj($c, Nat.Typ),
    IdentityTyp(
      Nat.Typ,
      PiTerm(
        Map(RepSymbObj(Name("n"), Nat.Typ) -> 1, RepSymbObj($c, Nat.Typ) -> 1)
      ),
      RepSymbObj(Name("k"), Nat.Typ)
    )
  )
)
In [73]:
findFactor(n * k, n)
Out[73]:
res72: Option[Nat] = None
In [74]:
findFactor(k, n * k)
Out[74]:
res73: Option[Nat] = Some(RepSymbObj(Name("n"), Nat.Typ))
In [75]:
DIV.unapply(divides(n)(Literal(7)))
Out[75]:
res74: Option[(Nat, Nat)] = Some(
  (
    RepSymbObj(Name("n"), Nat.Typ),
    RepSymbObj(ScalaSymbol(SafeLongLong(7L)), Nat.Typ)
  )
)
In [ ]: