Inductive types: explicit constructors and patterns

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:

  • Explicitly define the constructors and recursion/induction functions, such as Nat. This allows efficiency and simplification for recursion and induction functions, and should be done exactly when these are needed.
  • Explicitly define constructors and their associated constructor patterns.
  • Just specify constructor patterns, with constructors defined in terms of these.

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]:
import $ivy.$

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]:
import provingground._, induction._, coarse._
In [3]:
//import RecursiveDefinition._
import BaseConstructorTypes._
Out[3]:
import BaseConstructorTypes._

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.

Boolean type

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]:
res3: HoTT.Typ[U] = SmallBool
In [5]:
ff.typ
Out[5]:
res4: HoTT.Typ[U] = SmallBool

Recursion data

A recursive definition is specified by data associated to each constructor. This data is of type given by the recDataTyp method of the constructor pattern, depending on the target type.

In the case of Booleans, this is the target type.

In [6]:
W.recDataTyp(SmallBool, SmallBool)
Out[6]:
res5: HoTT.Typ[HoTT.Term] = SmallBool
In [7]:
W.recDataTyp(SmallBool, SmallNat)
Out[7]:
res6: HoTT.Typ[HoTT.Term] = SmallNat
In [8]:
W.recDataTyp(SmallBool, HoTT.Type)
Out[8]:
res7: HoTT.Typ[HoTT.Term] = Universe(0)
In [9]:
res7 == HoTT.Type
Out[9]:
res8: Boolean = true

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]:
import HoTT._

Induction levels

The definitions are based on a double induction, over the structure of the constructor and the number of constructors. The former takes place essentially in constructor patterns, while the latter is implemented in ConstructorSeq.

In [11]:
import ConstructorSeq.recFn
Out[11]:
import ConstructorSeq.recFn
In [12]:
recFn(BoolCons, SmallBool, SmallBool)
Out[12]:
res11: ConstructorSeq[Term, Term]#RecType = LambdaFixed(
  SymbObj(RecSym(ConstructorDefn(IdW(),true,SmallBool)), SmallBool),
  LambdaFixed(
    SymbObj(RecSym(ConstructorDefn(IdW(),false,SmallBool)), SmallBool),
    DataCons(
      SymbObj(RecSym(ConstructorDefn(IdW(),true,SmallBool)), SmallBool),
      provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@fe80bab,
      DataCons(
        SymbObj(RecSym(ConstructorDefn(IdW(),false,SmallBool)), SmallBool),
        provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@147bbc80,
        Empty(SmallBool, SmallBool),
        provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
      ),
      provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
    )
  )
)
In [13]:
val recBoolBool =
    recFn(BoolCons, SmallBool, SmallBool).asInstanceOf[Func[Term, Func[Term, Func[Term, Term]]]]
Out[13]:
recBoolBool: Func[Term, Func[Term, Func[Term, Term]]] = LambdaFixed(
  SymbObj(RecSym(ConstructorDefn(IdW(),true,SmallBool)), SmallBool),
  LambdaFixed(
    SymbObj(RecSym(ConstructorDefn(IdW(),false,SmallBool)), SmallBool),
    DataCons(
      SymbObj(RecSym(ConstructorDefn(IdW(),true,SmallBool)), SmallBool),
      provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@261fc8e7,
      DataCons(
        SymbObj(RecSym(ConstructorDefn(IdW(),false,SmallBool)), SmallBool),
        provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@58dddfdb,
        Empty(SmallBool, SmallBool),
        provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
      ),
      provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
    )
  )
)
In [14]:
val neg = recBoolBool(ff)(tt)
Out[14]:
neg: Func[Term, Term] = DataCons(
  SymbObj(Name("false"), SmallBool),
  provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@261fc8e7,
  DataCons(
    SymbObj(Name("true"), SmallBool),
    provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@58dddfdb,
    Empty(SmallBool, SmallBool),
    provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
  ),
  provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
)
In [15]:
neg(tt)
Out[15]:
res14: Term = SymbObj(Name("false"), SmallBool)
In [16]:
ff
Out[16]:
res15: Term = SymbObj(Name("false"), SmallBool)
In [17]:
neg("x" :: SmallBool)
Out[17]:
res16: Term = SymbObj(
  ApplnSym(
    DataCons(
      SymbObj(Name("false"), SmallBool),
      provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@261fc8e7,
      DataCons(
        SymbObj(Name("true"), SmallBool),
        provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@58dddfdb,
        Empty(SmallBool, SmallBool),
        provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
      ),
      provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
    ),
    SymbObj(Name("x"), SmallBool)
  ),
  SmallBool
)
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]:
x: Term = SymbObj(Name("x"), SmallBool)
res17_1: Term = SymbObj(
  ApplnSym(
    DataCons(
      SymbObj(Name("false"), SmallBool),
      provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@261fc8e7,
      DataCons(
        SymbObj(Name("true"), SmallBool),
        provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@58dddfdb,
        Empty(SmallBool, SmallBool),
        provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
      ),
      provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
    ),
    SymbObj(
      ApplnSym(
        DataCons(
          SymbObj(Name("false"), SmallBool),
          provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@261fc8e7,
          DataCons(
            SymbObj(Name("true"), SmallBool),
            provingground.induction.coarse.ConstructorSeq$Cons$$Lambda$2380/1495306900@58dddfdb,
            Empty(SmallBool, SmallBool),
            provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
          ),
          provingground.induction.RecursiveDefinition$DataCons$$$Lambda$2383/1441371154@2c8bf3af
        ),
        SymbObj(Name("x"), SmallBool)
      ),
      SmallBool
    )
  ),
...
res17_2: Boolean = false
In [ ]: