Computer Aided Formal Reasoning Fall, 1995 Lecture notes 7 Rod Burstall and Judith Underwood

Prop and Type

Just as previous rules described how to construct terms of particular types, we now need rules to describe when types and propositions are well formed. Up until now, these rules have (mostly) been implicit, but now we wish to mix the ideas in order to prove propositions about functions, etc. of type other than Prop. Since the distinction is now a bit more important, it may be useful to have the rules describing the connections written down.

Type

  \overline{⊢bool:Type}           \overline{⊢nat:Type}           \frac{G ⊢t:Type}{G ⊢list t:Type}
                 \frac{G ⊢s:Type   G ⊢t:Type}{G ⊢s->t:Type}

There are more type constructors than this; we’ll talk about them later on.

Prop

The introduction rules for Prop describe when a proposition is well-formed:

          ⊢absurd:Prop

                               \frac{G ⊢T:Type   G ⊢m:T   G ⊢n:T}{G ⊢Eq m n:Prop}

     \frac{G ⊢p:Prop   G ⊢q:Prop}{G ⊢p->q:Prop} \frac{G ⊢p:Prop   G ⊢q:Prop}{G ⊢and p q:Prop}  \frac{G ⊢p:Prop   G ⊢q:Prop}{G ⊢or p q:Prop}

The relationship between Prop and Type is described by

                                   \overline{⊢Prop:Type}

There is a subtle point involved here, in that we also have

                                  Prop ⊂ Type

in the sense that if Lego is expecting some t of type Type, it will be satisfied if t is of type

Prop.

There is another even more subtle point, which is that Type is really a hierarchy of type universes

                           Type(0):Type(1):Type(2). . .

(and also

                        Type(0) ⊂ Type(1) ⊂ Type(2). . .)

but Lego can generally deduce which universe level is required. This hierarchy is necessary because having Type:Type leads to inconsistency, but for most purposes you don’t need to know which universe you’re working in.

Induction

We will now give rules for doing proofs by induction over nat, bool, and list. Let us first consider nat. The principle of mathematical induction for natural numbers is often written something like

∀P.(P 0) → (∀n.(P n) → (P (n + 1))) → (∀n.P n)

This says “given P, if P is true for 0, and, if given any n and a proof of P n we can prove P n+1, then we have that P holds for all n.” Formalizing this in Lego notation gives a rule

           \frac{G ⊢P:nat->Type   G ⊢M:P zero   G ⊢N:\{n:nat\} P n ->P(suc n)}{G ⊢nat elim P M N:\{x:nat\} P x}

We have made explicit the type of P and given the rule a name nat elim but otherwise this is just the same as the ordinary induction principle for natural numbers.

This should remind you of the nat rec operator we used earlier to define functions. In fact, nat rec is simply a special case of nat elim:

Lego> nat_rec;
value of nat_rec = [t|Type]nat_elim ([_:nat]t)
type  of nat_rec = {t|Type}t->(nat->t->t)->nat->t

Thus, nat rec is just a nat elim which attempts to work out the type of P. Normally, when we want to prove something by induction in Lego we will have to specify P; when we are using the computational meaning of induction, it’s generally clear what the type of the result is meant to be.

So, to prove a goal of the form

Goal
  ?0 : {x:nat}P x

in Lego, we would refine by nat elim, specifying P:

Lego> Refine nat_elim P;
Refine by  nat_elim P
  ?1 : P zero
  ?2 : {x1:nat}(P x1)->P (suc x1)

This generates two subgoals – show P zero holds, and show that, assuming P x1, we can conclude

P (suc x1).

Boolean induction works in a similar way:

                 \frac{G ⊢P:bool->Type   G ⊢M:P true   G ⊢N:P false}{G ⊢bool elim P M N:\{b:bool\}P b}

Again, bool rec is a special case of bool elim:

Lego> bool_rec;
value of bool_rec = [T|Type]bool_elim ([_:bool]T)
type  of bool_rec = {T|Type}T->T->bool->T

Exercise: Given that the type of list elim is

{t:Type}{P:(list t)->Type}
  (P (nil t))->
   ({x1:t}{x2:list t}(P x2)->P (cons1 t x1 x2))->
     {z:list t}P z

write list elim as a rule, like nat elim and bool elim above.

Note that list elim always takes the type t (the type of the objects in the list) as an argument, whereas both t and P are implicit arguments to list rec.

Exercise: Define list rec in terms of list elim. Check your definition against that in Lego.

Lego hints

Now that we have equational reasoning and induction, we can do more complicated proofs in Lego. Here are some more Lego commands which will help.

Qrepl Along with the built-in rules for equational reasoning, we can use a Lego command called Qrepl. This is essentially a more convenient version of Eq subst – it is used to replace equals by equals within a goal. More precisely, if our current goal has a subterm a, and we have an assumption H : Eq a b, then Qrepl H replaces all occurrences of term a in the goal with b. (It’s called Qrepl because the equality it was originally written for is denoted Q instead of Eq – it’s set up to work for Eq, though.)

Immed The command Immed tries to unify each goal with each hypothesis. Thus, if you have a hypothesis which is a more general form of some goal, Immed will prove that goal by specializing the hypothesis.

Equiv You can use Equiv to replace the current goal with something equivalent to it. You will get an error if Lego cannot determine that the two goals are equivalent. This is often useful for “normalizing” parts of a goal by hand, i.e. replacing a part of a goal with something it computes to, without having to normalize everything. Similarly, you can use Equiv replace a part of a goal with something which computes to the same thing.

Claim Claim adds its argument as a new goal. You can use the label which Lego generates (something of the form ?n) to then use this claim to prove another goal. Naturally, you will eventually have to prove your claim. Lego doesn’t support this sort of reasoning very well, so you should generally avoid it – if you reach a stage where you need a real lemma, you’re better off proving the lemma separately. Of course, since you’ve worked out a plan for the proof beforehand, you’ll know which lemmas you need before you start the proof.

Definitions If you want to define an identifier to be an abbreviation for some term, you can just write [id = term] Note that “term” here includes types as well, so if you want to have a name for the type of functions from nat to nat, you can say, e.g. [natfun = nat->nat]. The logical connectives are defined in this way in the library.

Exercises:

1. Prove that (Eq (append l (nil t)) l) for all lists l of type list t. (append is a library function.)

2. Again for lists l of type list t, prove

       (not (Eq l (nil t))) -> Ex [hd:tl] Ex [tl:list t] Eq l (cons1 t ht tl)

3. Prove, for all lists l and m of type list t,

             Eq (reverse (append l m)) (append (reverse m) (reverse l))

(reverse is another library function.)

Example

Here is an annotated example of (part of) a proof using some of these commands.

Lego> Goal {l:list nat}Eq (sum_list l) (sum_list (reverse l));
Goal
  ?0 : {l:list nat}Eq (sum_list l) (sum_list (reverse l))

Remember sum list from the first assignment – it adds the elements of a list of natural numbers. We prove this by induction on l.

Lego> Refine list_elim nat [l:list nat]Eq (sum_list l) (sum_list (reverse l));
Refine by  list_elim nat ([l:list nat]Eq (sum_list l) (sum_list (reverse l)))
  ?3 : Eq (sum_list (nil nat)) (sum_list (reverse (nil nat)))
  ?4 : {x1:nat}{x2:list nat}(Eq (sum_list x2) (sum_list (reverse x2)))->
       Eq (sum_list (cons1 nat x1 x2)) (sum_list (reverse (cons1 nat x1 x2)))

list elim nat says we’re proving this by induction over lists of natural numbers. The rest of the line is the predicate which we are trying to prove. The first goal is the base case, when we have the empty list. Both sides of the equality are equivalent to zero, so this is true by reflexivity of equality:

Lego> Refine Eq_refl;
Refine by  Eq_refl
  ?4 : {x1:nat}{x2:list nat}(Eq (sum_list x2) (sum_list (reverse x2)))->
   Eq (sum_list (cons1 nat x1 x2)) (sum_list (reverse (cons1 nat x1 x2)))

Eq refl solved the first goal as expected. The next goal is the inductive case. It will be clearer when we introduce all the hypotheses:

Lego> intros;
intros (3)
  x1 : nat
  x2 : list nat
  x2_ih : Eq (sum_list x2) (sum_list (reverse x2))
  ?7 : Eq (sum_list (cons1 nat x1 x2)) (sum_list (reverse (cons1 nat x1 x2)))

x2 ih is the inductive hypothesis. We want to rewrite the first sum list to unfold the definition one level, so we assert that it is equivalent to something of the form we want:

Lego> Equiv Eq (plus x1 (sum_list ?)) ?;
Equiv
  ?7 : Eq (plus x1 (sum_list x2)) (sum_list (reverse (cons1 nat x1 x2)))

Note that I did not have to write the whole goal over again – Lego matched the second part of Eq with the second question mark, and worked out that the first question mark must be x2. We now rewrite the second part, using the definition of reverse:

Lego> Equiv Eq ? (sum_list (append (reverse x2) ?));
Equiv
  ?7 : Eq (plus x1 (sum_list x2)) (sum_list (append (reverse x2) (cons x1
  (nil nat))))

Again, Lego worked out what the second argument to append must be. Now we use Qrepl and the inductive hypothesis to replace (sum list x2) in the goal with (sum list (reverse x2)):

Lego> Qrepl x2_ih;
Qrepl  x2_ih
sum_list x2 => sum_list (reverse x2)
  ?25 : Eq (plus x1 (sum_list (reverse x2))) (sum_list (append (reverse x2)
 (cons x1 (nil nat))))

and so on.