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

Existential quantification

Last time, we looked at using universal quantification to describe families of propositions. Today we will look at existential quantification. As with the other connectives, this is defined using quantification over types.

The treatment of existential quantification highlights another difference between classical and constructive logic. 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. It is generally insufficient to show merely that the assumption ∀x.¬P (x) leads to a contradiction.

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}

Definition of Ex

As with the other connectives, Ex is defined by its intended relationship to other propositions. Also as with the other connectives, you shouldn’t really need to know this – the rules above should be sufficient for proofs in Lego. However, these definitions may explain some of the surprises you get when running Lego.

In this case, we can use an existential statement Ex P to prove a proposition B if we can use a proof of P a (for any a) to prove B.

The definition of Ex is:

    Ex = [P:T->Prop]{B:Prop}({t:T}(P t)->B)->B : (T->Prop)->Prop

Note that t cannot be free in B, so that B cannot depend on the particular witness. Note also that B must be a Prop; if T is a type other than Prop, we cannot recover the witness directly. 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.

ExIntro and ExElim are also defined:

ExIntro = [wit:T][P:T->Prop][prf:P wit][B:Prop][gen:{t:T} (P t)->B]gen wit prf
          : {wit:T}{P:T->Prop}(P wit)->Ex P
ExElim = [P|T->Prop][M:Ex P][N|Prop][prf:{t:T}(P t)->N]M N prf
          : {P|T->Prop}(Ex P)->{N|Prop}({t:T}(P t)->N)->N

Exercise: Give a computation rule for ExElim.

Equality

We have been working towards predicate logic, i.e. a way of forming propositions which depend on variables (of some kind). Predicate logic is used to describe logical properties of some domain, e.g. natural numbers. One such property (a particularly important one) is equality. Lego can be configured to use any one of several different notions of equality, but for now we’ll just be using the basic properties given in the rules below.

Rules for Equality

Equality is, like other operations, implicitly quantified over types. Thus, for each property, there is an implicit argument [t|Type] which specifies that the equality is on type t. This means that two objects of different types cannot be compared for equality.

The most fundamental property of equality is that it is an equivalence relation; that is, equality is reflexive, symmetric, and transitive. The axioms which specify this are:

Eq_refl: {t|Type}refl (Eq|t)
Eq_sym: {t|Type}sym (Eq|t)
Eq_trans: {t|Type}trans (Eq|t)

where refl, sym, and trans are defined for general relations R:T->T->Prop:

Lego> refl;
value of refl = [T|Type][R:T->T->Prop]{t:T}R t t
type  of refl = {T|Type}(T->T->Prop)->Prop
Lego> sym;
value of sym = [T|Type][R:T->T->Prop]{t,u|T}(R t u)->R u t
type  of sym = {T|Type}(T->T->Prop)->Prop
Lego> trans;
value of trans = [T|Type][R:T->T->Prop]{t,u,v|T}(R t u)->(R u v)->R t v
type  of trans = {T|Type}(T->T->Prop)->Prop

Written as rules, these are:

                             G, t:T ⊢Eq refl:Eq t t
                      G,t:T,u:T ⊢Eq sym:(Eq t u) ->Eq u t
              G,t:T,u:T,v:T ⊢Eq trans:(Eq t u)->(Eq u v)->(Eq t v)

Two more axioms for equality are more easily understood as rules than as axioms. They describe the fact that predicates and functions must respect equality. The first actually says that if m and n are equal in type T, then P m implies P n for all P:

               \frac{G, m:T, n:T ⊢M: (Eq m n)}{G, m:T, n:T ⊢Eq subst M :\{P: T ->Type\}(P m) ->P n}

The second rule says that if a function is applied to equal inputs, the results must be equal (in the range type):

                        \frac{G ⊢f:T->S   G ⊢M:Eq t1 t2}{G ⊢Eq resp f M :Eq (f t1) (f t2)}

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 one of the axioms of equality, the reflexive axiom, which is named Eq refl:

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

Lego hint: Because the rules for reasoning about equality are so basic, proofs about general equalities can be quite complicated. This is particularly the case when reasoning about functions defined by induction. It will become increasingly difficult to do your proofs while sitting at the computer. Thus, it is a good idea to have a plan on paper to help guide your proof. In other words, treat developing a proof like you would developing a program . . ..