(*T* \usection{Mathematical Prelude}\label{sect-init} *T*)

(*T* We begin with the module |init| in which we: (1) prepare the use of
the universe |Prop| to represent the propositions of a {\em classical
logic with axioms for logical extensionality and proof irrelevance},
and (2) include further mathematical libraries, in particular those
providing data types and support for boolean values, natural numbers,
sets and relations, well-founded relations and dependent
equality. *T*)

(*T* An intuitionistic development of a UNITY-style temporal logic
seems to be possible if the definitions of the temporal operators are
slightly modified w.r.t. the original presentation in
\cite{ChandyMisra88}. However, in the present work we have chosen to
stay close to the original definitions of the temporal assertions.
Consequently, we decided to employ the following ``classical'' axioms
whenever helpful to derive temporal proof rules. In fact we found that
these axioms are rarely needed; we will mention each instance of their
use in our development. A classical set-theoretic semantics for CIC
that justifies all these axioms can be found in \cite{Werner97a}. Alternatively,
it is possible to use the semantics presented in Chapter~8 of this thesis. *T*)

(*T* A minimal form of classical logic is obtained by using the single
axiom |classic| given below, expressing the law of the excluded middle
for the universe |Prop|.

\begin{verbatim}
Axiom classic : (p:Prop)(p \/ ~p).
\end{verbatim}

In addition, we assume logical extensionality, stating that
logically equivalent propositions in |Prop| are equal. 

\begin{verbatim}
Axiom log_extensionality : (p,q:Prop)(iff p q)->(p==q). 
\end{verbatim}

Furthermore, we assume proof irrelevance for proofs of propositions in
|Prop|, i.e. two proofs of the same proposition are equal.

\begin{verbatim}
Axiom proof_irrelevance : (P:Prop)(p,q:P)(p==q).
\end{verbatim}

The last axiom provides a means to cast an object of type |(F x)| into
an object of type |(F y)| given a proof of |x==y|. In CIC this
elimination principle, which is in fact the |Type| counterpart of the
induction principle |eqT_ind|, is not provided by the inductive
definition of |==|, since its definition would require the
construction of an informative object from a noninformative one,
which is impossible in CIC.

\begin{verbatim}
Axiom eqT_rec : (A:Type; x:A; F:(A->Type))(F x)->(y:A)x==y->(F y) .
\end{verbatim}

Next we include a number of library modules that we briefly explain
below.

\begin{verbatim}
Require Arith.
Require Compare_dec.
Require Peano_dec.
Require Minus.
Require Arith_suppl.
Require Ensembles.      Definition set := [T : Type] (Ensemble T) .
Require Classical_sets .
Require Relations.
Require WfT.
Require WfT_nat.
Require EqdepT.
Require Finite_types.
\end{verbatim}

*T*)

(*BEGIN-H*)

Axiom classic : (p:Prop)(p \/ ~p).
Axiom log_extensionality : (p,q:Prop)(iff p q)->(p==q). 
Axiom proof_irrelevance : (P:Prop)(p,q:P)(p==q).
Axiom eqT_rec : (A:Type; x:A; P:(A->Type))(P x)->(y:A)x==y->(P y) .

Require Arith.
Require Compare_dec.
Require Peano_dec.
Require Minus.
Load Arith_suppl.
Require Ensembles.
Definition set := [T : Type] (Ensemble T) .
Require Classical_sets .
Require Relations.
Load WfT.
Load WfT_nat.
Load EqdepT.
Load Finite_types.

(*END-H*)

(*T* The modules |Arith|, |Peano_dec|,
|Compare_dec| and |Minus| contain definitions and facts related to the
type |nat| of natural numbers and the standard ordering which is given
by predicates |le| and |lt| for ``less or equal'' and ``less than'',
respectively.  The module |Arith_suppl| contains a set of auxiliary
theorems about |nat| needed in some proofs. The type |(Ensemble T)| of
sets over a type |T|, which is defined as |T -> Prop| and we prefer to write as |(set T)|, and
corresponding operations are provided by the modules |Ensembles| and
|Classical_sets|. Operations that we frequently use are |(Empty_set T)|, 
denoting the empty set over |T|, |(Add T S s)| denoting the
addition of an element |s| to a set |S| over |T| and |(Union T S S')|,
denoting the union of sets |S| and |S'| over |T|. |Classical_sets|
uses the axiom |classic| given above. The module |EqdepT|
provides a dependent equality. Compared with the standard polymorphic
equality it is more flexible concerning the argument types (they do
not have to be computationally equivalent). It is used in Section
\ref{sect-states} for state spaces with typed variables.  Relations
and their well-foundedness are defined in the modules |Relations| and
|WfT|, respectively.  Well-foundedness of the standard ordering on
natural number is provided by the module |WfT_nat|. These modules will
be used in Section \ref{liveness-section}, where temporal logic proof
rules for well-founded induction are developed. Finally, we need
cardinality and finiteness of types, which is provided by the module
|Finite_types|. *T*)

(*T* The modules |EqdepT|, |WfT|, and |WfT_nat| are our adaptions of
the module |Eqdep|, |Wf|, and |Wf_nat|, respectively, provided by the
COQ library, the main change being that it uses the universe |Type|
rather than the universe |Set|. These modifications reflect our
intention of using the predicative universe |Type| for data types
rather than the impredicative universe |Set|, which we do not use in
any essential way.\footnote{In the COQ library the data types reside
in |Set| (which is a subuniverse of |Type|), but we do not exploit its
impredicativity in this development. Hence, we assume without loss of
generality that |Set| is not used at all, an important point, which
makes it possible to understand our development in a purely
set-theoretic way, e.g.\ on the basis of \cite{Werner97a}.} Except for
|Arith_suppl| and |Finite_types| all other modules are part of the
mathematical library distributed with the COQ system, and we refer to
\cite{HuPa99} for more details. *T*)