Computer Aided Formal Reasoning 1996/7 Lecture notes 8 Judith Underwood

Prop and Type

Until now I have been emphasizing the similarities between propositions and types. In Lego, however, there is a distinction – propositions are types, but not all types are propositions. (I have been somewhat sloppy about the distinction in these notes, but we will fix that soon.) The reason is that there are really two kinds of quantification in Lego, one which defines propositions and one which defines types. So far, we have been working mostly with propositions. However, we will use both ideas when we talk about existential quantification.

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 some of 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, x:S ⊢ T:Type}{G ⊢ \{x:S\}T:Type}

This is still slightly inaccurate, but it will do for now. Remember that the formula {x:S}T is simplified to S->T if T does not depend on x. There are more type constructors than this, which we’ll talk about later. We will also learn how to define new types inductively.

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 ⊢ and p q:Prop}  \frac{G ⊢ p:Prop   G ⊢ q:Prop}{G ⊢ or p q:Pr op}

     \frac{G ⊢ P:Prop   G, P:Prop ⊢ Q:Prop}{G ⊢ \{P:Prop\}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.

Existential quantification

So far, we have been using only universal quantification: creating and proving statements like “for all x of type A, property P holds of x.” If you’ve studied logic before, you may know that there is also existential quantification. This creates statements like “there exists an x in type A such that property P holds for x.” In classical logic, existential quantification can be defined from universal quantification, but this is not true constructively.

A constructive proof of a statement

∃x : A.P (x)

must contain a witness in the form of a particular a : A and a proof that P (a) holds. In classical logic, this is equivalent to the statement

¬∀x.¬P (x).

Constructively, this means that the assumption ∀x.¬P (x) leads to a contradiction, and this is not always enough to produce a witness.

Rules

The Lego notation for existential quantification is Ex P, where P: T ->Prop for some type T. Thus, the type of P determines the domain of the existential quantification. We’ll generally have existential formulas which look like Ex [x:A]B, to be read “there exists x of type A such that B”

– note that here P = [x:A]B which is of type A ->Prop.

The introduction and elimination rules for Ex are:

     \frac{G ⊢ witness:T   G, P:T ->Prop, witness:T ⊢ prf:P witness}{G ⊢ ExIntro witness P prf:Ex P}

           \frac{G ⊢ M:Ex P   G, N:Prop ⊢ prf:\{t:T\}(P t) -> N}{G ⊢ ExElim M N prf:N}

Thus, the connective Ex has type {T|Type}(T->Prop) -> Prop, and the introduction and elimination rules can be typed

ExIntro : {T|Type}{wit:T}{P:T->Prop}(P wit)->Ex P
ExElim : {T|Type}{P|T->Prop}(Ex P)->{N|Prop}({t:T}(P t)->N)->N

The elimination rule is something like the elimination rule for or. It says that in order to use a proof of Ex P to prove a proposition N, we must be able to prove N given any t and a proof of P t. This means that N cannot depend on t, that is, N cannot generally use the witness given in the proof of Ex P directly. Furthermore, we cannot use an existential Ex P to prove anything other than a proposition.

There is a computation rule for ExElim:

ExElim (ExIntro wit P prf) f => f wit prf

where

T : Type
wit : T
P : T -> Prop
prf : P wit
N : Prop
f : {t:T}(P t) -> N

There are actually two kinds of existential quantification in Lego. Given a proof prf of the formula Ex [x:T](P x), if T is a type other than Prop, we will not be able to recover the witness from prf. This is sometimes called weak existential quantification. Lego also has a form of strong existential quantification, in which we can always recover the witness from the proof. When T is Prop, we can recover the witness even with the weak quantifier. For convenience, the library includes special cases of the rules for when T is Prop, with an extra rule which recovers the witness for the proposition. The quantifier in this case is called ex, the introduction rule is ex_intro, and

instead of an elimination rule we have witness:{A|Prop}{P|A->Prop}(ex P)->A.

Example

Let’s look at a (very simple) example in Lego. We will prove

                          {T:Type}{t:T}Ex [s:T](Eq s t)

In other words, for all types T, for every t of type T, there exists something equal to t.

Lego> Goal {T:Type}{t:T}Ex [s:T](Eq s t);
Goal
  ?0 : {T:Type}{t:T}Ex ([s:T]Eq s t)
Lego> intros;
intros (2)
  T : Type
  t : T
  ?1 : Ex ([s:T]Eq s t)

Now we must supply a witness for the claim that there exists something equal to t. Since t is equal to t, we introduce it:

Lego> Refine ExIntro t;
Refine by  ExIntro t
  ?4 : Eq t t

This leaves us with the goal of showing that t is equal to t. But this is the reflexive axiom of equality, Eq_refl:

Lego> Refine Eq_refl;
Refine by  Eq_refl
Discharge..  t T
*** QED ***