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]:
import $ivy.$
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)
In [4]:
import spire.implicits._
Out[4]:
import spire.implicits._
In [5]:
import HoTT._
val recNatType = rec(Type)
Out[5]:
import HoTT._

recNatType: Func[Typ[Term], Func[Func[Nat, Func[Typ[Term], Typ[Term]]], Func[Nat, Typ[Term]]]] = LambdaFixed(
  SymbTyp($i, 0),
  LambdaFixed(
    SymbolicFunc($j, Nat.Typ, FuncTyp(Universe(0), Universe(0))),
    Rec(
      SymbTyp($i, 0),
      SymbolicFunc($j, Nat.Typ, FuncTyp(Universe(0), Universe(0)))
    )
  )
)
In [6]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [7]:
recNatType.typ
Out[7]:
res6: Typ[Func[Typ[Term], Func[Func[Nat, Func[Typ[Term], Typ[Term]]], Func[Nat, Typ[Term]]]]] = (𝒰  → ((Nat.Typ → (𝒰  → 𝒰 )) → (Nat.Typ → 𝒰 )))
In [8]:
val recNatNatType = rec(NatTyp ->: Type)
Out[8]:
recNatNatType: Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[Func[Nat, Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[RepTerm[spire.math.SafeLong], Typ[Term]]]], Func[Nat, Func[RepTerm[spire.math.SafeLong], Typ[Term]]]]] = ($ag : (Nat.Typ → 𝒰 )) ↦ ($ah : (Nat.Typ → ((Nat.Typ → 𝒰 ) → (Nat.Typ → 𝒰 )))) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }($ag)($ah)
In [9]:
recNatNatType.typ
Out[9]:
res8: Typ[Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[Func[Nat, Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[RepTerm[spire.math.SafeLong], Typ[Term]]]], Func[Nat, Func[RepTerm[spire.math.SafeLong], Typ[Term]]]]]] = ((Nat.Typ → 𝒰 ) → ((Nat.Typ → ((Nat.Typ → 𝒰 ) → (Nat.Typ → 𝒰 ))) → (Nat.Typ → (Nat.Typ → 𝒰 ))))
In [10]:
val A = Type.sym
recNatType(One).typ
Out[10]:
A: Typ[Term] = A
res9_1: Typ[Func[Func[Nat, Func[Typ[Term], Typ[Term]]], Func[Nat, Typ[Term]]]] = ((Nat.Typ → (𝒰  → 𝒰 )) → (Nat.Typ → 𝒰 ))
In [11]:
val step01 = n :-> (A :-> (Zero: Typ[Term]))
Out[11]:
step01: Func[RepTerm[spire.math.SafeLong], Func[Typ[Term], Typ[Term]]] = (_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero
In [12]:
step01.typ
Out[12]:
res11: Typ[Func[RepTerm[spire.math.SafeLong], Func[Typ[Term], Typ[Term]]]] = (Nat.Typ → (𝒰  → 𝒰 ))
In [13]:
val base0 = recNatType(One)(step01)
Out[13]:
base0: Func[Nat, Typ[Term]] = rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero)
In [14]:
recNatNatType(base0).typ
Out[14]:
res13: Typ[Func[Func[Nat, Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[RepTerm[spire.math.SafeLong], Typ[Term]]]], Func[Nat, Func[RepTerm[spire.math.SafeLong], Typ[Term]]]]] = ((Nat.Typ → ((Nat.Typ → 𝒰 ) → (Nat.Typ → 𝒰 ))) → (Nat.Typ → (Nat.Typ → 𝒰 )))
In [15]:
base0(0: Nat)
Out[15]:
res14: Typ[Term] = Unit
In [16]:
base0(1: Nat)
Out[16]:
res15: Typ[Term] = Zero
In [17]:
base0(n + 1)
Out[17]:
res16: Typ[Term] = Zero
In [18]:
val Q = (NatTyp ->: Type).sym
Out[18]:
Q: Func[RepTerm[spire.math.SafeLong], Typ[Term]] = Q
In [19]:
recNatType(Zero).typ
Out[19]:
res18: Typ[Func[Func[Nat, Func[Typ[Term], Typ[Term]]], Func[Nat, Typ[Term]]]] = ((Nat.Typ → (𝒰  → 𝒰 )) → (Nat.Typ → 𝒰 ))
In [20]:
(n :-> A :-> Q(n)).typ
Out[20]:
res19: Typ[Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Typ[Term]]] = ((Nat.Typ → 𝒰 ) → 𝒰 )
In [21]:
val step1arg = recNatType(Zero)(k :-> (A :-> Q(k)))
Out[21]:
step1arg: Func[Nat, Typ[Term]] = rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k))
In [22]:
step1arg.typ
Out[22]:
res21: Typ[Func[Nat, Typ[Term]]] = (Nat.Typ → 𝒰 )
In [23]:
val step0 = n :-> (Q :-> step1arg)
Out[23]:
step0: Func[RepTerm[spire.math.SafeLong], Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[Nat, Typ[Term]]]] = (_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k))
In [24]:
step0.typ
Out[24]:
res23: Typ[Func[RepTerm[spire.math.SafeLong], Func[Func[RepTerm[spire.math.SafeLong], Typ[Term]], Func[Nat, Typ[Term]]]]] = (Nat.Typ → ((Nat.Typ → 𝒰 ) → (Nat.Typ → 𝒰 )))
In [25]:
val AreEqual = recNatNatType(base0)(step0)
Out[25]:
AreEqual: Func[Nat, Func[RepTerm[spire.math.SafeLong], Typ[Term]]] = rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))
In [26]:
AreEqual.typ
Out[26]:
res25: Typ[Func[Nat, Func[RepTerm[spire.math.SafeLong], Typ[Term]]]] = (Nat.Typ → (Nat.Typ → 𝒰 ))
In [27]:
AreEqual(0: Nat)(0: Nat)
Out[27]:
res26: Typ[Term] = Unit
In [28]:
AreEqual(0: Nat)(1: Nat)
Out[28]:
res27: Typ[Term] = Zero
In [29]:
AreEqual(0)(n)
Out[29]:
res28: Typ[Term] = rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero)(n)
In [30]:
AreEqual(n + 1)(0)
Out[30]:
res29: Typ[Term] = Zero
In [31]:
AreEqual(n + 1)(n + 1)
Out[31]:
res30: Typ[Term] = rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(n)(n)
In [32]:
AreEqual(m + 1)(m + 1) == AreEqual(m)(m)
Out[32]:
res31: Boolean = true
In [33]:
val diagInd = induc(m :-> AreEqual(m)(m))
Out[33]:
diagInd: Func[Term, Func[FuncLike[Nat, Func[Term, Term]], FuncLike[Nat, Term]]] = ($nnx : Unit) ↦ ($xqn : ∏($nny : Nat.Typ){ (rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny) → rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny)) }) ↦ induc_{ Nat.Typ ; (m : Nat.Typ) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m) }($nnx)($xqn)
In [34]:
diagInd.typ
Out[34]:
res33: Typ[Func[Term, Func[FuncLike[Nat, Func[Term, Term]], FuncLike[Nat, Term]]]] = (Unit → (∏($nny : Nat.Typ){ (rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny) → rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny)) } → ∏(m : Nat.Typ){ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m) }))
In [36]:
AreEqual(2)(3)
Out[36]:
res35: Typ[Term] = Zero
In [37]:
diagInd(Star).dom
Out[37]:
res36: Typ[FuncLike[Nat, Func[Term, Term]]] = ∏($nny : Nat.Typ){ (rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny) → rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($nny)($nny)) }
In [38]:
diagInd(Star).dom == m ~>: (AreEqual(m)(m) ->: AreEqual(m)(m))
Out[38]:
res37: Boolean = true
In [39]:
val p = AreEqual(m)(m).sym
Out[39]:
p: Term = p
In [41]:
val diag = diagInd(Star)(m :~> (p :-> p))
Out[41]:
diag: FuncLike[Nat, Term] = induc_{ Nat.Typ ; (m : Nat.Typ) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m) }(Star)((m : Nat.Typ) ↦ (p : rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m)) ↦ p)
In [42]:
diag.typ == n ~>: (AreEqual(n)(n))
Out[42]:
res41: Boolean = true
In [69]:
val target = n :~> (m :~> (("_" :: (n =:= m)) :-> AreEqual(n)(m)))
Out[69]:
target: FuncLike[RepTerm[spire.math.SafeLong], FuncLike[RepTerm[spire.math.SafeLong], Func[Equality[RepTerm[spire.math.SafeLong]], Typ[Term]]]] = (n : Nat.Typ) ↦ (m : Nat.Typ) ↦ (_ : n = m) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(n)(m)
In [70]:
val indEq = IdentityTyp.induc(NatTyp, target)
Out[70]:
indEq: Func[FuncLike[RepTerm[spire.math.SafeLong], Term], FuncLike[RepTerm[spire.math.SafeLong], FuncLike[RepTerm[spire.math.SafeLong], Func[Equality[RepTerm[spire.math.SafeLong]], Term]]]] = ($yrlo : ∏($ypvu : Nat.Typ){ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($ypvu)($ypvu) }) ↦ ($yrlp : Nat.Typ) ↦ ($yrlq : Nat.Typ) ↦ ($yrlr : $yrlp = $yrlq) ↦ induc_{ ($zzyq : Nat.Typ) ↦ ($zzyr : Nat.Typ) ↦ $zzyq = $zzyr ; (n : Nat.Typ) ↦ (m : Nat.Typ) ↦ (_ : n = m) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(n)(m) }($yrlo)($yrlr)
In [71]:
indEq.typ
Out[71]:
res70: Typ[Func[FuncLike[RepTerm[spire.math.SafeLong], Term], FuncLike[RepTerm[spire.math.SafeLong], FuncLike[RepTerm[spire.math.SafeLong], Func[Equality[RepTerm[spire.math.SafeLong]], Term]]]]] = (∏($ypvu : Nat.Typ){ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($ypvu)($ypvu) } → ∏($yrlp : Nat.Typ){ ∏($yrlq : Nat.Typ){ ($yrlp = $yrlq → rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($yrlp)($yrlq)) } })
In [72]:
indEq.dom == m ~>: AreEqual(m)(m)
Out[72]:
res71: Boolean = true
In [73]:
indEq.dom == diag.typ
Out[73]:
res72: Boolean = true
In [74]:
indEq(diag).typ
Out[74]:
res73: Typ[FuncLike[RepTerm[spire.math.SafeLong], FuncLike[RepTerm[spire.math.SafeLong], Func[Equality[RepTerm[spire.math.SafeLong]], Term]]]] = ∏($yrlp : Nat.Typ){ ∏($yrlq : Nat.Typ){ ($yrlp = $yrlq → rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))($yrlp)($yrlq)) } }
In [75]:
indEq(diag)(m)(n)
Out[75]:
res74: Func[Equality[RepTerm[spire.math.SafeLong]], Term] = ($yrlr : m = n) ↦ induc_{ ($afaku : Nat.Typ) ↦ ($afakv : Nat.Typ) ↦ $afaku = $afakv ; (n : Nat.Typ) ↦ (m : Nat.Typ) ↦ (_ : n = m) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(n)(m) }(induc_{ Nat.Typ ; (m : Nat.Typ) ↦ rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m) }(Star)((m : Nat.Typ) ↦ (p : rec_{ Nat.Typ ; (Nat.Typ → 𝒰 ) }(rec_{ Nat.Typ ; 𝒰  }(Unit)((_ : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Zero))((_ : Nat.Typ) ↦ (Q : (Nat.Typ → 𝒰 )) ↦ rec_{ Nat.Typ ; 𝒰  }(Zero)((k : Nat.Typ) ↦ (_ : 𝒰 ) ↦ Q(k)))(m)(m)) ↦ p))($yrlr)
In [76]:
indEq(diag)(m)(n).typ == (m =:= n) ->: AreEqual(m)(n)
Out[76]:
res75: Boolean = true
In [77]:
indEq(diag).typ == m ~>: (n ~>: ((m =:= n) ->: AreEqual(m)(n)))
Out[77]:
res76: Boolean = true
In [79]:
indEq(diag)(0: Nat)(1: Nat).typ
Out[79]:
res78: Typ[Func[Equality[RepTerm[spire.math.SafeLong]], Term]] = (0 = 1 → Zero)
In [ ]: