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

Equality

In type theory, a notion of computation is usually considered more fundamental than a notion of equality. This gives us more freedom to consider different approaches to equality within a type theory. There are many proof-theoretic aspects of the treatment of equality within a formal system which are not obviously related to the actual equivalence relation (though the formal treatment does affect the relation defined). We’ll look at some of the general issues, then consider the options for equality in Lego.

An equivalence relation on terms indirectly defines which aspects of a term we are currently interested in. The idea of introducing an equivalence is to disregard certain differences between terms by making them equivalent, so that if two terms are not equivalent, they must be different in some interesting way. Various aspects of terms may be interesting in different contexts, requiring different notions of equality.

Intensional equality

This is a computational equality, usually described by taking the reflexive, transitive closure of the relation defined by the reduction rules. Two terms are intensionally equal if they are interconvertible. In type theories with strong normalization, two terms are intensionally equal if they have the same normal form. Usually, this is extended slightly to identify terms which are identical up to uniform renaming of variables (called α conversion).

Extensional equality

Intensional equality focuses on the computational behaviour of terms. In contrast, extensional equality describes the functional behaviour of terms. Two functions are extensionally equal if they produce equal results when applied to equal arguments. (Usually, in this context, base types are assumed to have their own built-in equality, and these are then used to define equality at more complex types.) Functions are extensionally equal if they compute the same (set-theoretic) function; functions are only intensionally equal if they compute the same function in essentially the same way.

Leibniz’s equality

The mathematician Leibniz expressed the idea that two things should be equal if all logical statements about them were logically equivalent. This notion of equality has been very important in the development of Lego. Since we use Prop as our universe of logical statements, this translates into the Lego definition

Eq = [x,y:T]{P:T->Prop}(P x) -> P y

Note that the type of Eq is T->T->Prop.

Exercise: Show that Eq is symmetric, i.e. (Eq a b) -> (Eq b a). Hint: Remember that Eq x y:Prop. This justifies the single implication in the definition instead of “if and only if”.

We have described three approaches to the meaning of equality; we have not mentioned reasoning about equality. There are many delicate issues involved when adding equality to a formal system. For example, we may want to consider a computational equality to be the fundamental equality in a system, but if we also wish to employ the propositions-as-types analogy, we must then reflect computational equality as a type in some way. So, in Martin-Löf’s type theories, we find both equality judgements (of the form M = N : T, meaning M equals N in type T), and equality types (or identity types) I(T, M, N), representing the proposition that M equals N in type T. The precise formulation of the rules connecting these ideas will influence the relationship between them.

Equality in Lego

In Lego, we have not yet had concern ourselves with the details of equality; we have taken certain axioms about equality as fundamental, and used those whenever we need equational reasoning. This approach is safe and appealing – our theorems can be used for any “well-behaved” equality without modification. As a reminder, these axioms are:

[refl = [T|Type][R:T->T->Prop]{t:T}R t t]
Eq_refl: {t|Type}refl (Eq|t)
[sym = [T|Type][R:T->T->Prop]{t,u|T}(R t u)->R u t]
Eq_sym: {t|Type}sym (Eq|t)
[trans = [T|Type][R:T->T->Prop]{t,u,v|T}(R t u)->(R u v)->R t v]
Eq_trans: {t|Type}trans (Eq|t)
[respect = [T|Type][S|Type][f:T->S][R:{X|Type}X->X->Prop]
           {t,u|T}(R t u)->R (f t) (f u)]
