Hints on proving theorems in Twelf, continued
Andrew W. Appel
March 2000
19. Extensionality & Equivalence Relations
Load the usual sources.cfg, then visit core/set/set.elf and load
that file (by control-C control-S). If you would like some exercises
to practice your proving skills, reprove each of the theorems
in that file by visiting proving7a.elf instead and replacing
each hole.
Now warm up by proving the following theorem:
set_congr: pf (eq A B) -> pf (set_equiv @ A @ B) = ...
The next theorem is just the converse. Prove this one,
and if you get stuck, see the hint (proving7b.elf) sooner
rather than later.
set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) = ...
Do not continue with this section until you have either proved
the theorem or looked at the hint.
More hints (but see proving7b first):
The solution to set_extensionality starts like this,
set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) =
[p1: pf (set_equiv @ A @ B)]
extensionality
(forall_i [x]
cut p1 [_]
hole (eq (A @ x) (B @ x))).
fill in the hole if you can; otherwise keep reading.
set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) =
[p1: pf (set_equiv @ A @ B)]
cut p1 [_]
extensionality
(forall_i [x]
or_e excluded_middle
([p11: pf (A @ x)]
hole (eq (A @ x) (B @ x)))
([p21: pf (not (A @ x))]
hole (eq (A @ x) (B @ x)))).
fill in the hole if you can; otherwise keep reading.
set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) =
[p1: pf (set_equiv @ A @ B)]
cut p1 [_]
extensionality
(forall_i [x]
or_e excluded_middle
([p11: pf (A @ x)]
cut (set_equiv_e1 p1 p11)
[p12: pf (B @ x)]
trans (extensional_true p11) (symm (extensional_true p12)))
([p21: pf (not (A @ x))]
hole (eq (A @ x) (B @ x)))).
fill in the hole if you can; otherwise keep reading.
set_extensionality: pf (set_equiv @ A @ B) -> pf (eq A B) =
[p1: pf (set_equiv @ A @ B)]
cut p1 [_]
extensionality
(forall_i [x]
or_e excluded_middle
([p11: pf (A @ x)]
cut (set_equiv_e1 p1 p11)
[p12: pf (B @ x)]
trans (extensional_true p11) (symm (extensional_true p12)))
([p21: pf (not (A @ x))]
cut (not_ei p21 [p22: pf (B @ x)] set_equiv_e2 p1 p22)
[p23: pf (not (B @ x))]
trans (extensional_false p21) (symm (extensional_false p23)))).
Well, that's all very nice, but our object logic doesn't have
an extensionality law, so these proofs can't be used. In fact,
now your Twelf server is corrupted by the loading of the extensionality
axioms, so you should reset Twelf (see the Twelf menu at the top
of the Emacs window) and reload the sources.cfg and core/set/set.elf.
Why do we avoid extensionality? There are three reasons:
1. It's unnecessary. We can do without it, so we avoid cluttering
are axiom base.
2. We wish to construct proofs that are checkable in many other
mechanical proof assistants, such as Coq (which uses the Calculus
of Constructions) or HOL (which uses higher-order logic). Coq
has no extensionality law -- in the full calculus of constructions
it is not sound -- so we will avoid it too.
3. If we build theorem libraries that rely on "eq" equality,
they will be insufficiently general. Very often the appropriate
equivalence relation on mathematical structures is not "eq"
but something else. Avoiding the extensionality axiom
disciplines us, requires us to construct more general theories.
Now, back to set_extensionality. Without the extensionality axiom,
set_extensionality is unprovable. Therefore, we must avoid
constructing theorems that rely on the "eq" equality of two sets;
instead we should rely on "set_equiv" equality. In general, each
type has its own natural equality function:
eqrel: tp -> tp = [T] T arrow T arrow form.
eq_arith: tm (eqrel num) = lam2 [x][y] eq x y.
eq_set: tm (eqrel (set T)) = set_equiv.
eq_form: tm (eqrel form) = lam2 [a][b] a equiv b.
Each of these has the property that it is an equivalence relation;
that is, it is reflexive, symmetric, and transitive.
Examine (and load) the file core/rel/equiv.elf and find the definition of
an equivalence relation:
valideqv: tm (rel T T arrow form) =
lam [R] reflexive @ R and symmetric @ R and transitive @ R.
Exercise: prove each of the following.
eq_arith_eqv: pf (valideqv @ eq_arith) = ...
eq_set_eqv: pf (valideqv @ eq_set) = ...
eq_form_eqv: pf (valideqv @ eq_form) = ...
Solutions in proving7d.elf.
It would be a good thing to make a utility lemma "valideqv_i" for proving
that things are equivalence relations. This lemma would include
the standard verbiage of
def1_i (and3_i (def1_i (forall_i ...))
(def1_i (forall2_i ...))
(def1_i (forall3_i ...)))
Using the lemma, we could prove eq_form_eqv more concisely:
eq_form_eqv: pf (valideqv @ eq_form) =
valideqv_i ([x] def2_i equiv_refl)
([x][y][p1: pf (eq_form @ x @ y)]
def2_i (equiv_symm (def2_e p1)))
([x][y][z][p2: pf (eq_form @ x @ y)]
[p3: pf (eq_form @ y @ z)]
def2_i (equiv_trans (def2_e p2) (def2_e p3))).
Exercise: Design and prove the valideqv_i lemma, so that the proof
above is valid. (Solution in proving7e.elf.)
We say that a function [respects extensionality] (is that the right
term?) if it maps equivalent arguments to equivalent results. But
there are many notions of "equivalent", as we have seen. So we must
phrase the notion more precisely:
function_extens: tm (eqrel S arrow eqrel T arrow (S arrow T) arrow form) =
lam3 [eqS: tm (eqrel S)]
[eqT: tm (eqrel T)]
[f: tm (S arrow T)]
forall2 [x: tm S][y: tm S] eqS @ x @ y imp eqT @ (f @ x) @ (f @ y).
An example is the predicate "isempty",
isempty: tm (set U arrow form) = lam [s] not (exists [x] s @ x).
Here, S is "set U", T is "form", and the theorem is that isempty
respects extensionality:
isempty_extens: pf (function_extens @ eq_set @ eq_form @ isempty) = ...
Exercise: Prove this theorem. Solution: proving7f.elf.
Suppose we have functions F and G, each of type (Ta arrow Tb), and
suppose we have an equality function (equivalence relation)
H1 on Ta and an equality H2 on Tb:
H1 : tm (eqrel Ta)
H2 : tm (eqrel Tb)
F : tm (Ta arrow Tb)
G : tm (Ta arrow Tb)
Then we say that F and G are equivalent functions if they map
equivalent arguments to equivalent results. This is expressed
by the eq+ predicate (found in core/eq.elf).
eq+ : tm (eqrel Ta arrow eqrel Tb arrow eqrel (Ta arrow Tb)) =
lam4 [H1 : tm (eqrel Ta)]
[H2 : tm (eqrel Tb)]
[F : tm (Ta arrow Tb)]
[G : tm (Ta arrow Tb)]
forall2 [x : tm Ta][y : tm Ta]
(H1 @ x @ y imp H2 @ (F @ x) @ (F @ y)) imp
(H1 @ x @ y imp H2 @ (G @ x) @ (G @ y)) imp
(H1 @ x @ y imp H2 @ (F @ x) @ (G @ y)).
(Actually, we are a bit more liberal: if F or G does not respect the
equivalences H1 & H2 -- that is, if F maps equivalent arguments to
inequivalent results -- then we're also willing to say that F=G. This
is mainly so that every function will be equivalent to itself.)
For example, consider two different formulations of isempty:
isempty: tm (set U arrow form) = lam [s] not (exists [x] s @ x).
isempty2: tm (set U arrow form) =
lam [s] forall [t] subset @ (set_union @ s @ t) @ t.
We can say that these functions are "equal" by asserting,
isempty_eq_isempty2: (eq+ @ eq_set @ eq_form) @ isempty @ isempty2.
So, eq+ is used to construct equality predicates on functions from
the equality predicates on the argument and result types.
Exercise: prove isempty_eq_isempty2.
Hints & solution: proving7g.elf.
Exercise: Using eq+, construct the appropriate equality function
for the type (num arrow num arrow num), and then show that
the following two functions are equal:
f: tm (num arrow num arrow num) = lam2 plus.
g: tm (num arrow num arrow num) = lam2 [x][y] plus y x.
Solution: proving7h.elf.
Conclusion: Though it's tempting to use the polymorphic "eq" function
in defining other predicates, beware. Users of your predicates
will be able to use the congruence rule (congr) to eliminate the eq, but
may have a difficult time introducing facts of the form (eq A B).
To avoid this problem, use the appropriate higher-order equality
function, constructed using eq+, eq_arith, eq_form, etc.