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

Inductively defined families of types

Today we will look at two families of inductively defined types. The purpose of this is twofold; first, to gain some more experience with inductive types in Lego, and second, because they are useful in their own right.

We look first at vectors. Vectors over a type A are essentially fixed-length lists of elements of A. We then consider finite types, which we think of as finite sets of natural numbers. The common factor is that not only do both types depend on a natural number n (the length of the vector or the number of elements of the set), but proving properties of these types generally requires induction not only over elements of a particular type, but also over the types in the family.

Vectors

The inductive definition of vectors is:

Inductive [vect:{n:nat}Type] ElimOver Type
Parameters [A:Type]
Constructors
[vnil:vect zero]
[vcons:{a:A}{n|nat}{v:vect n}(vect (suc n))];

A is the type of elements of the vectors.

The things to notice are that vnil is the vector of length zero, and that vcons takes an element of A and an element of vect n (an n-length vector) and returns an element of vect (suc n). Thus, in order to construct an element of vect (suc n), we use an element of the different type vect n.

The automatically generated elimination rule is:

vect_elim :
  {A:Type}{P:{n|nat}(vect A n)->Type}
  (P (vnil A))->
  ({a:A}{n|nat}{v:vect A n}(P v)->P (vcons A a v))->
     {n|nat}{z:vect A n}P z

Note that this proves P z for all n and all z in vect A n – not just for a particular n. Also note that the base case is P (vnil A). Since this is the empty vector, this case is generally either trivial or irrelevant. Because of this, the library includes another elimination form which ranges over vectors of length at least one:

vect_elim'_lemma:
  {A:Type}{n:nat}
  {m:vect A (suc n)}{P:(vect A (suc n))->Type}
  ({a:A}{m1:vect A n}P (vcons A a m1))->
  P m

This elimination lemma takes n as an explicit argument and takes the other arguments in a different order. Otherwise, the significant difference is that m ranges over vect A (suc n) as n ranges over natural numbers, so that the lemma proves properties of non-empty vectors.

Example

As an example of a proof using this type, we define a function from vectors to lists:

[A:Type];
Lego> Goal vector_to_list:{n|nat}(vect A n) -> (list A);
Goal
  ?0 : {n|nat}(vect A n)->list A
Lego> Refine vect_elim A ([n|nat][v:vect A n]list A);
Refine by  vect_elim A ([n|nat][_:vect A n]list A)
  ?1 : list A
  ?2 : A->{n|nat}(vect A n)->(list A)->list A
Lego> Refine nil A;
Refine by  nil A
  ?2 : A->{n|nat}(vect A n)->(list A)->list A
Lego> intros;
intros (4)
  a : A
  n | nat
  v : vect A n
  v_ih : list A
  ?3 : list A
Lego> Refine cons|A a v_ih;
Refine by  cons|A a v_ih
Discharge..  v_ih v n a
*** QED ***

Example

As another example, we will define a function from vect nat n (n-length vectors of natural numbers) to nat which calculates the product of the numbers in the vector.

Here is a straightforward derivation:

(* product of vector elements *)
Goal {n:nat}{v:vect nat n}nat;
Lego> Goal
  ?0 : {n:nat}(vect nat n)->nat
Lego> Refine vect_elim nat [n|nat][_:vect nat n] nat;
Refine by  vect_elim nat ([n|nat][_:vect nat n]nat)
  ?1 : nat
  ?2 : nat->{n|nat}(vect nat n)->nat->nat
Lego> Refine one;  (* case for an empty vector *)
Refine by  one
  ?2 : nat->{n|nat}(vect nat n)->nat->nat
Lego> intros;
intros (4)
  a : nat
  n | nat
  v : vect nat n
  v_ih : nat
  ?3 : nat
Lego> Refine times a v_ih;  (* a is the head, v_ih is the *)
Refine by  times a v_ih     (*  product of the tail *)
Discharge..  v_ih v n a

*** QED ***

Suppose we wanted to do this in a slightly more clever way. If we ever encounter a zero while computing the product, we can stop immediately and return zero. So let us try to express this:

 (* product of vectors 2 *)
Goal {n:nat}{v:vect nat n}nat;
Lego> Goal
  ?0 : {n:nat}(vect nat n)->nat
Lego> Refine vect_elim nat [n|nat][_:vect nat n] nat;
Refine by  vect_elim nat ([n|nat][_:vect nat n]nat)
  ?1 : nat
  ?2 : nat->{n|nat}(vect nat n)->nat->nat
Lego> Refine one;  (* base case -- same as before *)
Refine by  one
  ?2 : nat->{n|nat}(vect nat n)->nat->nat
Lego> intros;  (* inductive case *)
intros (4)
  a : nat
  n | nat
  v : vect nat n
  v_ih : nat
  ?3 : nat

Now we want to do a case split, depending on whether or not a is zero. We can do this by introducing a boolean induction, depending on the boolean predicate (nat_eq a zero) (in lib_nat_bool_rels). But we also need to introduce a boolean variable over which to do induction. To get the case split to be over the predicate we really want, we require that the new boolean variable be equal to the value of the predicate.

Lego> Refine bool_elim [b:bool](Eq b (nat_eq a zero)) -> nat;
Refine by  bool_elim ([b:bool](Eq b (nat_eq a zero))->nat)
  ?5 : (Eq true (nat_eq a zero))->nat
  ?6 : (Eq false (nat_eq a zero))->nat
  ?7 : bool
  ?8 : Eq ?7 (nat_eq a zero)

These last two goals are an artifact of the roundabout way we’ve had to do things – we can eliminate them right away:

Lego> Refine -0 Eq_refl;
Refine 8 by  Eq_refl
  ?5 : (Eq true (nat_eq a zero))->nat
  ?6 : (Eq false (nat_eq a zero))->nat

And now we have the two cases we wanted.

Lego> intros;
intros (1)
  H : Eq true (nat_eq a zero)
  ?11 : nat
Lego> Refine zero;              (* if a is zero return zero *)
Refine by  zero
Discharge..  H
  a : nat
  n | nat

  v : vect nat n
  v_ih : nat
  ?6 : (Eq false (nat_eq a zero))->nat
Lego> intros;
intros (1)
  H : Eq false (nat_eq a zero)   (* if a is non-zero return the product, *)
  ?12 : nat                        (* as before *)
Lego> Refine times a v_ih;
Refine by  times a v_ih
Discharge..  H
Discharge..  v_ih v n a
*** QED ***

This is a useful trick for introducing case splits. It works not only with boolean elimination, but other elimination rules as well.

Exercise: Define

vect_head:{A:Type}{n|nat}(vect A (suc n))->A
 and
vect_tail:{A:Type}{n|nat}(vect A (suc n))->vect A n

. Using your definitions, show

{n|nat}{v:vect A (suc n)}Eq (vcons A (vect_head A v) (vect_tail A v)) v

Finite Types

The finite type fin n is the type with n elements. The elements are denoted f_zero n, f_suc (f_zero n), and so forth. The inductive definition in the library is:

Inductive [fin:{n:nat}Type] ElimOver Type
Constructors
[f_zero:{n:nat}(fin (suc n))]
[f_suc:{n|nat}{x:(fin n)}(fin (suc n))];

Note that fin zero is the empty type, and the only element of fin one is f_zero zero You can think of the elements of fin n as the numbers 0, …, n − 1 built using f_zero n and f_suc rather than zero and suc.

The generated elimination rule is:

fin_elim : {P:{n|nat}(fin n)->Type}
            ({n:nat}P (f_zero n))->
            ({n|nat}{x:fin n}(P x)->P (f_suc x))->
             {n|nat}{z:fin n}P z

Again, since fin zero is the empty type, we are generally more interested in proving properties of non-empty types. To help with this the library included a derived elimination rule

fin_elim':
fin_elim' : {n:nat}{P:(fin (suc n))->Type}
              (P (f_zero n))->
              ({m:fin n}P (f_suc m))->
               {m:fin (suc n)}P m

As with the extra vector elimination form, fin_elim' takes n as an explicit argument.

Examples

Our first example defines a function from elements of finite types to natural numbers:

Lego> Goal fin_to_nat:{n|nat}{x:fin n}nat;
Goal
  ?0 : {n|nat}(fin n)->nat
Lego> Refine fin_elim ([n|nat][x:fin n]nat);
Refine by  fin_elim ([n|nat][_:fin n]nat)
  ?1 : nat->nat
  ?2 : {n|nat}(fin n)->nat->nat
Lego> Refine [n:nat]zero;
Refine by  [_:nat]zero
  ?2 : {n|nat}(fin n)->nat->nat
Lego> intros;
intros (3)
  n | nat
  x : fin n
  x_ih : nat
  ?3 : nat
Lego> Refine suc x_ih;
Refine by  suc x_ih
Discharge..  x_ih x n
*** QED ***

The second example is slightly more involved. It says that every element of a nonempty finite type is either f_zero or f_suc of something.

Lego> Goal {n:nat}{x:fin (suc n)}
      (or (Eq x (f_zero n)) (Ex [x':fin n]Eq x (f_suc x')));
Goal
  ?0 : {n:nat}{x:fin (suc n)}
      or (Eq x (f_zero n)) (Ex ([x':fin n]Eq x (f_suc x')))
Lego> intros n;
intros (1) n
  n : nat
  ?1 : {x:fin (suc n)}or (Eq x (f_zero n)) (Ex ([x':fin n]Eq x (f_suc x')))

Here we are doing induction over the non-empty finite sets, so we use fin_elim':

Lego> Refine fin_elim' n [x:fin (suc n)](or (Eq x (f_zero n))
                             (Ex [x':fin n]Eq x (f_suc x')));
Refine by  fin_elim' n ([x:fin (suc n)]or (Eq x (f_zero n))
                             (Ex ([x':fin n]Eq x (f_suc x'))))
  ?6 : or (Eq (f_zero n) (f_zero n)) (Ex ([x':fin n]Eq (f_zero n) (f_suc x')))
  ?7 : {m:fin n}or (Eq (f_suc m) (f_zero n))
                   (Ex ([x':fin n]Eq (f_suc m) (f_suc x')))

The base case is easy:

Lego> Refine inl;
Refine by  inl
  ?10 : Eq (f_zero n) (f_zero n)
  ?7 : {m:fin n}or (Eq (f_suc m) (f_zero n))
                   (Ex ([x':fin n]Eq (f_suc m) (f_suc x')))
Lego> Refine Eq_refl;
Refine by  Eq_refl

  ?7 : {m:fin n}or (Eq (f_suc m) (f_zero n))
                   (Ex ([x':fin n]Eq (f_suc m) (f_suc x')))

The inductive case is also pretty easy:

Lego> intros;
intros (1)
  m : fin n
  ?13 : or (Eq (f_suc m) (f_zero n)) (Ex ([x':fin n]Eq (f_suc m) (f_suc x')))
Lego> Refine inr;
Refine by  inr
  ?16 : Ex ([x':fin n]Eq (f_suc m) (f_suc x'))
Lego> Refine ExIntro;
Refine by  ExIntro
  ?18 : fin n
  ?20 : Eq (f_suc m) (f_suc ?18)
Lego> Refine +1 Eq_refl;
Refine 20 by  Eq_refl
Discharge..  m
Discharge..  n
*** QED ***

Warning: It is very easy to become confused by off-by-one (really off-by-suc) problems when dealing with finite types. I’m afraid I don’t have any really useful hints other than to experiment with these a bit.

Exercise: Prove {A:Type}{n|nat}{x:fin n}{v:vect A n}A. Note that this is a function which, given x:fin n, extracts the xth element of the vector v:vect A n.

Exercise: Using fin_to_nat as defined above, prove

{n|nat}{x:fin n}(Eq (suc (fin_to_nat x)) (fin_to_nat (f_suc x))).

This partly justifies the correctness of the fin_to_nat function.