Eq_resp: {A|Type}{B|Type}{f:A->B}respect f Eq
Eq_subst: {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n

Given any relation Eq of type {A|Type}A->A->Prop and corresponding proofs of Eq_subst and Eq_sym, we can configure the Qrepl command (which replaces equals by equals in the current goal) to use the equality defined by Eq. The syntax for this is just:

Configure Qrepl Eq Eq_subst Eq_sym;

We’ll look at two of the possibilities available from the library: Leibniz’s equality and Martin-Löf’s inductive equality. Both of these are forms of intensional equality.

Leibniz’s equality

Although Leibniz’s equality is not the equality we have been using, it is easier to understand. The definition is straightforward:

[T|Type];
[     Eq = [x,y:T]{P:T->Prop}(P x)->P y
          : T->T->Prop
]

The axioms are proved using the definition, for example:

Goal
  ?0 : {t|T}Eq t t;
Lego> Intros;
Intros (3)
  t | T
  P : T->Prop
  H : P t

  ?1 : P t
Lego> Refine H;
Refine by  H
Discharge..  H P t
*** QED ***

Using Intros here instead of intros means that the definition of Eq is expanded. This proof is actually defined explicitly in the library:

[     Eq_refl = [t:T][P:T->Prop][h:P t]h
          : refl (Eq|T)
]

The substitution axiom is particularly easy to prove:

Goal {x,y|T}(Eq x y)->{P:T->Prop}(P x)->P y;
 Intros x y H P H1;
(*   H : Eq x y
     P : T->Prop
     H1 : P x  *)
 Refine H P H1;

Note, however, that P:T->Prop. The type of this axiom is more restrictive than the Eq_subst on the previous page. As a result, substitution (both directly and through Qrepl) is more restrictive than in it might be – substitution is only allowed in terms of type Prop. For this reason, we use a slightly different definition of equality.

Exercise: Prove the other properties of Eq. You can check your answers with those in the library.

Martin-Löf’s inductive equality

This is currently the default equality, from the file lib_ML_eq.l in the lib_Type library. Equality is defined inductively, with Eqr (representing reflexivity) the only constructor. The definition is:

$[Eq : {t|Type}t->t->Prop];
$[Eqr : {t|Type}{x:t}Eq x x];
$[Eq_elim : {t|Type}{P:{x,y:t}(Eq x y)->Type}({x:t}P x x (Eqr x))->
                {x,y:t}{p:Eq x y}P x y p];
[[t:Type]
 [P:{x,y:t}(Eq x y)->Type]
 [h:{x:t}P x x (Eqr x)]
 [x:t]
    Eq_elim P h x x (Eqr x) ==> h x];

It would be nice to use the Inductive type declaration to define this, but the type of Eqr is not allowed under the rules for inductive types.

Given this definition, proving Eq_refl is very easy:

Goal
  ?0 : {T|Type}{x:T}Eq x x
Lego> Refine Eqr;
Refine by  Eqr
*** QED ***
Save Eq_refl;

Proof of other properties are slightly more involved, generally using Eq_elim. This elimination rule essentially says that in order to prove a a property P of x,y:t and p:Eq x y, we need only show that it holds for all x and the reflexive case Eqr x. For example:

Lego> Goal {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n;
Goal
  ?0 : {t|Type}{m,n|t}(Eq m n)->{P:t->Type}(P m)->P n
Lego> Intros ___;
Intros (3) ___
  t | Type
  m | t
  n | t
  ?1 : (Eq m n)->{P:t->Type}(P m)->P n
Lego> Refine Eq_elim ([x,y:t][_:Eq x y]{P:t->Type}(P x)->P y);
Refine by  Eq_elim ([x,y:t][_:Eq x y]{P:t->Type}(P x)->P y)
  ?4 : {x:t}{P:t->Type}(P x)->P x             (* reflexive case *)
Lego> Intros;
Intros (3)
  x : t
  P : t->Type
  H : P x
  ?7 : P x
Lego> Immed;
Immediate
Discharge..  H P x
Discharge..  n m t
*** QED ***

This is a proof of Eq_subst for this equality. Note that P:t->Type, as opposed to the type of Eq_subst for Leibniz’s equality. This allows us to use equational reasoning in more contexts. An example of a theorem provable with this equality but not with Leibniz’s equality is

                                 absurd->empty

Recall that absurd:Prop and empty:Type. A proof of this theore must lift propositional absurdity to an element of the empty type. Eq_elim is the only function we’ve seen which lets a type depend on a particular proposition – since P:{x,y:t}(Eq x y)->Type, we can use x and y in the result as well as Eq x y. With the type-level Eq_elim, we can use bool_elim and the propositon Eq true false (provable by absurd) to produce an element of empty, as follows:

Goal
  ?0 : absurd->empty
Lego> intros;
intros (1)
  H : absurd
  ?1 : empty
Lego> Equiv bool_elim ([_:bool]Type) empty unit true;
Equiv
  ?1 : bool_elim ([_:bool]Type) empty unit true
(* unit is the singleton type; its only element is called void *)
Lego> Claim Eq true false;
Claim  Eq true false
  ?1 : bool_elim ([_:bool]Type) empty unit true
  ?3 : Eq true false

Lego> Qrepl ?+1;
Qrepl  ?3
true => false
(* now the first goal becomes unit *)
  ?13 : unit
  ?3 : Eq true false
Lego> Refine void;
Refine by  void
  ?3 : Eq true false
Lego> Immed;   (* since we have H: absurd, and this is a Prop *)
Immediate
Discharge..  H
*** QED ***
Lego>

With the Leibniz Eq_subst, Qrepl cannot work because the substitution is done in Type,

not Prop.