In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.1-SNAPSHOT`
Out[1]:
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:
The ring of natural numbers is an object NatRing. This has
In [2]:
import provingground._, induction._, scalahott._
import NatRing._
Out[2]:
In [3]:
val n = "n" :: NatTyp
val m = "m" :: NatTyp
val k = "k" :: NatTyp
Out[3]:
Spire implicits let us use the addition and multiplication operations.
In [4]:
import spire.math._
import spire.algebra._
import spire.implicits._
Out[4]:
In [5]:
n + m
Out[5]:
In [6]:
(n + m) + n
Out[6]:
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]:
In [8]:
(n + n) + m == (n + m) + n
Out[8]:
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]:
In [10]:
n * (m * k)
Out[10]:
In [11]:
(n * m) * k
Out[11]:
In [12]:
n * (m + k)
Out[12]:
In [13]:
n *(m + k) == (n * m) + (n * k)
Out[13]:
In [14]:
n + 1
Out[14]:
In [15]:
1 + n
Out[15]:
In [16]:
(1 + n) + 2
Out[16]:
In [17]:
n * n
Out[17]:
In [18]:
import HoTT._
val fn = lmbda(n)(n * n)
Out[18]:
In [19]:
fn(3)
Out[19]:
In [20]:
fn(k)
Out[20]:
In [21]:
val m = lmbda(n)(prod(n + 1))
val factorial = Rec(1: Nat, m)
Out[21]:
In [22]:
factorial(3)
Out[22]:
In [23]:
factorial(5)
Out[23]:
In [24]:
factorial(n)
Out[24]:
In [25]:
val g = lmbda(k)(factorial(k * k))
Out[25]:
In [26]:
g(3)
Out[26]:
In [27]:
factorial(9)
Out[27]:
In [28]:
factorial(n + 1)
Out[28]:
In [29]:
val fn = lmbda(n)(factorial(n + 1))
Out[29]:
In [30]:
fn(1)
Out[30]:
In [31]:
fn(4)
Out[31]:
In [32]:
(n + 2) * (n + 1)
Out[32]:
In [33]:
(3 * n) * n
Out[33]:
In [34]:
n * (n * n)
Out[34]:
In [35]:
(n * k) * k
Out[35]:
In [36]:
k * (n * k)
Out[36]:
In [37]:
(n * n) * n
Out[37]:
In [38]:
factorial(n + 2)
Out[38]:
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]:
In [40]:
func(k) == factorial(k) * (k + 2) * (k + 1)
Out[40]:
In [41]:
1 + 2
Out[41]:
In [42]:
findFactor(Literal(2), Literal(4))
Out[42]:
In [43]:
findDivisibilty(Literal(2), Literal(4))
Out[43]:
In [44]:
findDivisibilty(Literal(2), Literal(4)).map(_.typ)
Out[44]:
In [45]:
findFactor(n *2, n* 4)
Out[45]:
In [46]:
findFactor(n * 2, n * 2 * k)
Out[46]:
In [47]:
findFactor(n * k, n * n * k)
Out[47]:
In [48]:
findFactor(n * 2, n * 4 * k)
Out[48]:
In [49]:
findFactor(n * 2, n * 7 * k)
Out[49]:
In [50]:
findFactor(n * 2, n * 4 * k) == Some(k * 2)
Out[50]:
In [51]:
findDivisibilty(n * 2, n * 4 * k)
Out[51]:
In [52]:
divides(Literal(2))(Literal(3))
Out[52]:
In [53]:
findDivisibilty(2, 4)
Out[53]:
In [54]:
findDifference(n+ 4, n + 2)
Out[54]:
In [55]:
findDifference(4, 2)
Out[55]:
In [56]:
findDifferenceFlip(4, 2)
Out[56]:
In [57]:
findLEQ(2, 4)
Out[57]:
In [58]:
LEQ.unapply(leq(n)(k))
Out[58]:
In [59]:
LEQ.unapply(leq(Literal(2))(Literal(4)))
Out[59]:
In [60]:
val sg = leq(Literal(2))(Literal(4))
Out[60]:
In [61]:
findDifference(n + 2, 2)
Out[61]:
In [62]:
val x = NatTyp.Var
Out[62]:
In [63]:
val eqn = sg.fibers(x).asInstanceOf[IdentityTyp[Nat]]
Out[63]:
In [64]:
eqn.dom == NatTyp
Out[64]:
In [65]:
eqn.lhs
Out[65]:
In [66]:
findDifference(eqn.lhs, x)
Out[66]:
In [67]:
x + 2
Out[67]:
In [68]:
findDifference(x + 2, 2)
Out[68]:
In [69]:
eqn.lhs == x + 2
Out[69]:
In [70]:
findDifference(x + 2, x)
Out[70]:
In [71]:
DIV.unapply(divides(n)(k))
Out[71]:
In [72]:
divides(n)(k)
Out[72]:
In [73]:
findFactor(n * k, n)
Out[73]:
In [74]:
findFactor(k, n * k)
Out[74]:
In [75]:
DIV.unapply(divides(n)(Literal(7)))
Out[75]:
In [ ]: