Computer Aided Formal Reasoning Fall, 1995 Lecture notes 10 Judith Underwood

Inductive types

In ML, we can define new datatypes recursively. For example, we can define the type of binary trees labelled with integers with the declaration

datatype IntTree = Lf of int
                 | Node of int * IntTree * IntTree;

This declaration defines a new type, IntTree, and two constructors, Lf and Node, for creating objects in this new type. Functions from IntTree to other types are defined by pattern matching, i.e. cases depending on whether the argument is constructed with Lf or Node.

This method of constructing new types is very useful, not only for programming, but also for defining representations of mathematical objects. Some type theories have a built in operator for defining new types by induction. Lego doesn’t have this, but it does have the next best thing – a facility for automatically generating the appropriate rules, given a description of an inductive type something like the ML datatype declaration above.

Example: natural numbers

We’ll look at several examples to see how to build and use Lego’s inductive type constructors. The first example is that of the natural numbers. This is actually how natural numbers are defined in Lego in lib nat.

In ML style, the datatype of natural numbers would be

datatype nat = zero
             | suc of nat;

The Lego syntax for this is

Inductive [nat:Type] Constructors [zero:nat][suc:nat->nat];

[nat:Type] gives the name for the new type; the keyword Constructors introduces names for the constructors in the new type, and gives the types of any arguments to the constructors.

This is equivalent to the sequence of persistent (i.e. non-dischargable) declarations:

$[nat:Type];
$[zero:nat];
$[suc:nat->nat];

Lego now generates an elimination rule for nat and adds computation rules for the elimination operator. Elimination rules for all inductive types work in the same way. If S is an inductive type, we can define functions from S to any type S' by cases depending on how the argument was constructed, by using the value of any smaller terms and the value of the function on those smaller terms. Given a function from terms built from each constructor to an element of S', then we can put them together to obtain a function from all elements of S to S'. In order to ensure we can define a function from S to any S', we add S' (of type Type) as a parameter to the elimination rule. In fact, since S' may depend on the element of S to which the function is applied, we express this dependency by describing S' via a function T:S->Type.

In the case of natural numbers, then, Lego automatically constructs the declaration:

$[nat_elim:{T:nat->Type}(T zero)->({n:nat}(T n)->(T (suc n)))->{n:nat}(T n)];

Lego actually generates the name C_nat instead of T. Lego also generates computation rules for

nat_elim:
[[T:nat->Type][Zero_case:T zero][Suc_case:{n:nat}(T n)->(T (suc n))][n:nat]
    nat_elim T Zero_case Suc_case zero ==> Zero_case
 || nat_elim T Zero_case Suc_case (suc n) ==>
                                Suc_case n (nat_elim T Zero_case Suc_case n)];

This rule can be understood as follows. The first line is simply a collection of local declarations which describe the arguments to nat_elim. The next two lines actually describe the computation rules – the term on the left of the ==> computes to the term on the right. Lego imposes some restrictions on the form of these rules but for simple inductive types this isn’t a problem.

Example: lists

As a more complex example, the type of lists is defined as follows:

Inductive [list:Type]  Parameters [t:Type]
Constructors [nil:list][cons1:t->list->list];

This declaration includes the keyword Parameters, which describes the fact that new type of lists will take a type t: Type as a parameter. This is equivalent to simply giving a declaration [t:Type] before the inductive type declaration. Because of this, after the declaration of list, we will abstract away the parameter by saying

Discharge t;

This generates the list type constructor

list : Type->Type

and nil and cons1 constructors for lists; the implicitly typed version of cons is defined in the library

[cons [t|Type][x:t][l:list t]= cons1 t x l];

Example: An empty type

The empty type is particularly easy to define:

Inductive [empty:Type] Constructors;

The empty type acts as a Type-level absurd. The empty type has no constructors since it has no elements. It does have an elimination rule, which has type

empty_elim : {T:empty->Type}{x:empty}T x

If we assume e is in the empty type, we can produce a member of any type S by using empty elim:

empty_elim ([z:empty]S) e : S

There are no reduction rules for empty elim. Exercise: Prove there is only one empty type, in the sense that if empty2 is another type with an elimination rule

empty2_elim : {T:empty2->Type}{x:empty2}T x

then empty is inhabited iff empty2 is inhabited.

Double Inductions

Lego can generate definitions of mutually inductive objects as well. One example of such a definition is that of an alternating binary tree, where nodes are either and nodes or or nodes, which alternate along any branch. Trees of this kind are used to describe strategies in games.

   In Lego, we define both and_or_trees and or_and_trees – the root of an and_or_tree is

an and node, and the root of an or_and_tree is an or node. Leaves are labelled by natural numbers. The actual definition is:

Inductive [and_or_tree:Type][or_and_tree:Type]
Constructors [and_leaf:nat->and_or_tree][or_leaf:nat->or_and_tree]
[and_node:or_and_tree->or_and_tree->and_or_tree]
[or_node:and_or_tree->and_or_tree->or_and_tree];

Two elimination forms are created, one for and_or_trees and one for or_and_trees. Their types are fairly complex:

and_or_tree_elim:{P1:and_or_tree->TYPE}{P2:or_and_tree->TYPE}
     ({x6:nat}P1 (and_leaf x6))->
     ({x5:nat}P2 (or_leaf x5))->
     ({x3,x4:or_and_tree}(P2 x3)->(P2 x4)->P1 (and_node x3 x4))->
     ({x1,x2:and_or_tree}(P1 x1)->(P1 x2)->P2 (or_node x1 x2))->
         {z:and_or_tree}P1 z
or_and_tree_elim:{P1:and_or_tree->TYPE}{P2:or_and_tree->TYPE}
     ({x6:nat}P1 (and_leaf x6))->
     ({x5:nat}P2 (or_leaf x5))->
     ({x3,x4:or_and_tree}(P2 x3)->(P2 x4)->P1 (and_node x3 x4))->
     ({x1,x2:and_or_tree}(P1 x1)->(P1 x2)->P2 (or_node x1 x2))->
         {z:or_and_tree}P2 z

To see how to use these elimination forms, we shall define (by refinement) a function from and or trees to natural numbers. This function produces a single value from all the values at the leaves by taking the minimum of the two values at and nodes and the maximum at or nodes.

Goal and_or_tree->nat;
(* Use and_or_tree_elim, providing the type of the results
 for both and_or subtrees and or_and subtrees *)
Refine and_or_tree_elim ([_:and_or_tree]nat) ([_:or_and_tree]nat);
(* Base cases -- the value of a leaf is just its label *)
Refine [x:nat]x;
Refine [x:nat]x;
(* Inductive case 1 -- x3 and x4 are or_and_trees, x3_ih and x4_ih
are the values of those trees.  Since we are now at an and branch,
we take the minimum *)
intros;Refine min x3_ih x4_ih;
(* Inductive case 2 -- x1 and x2 are and_or_trees, x1_ih and x2_ih
are the values of those trees.  Since we are now at an or branch,
we take the maximum *)
intros;Refine max x1_ih x2_ih;
(* That's it! *)
Save min_max_calc;

(* Example tree *)
[tree=and_node (or_node (and_leaf one) (and_leaf two)) (or_node
(and_leaf one) (and_leaf three))];
(Normal min_max_calc tree);
(* Returns suc (suc zero) *)

Miscellaneous notes

Not all inductive definitions are safe. For example, an inductive definition of a type T where T occurs negatively (i.e. on the left of an odd number of function arrows) in the type of the argument to the constructor is not valid. So, for example, if we try to define such a type:

Lego> Inductive [bad:Type] Constructors [bad_cons:(bad->nat)->bad];
Error: Inductive: Not a valid schema

we get an error. This is because the definition is impredicative: an argument to bad cons is of type bad->nat, i.e. {_:bad}nat, so it involves quantifying over the type bad which we are currently defining.

There are a couple of options available when generating inductive data types in Lego.

ElimOver U

This specifies that the generated elimination rule should construct objects in U. In all the cases above this is specified in the libraries to be ElimOver Type.

NoReductions

This prevents Lego from generating computation rules. This is useful if the computation rules which Lego would ordinarily try to generate are not actually acceptable to it as computation rules.