We attempt to decide identity for natural numbers.
In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.1-SNAPSHOT`
Out[1]:
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]:
In [4]:
import spire.implicits._
Out[4]:
In [5]:
import HoTT._
val recNatType = rec(Type)
Out[5]:
In [6]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [7]:
recNatType.typ
Out[7]:
In [8]:
val recNatNatType = rec(NatTyp ->: Type)
Out[8]:
In [9]:
recNatNatType.typ
Out[9]:
In [10]:
val A = Type.sym
recNatType(One).typ
Out[10]:
In [11]:
val step01 = n :-> (A :-> (Zero: Typ[Term]))
Out[11]:
In [12]:
step01.typ
Out[12]:
In [13]:
val base0 = recNatType(One)(step01)
Out[13]:
In [14]:
recNatNatType(base0).typ
Out[14]:
In [15]:
base0(0: Nat)
Out[15]:
In [16]:
base0(1: Nat)
Out[16]:
In [17]:
base0(n + 1)
Out[17]:
In [18]:
val Q = (NatTyp ->: Type).sym
Out[18]:
In [19]:
recNatType(Zero).typ
Out[19]:
In [20]:
(n :-> A :-> Q(n)).typ
Out[20]:
In [21]:
val step1arg = recNatType(Zero)(k :-> (A :-> Q(k)))
Out[21]:
In [22]:
step1arg.typ
Out[22]:
In [23]:
val step0 = n :-> (Q :-> step1arg)
Out[23]:
In [24]:
step0.typ
Out[24]:
In [25]:
val AreEqual = recNatNatType(base0)(step0)
Out[25]:
In [26]:
AreEqual.typ
Out[26]:
In [27]:
AreEqual(0: Nat)(0: Nat)
Out[27]:
In [28]:
AreEqual(0: Nat)(1: Nat)
Out[28]:
In [29]:
AreEqual(0)(n)
Out[29]:
In [30]:
AreEqual(n + 1)(0)
Out[30]:
In [31]:
AreEqual(n + 1)(n + 1)
Out[31]:
In [32]:
AreEqual(m + 1)(m + 1) == AreEqual(m)(m)
Out[32]:
In [33]:
val diagInd = induc(m :-> AreEqual(m)(m))
Out[33]:
In [34]:
diagInd.typ
Out[34]:
In [36]:
AreEqual(2)(3)
Out[36]:
In [37]:
diagInd(Star).dom
Out[37]:
In [38]:
diagInd(Star).dom == m ~>: (AreEqual(m)(m) ->: AreEqual(m)(m))
Out[38]:
In [39]:
val p = AreEqual(m)(m).sym
Out[39]:
In [41]:
val diag = diagInd(Star)(m :~> (p :-> p))
Out[41]:
In [42]:
diag.typ == n ~>: (AreEqual(n)(n))
Out[42]:
In [69]:
val target = n :~> (m :~> (("_" :: (n =:= m)) :-> AreEqual(n)(m)))
Out[69]:
In [70]:
val indEq = IdentityTyp.induc(NatTyp, target)
Out[70]:
In [71]:
indEq.typ
Out[71]:
In [72]:
indEq.dom == m ~>: AreEqual(m)(m)
Out[72]:
In [73]:
indEq.dom == diag.typ
Out[73]:
In [74]:
indEq(diag).typ
Out[74]:
In [75]:
indEq(diag)(m)(n)
Out[75]:
In [76]:
indEq(diag)(m)(n).typ == (m =:= n) ->: AreEqual(m)(n)
Out[76]:
In [77]:
indEq(diag).typ == m ~>: (n ~>: ((m =:= n) ->: AreEqual(m)(n)))
Out[77]:
In [79]:
indEq(diag)(0: Nat)(1: Nat).typ
Out[79]:
In [ ]: