Formalizing

We have seen how to formalize (1) and (2). To express we need to formalize condition (3). First we define the induced relation (this is how it appears in the libraries). This language is a function of a given language , but that parameter is not always displayed although it is implicit.

We establish straight forwardly that is an equivalence relation.

The formulation of (3) as in Hopcroft and Ullman would be that is of finite index. But we will see that to prove constructively we need to be explicit that is a decidable language. So we take (3) to be: is decidable and is of finite index.

The proof of (3) from (2) appears to be the simplest of the implications. (From (2) we know immediately that is decidable.) We show that if refines , then the index of is no larger than that of , that is, So the only nonroutine step is to show

This follows directly from the fact that is extension invariant since , but then This seems to be the whole story until we look at the details of the lemma

It requires that we prove that the relation is decidable (see ). This complication suggests another more elegant proof which we outline after stating the theorem. This second proof is the one we formalize.

Corresp


Corresp

We can use the same devices as before to render this theorem more readable. Here is Stuart Allen's version.

Proof
The key idea in this proof is to show that where is like but is defined on the quotient type using the boolean valued function . This function characterizes in a simple way and is easier to work with than itself. This leads us to work with an equivalence relation instead of . The proof is essentially establishing two isomorphisms,

1. The first isomorphism follows from a lemma called quo_of_quo.
2. The second isomorphism follows from the lemma quo_of_finite. This is the heart of the proof. It requires that is a decidable relation.

Qed
Here is the main line of the Web proof as it appears after applying Allen's technique to the full Web proof. Here will be displayed as to reveal the dependence on . Notice that there are two side proofs as well as a number of lemma references. These can be expanded in the on-line version just by clicking on the names.
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.



12.
13.
14.
15.
16.
17.

The real work for us in proving this theorem was actually spent on building general facts about quotients and in defining and showing that it is an equivalence relation on . This required a long sequence of lemmas. All of this is left implicit in Hopcroft and Ullman who need at least the properties of @ on quotient sets and facts about equivalence relations on quotient sets.

EquivRel(