Inductive types and the associated recursion and induction functions are the subtlest part of HoTT. There are three levels at which we can implement these:
Nat. This allows efficiency and simplification for recursion and induction functions, and should be done exactly when these are needed.This note concerns the middle case, with the subtleties of defining induction and recursion.
In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
As the implementation is self-contained and in the core, we just load the jar of the core.
In [2]:
import provingground._, induction._, coarse._
Out[2]:
In [3]:
//import RecursiveDefinition._
import BaseConstructorTypes._
Out[3]:
Booleans and natural numbers are defined in BaseConstructorTypes, for illustration and testing. These are called SmallBool and SmallNat to avoid clashes with the ScalaRep based implementations.
At present a Constructor is a constructor function with an associated pattern, with the cons attribute the function itself. Should eventually rename these.
The Boolean type only uses the constant/identity constructor pattern. This is used to give two Constructors and their associated functions.
val ttC = W.constructor(SmallBool, "true")
val ffC = W.constructor(SmallBool, "false")
val tt : Term = ttC.cons
val ff : Term = ffC.cons
val BoolCons = List(ttC, ffC)
The constructors have type booleans
In [4]:
tt.typ
Out[4]:
In [5]:
ff.typ
Out[5]:
In [6]:
W.recDataTyp(SmallBool, SmallBool)
Out[6]:
In [7]:
W.recDataTyp(SmallBool, SmallNat)
Out[7]:
In [8]:
W.recDataTyp(SmallBool, HoTT.Type)
Out[8]:
In [9]:
res7 == HoTT.Type
Out[9]:
The action of a recursion functions is defined recursively, in terms of cases. This is implemented as a diagonal construction, with a method, in the trait RecFunction definining the recursion function in terms of a function of its own type, and applying this to itself.
In [10]:
import HoTT._
Out[10]:
In [11]:
import ConstructorSeq.recFn
Out[11]:
In [12]:
recFn(BoolCons, SmallBool, SmallBool)
Out[12]:
In [13]:
val recBoolBool =
recFn(BoolCons, SmallBool, SmallBool).asInstanceOf[Func[Term, Func[Term, Func[Term, Term]]]]
Out[13]:
In [14]:
val neg = recBoolBool(ff)(tt)
Out[14]:
In [15]:
neg(tt)
Out[15]:
In [16]:
ff
Out[16]:
In [17]:
neg("x" :: SmallBool)
Out[17]:
In [18]:
val x = "x" :: SmallBool
neg(neg(x))
neg(neg(x)) == x // not equal by definition, needs a theorem proved by induction
Out[18]:
In [ ]: