(*T* \uchapter{A Toy Example in Program Verification}\label{chap-example} *T*)

(*T* In this section we demonstrate the use of the temporal logic
library for the verification of UNITY programs by means of a very
simple example. We describe a formal specification and verification of
the well-known ``Common Meeting Time Problem''. The example will be
reused in Section \ref{sect-comp-example} to demonstrate the use of
our compositionality results that we develop in Section
\ref{sect-union}. *T*)

(*T* What we will present in the following can be seen as a special
instance of an embedding of UNITY programs into CIC via their
transition system semantics. From the viewpoint of type theory the
most natural concept that could be used to represent a UNITY statement
is that of an operation which can be effectively executed. To exploit
the power and elegance of type theory for the verification of
functional programs it seems advantageous to view a UNITY
program as a collection of communicating functional components. Each
of these components can be specified and verified within type theory
using standard techniques. More precisely, we represent a UNITY
program as a set of functions operating on a shared state space and
communicating via its variables. In fact, such representations
correspond to a subclass of transitions systems that we called {\em
functional transiton systems} in \cite{Stehr98-coqunity}.\footnote{We
also would like to point out that a limitation of the approach
in \cite{Stehr98-coqunity}, namely the requirement that a UNITY program
has only a finite number of statements and therefore can be
represented as a list, is not enforced any more in the present state
of the library due to the use of arbitrary transition systems.} *T*)

(*T* To further motivate the representation of UNITY programs that we
have choosen, we would like to point out another benefit of the use of
a strongly normalizing type theory such as CIC: The idea that an
operational statement in the program should represent an {\em atomic}
execution step nicely corresponds to the fact that all operations in
CIC are total and terminating. So, termination proofs are implicit at
the level of atomic steps. They are done by type checking and
therefore do not require manual intervention. In summary, we have
termination at the level of individual actions (ensured by strong
normalization of CIC), but for the entire program termination is not
enforced. Another important issue often related to termination is
determism.  Again, we have determinism at the level of statements
(ensured by confluence of CIC), reflecting the fact that each single
statement has a unique result, but for the entire program (and its
components) determinism is not enforced. *T*)

(*T* It should be clear that, although we use UNITY programs as an
example in this section, the functional transition system
representation described above is not limited to programs in the UNITY
programming language, but it can be used to represent programs in
other languages as well, provided that atomic statements can be
expressed as functions in CIC. In fact, functional transition systems
are a specialization of general transition systems that allow us to
express the central concept of executability using the type-theoretic
notion of a computable function.  *T*)

(*T* In the following we briefly recall the common meeting time
problem and a solution in terms of a simple UNITY program.  Modeling
time by natural numbers the problem is to find the earliest possible
common meeting time for two persons. We presuppose the existence of
such a common meeting time and for each of the two persons we assume a
function, say |f| and |g|, respectively, such that |f(t)| and |g(t)|
is the earliest availability time not earlier than |t|.  We are looking
for a program that has a variable |time| and satisfies the following
temporal specification: (1) {\em Partial correctness}, i.e. |time| is
approximating the common meeting, i.e. it will never decrease and will
never exceed the smallest common meeting time. (2) {\em Total
correctness}, i.e.  in addition to partial correctness, |time| will
eventually contain the smallest common meeting time.  A solution
satisfying this informal specification is provided by the UNITY
program |CMT| given below.  Observe that the UNITY fairness
requirement is essential for total correctness.

\begin{verbatim}
Program CMT
declare time : nat
initially time = 0  
assign time := f(time)
     | time := g(time)
end
\end{verbatim}
*T*)

(*T* In the remainder of this section we will demonstrate the use of
the temporal logic library to: (1) give a formal representation of the
program, (2) formalize it's informal specification, i.e. the
assumptions and the temporal properties of partial and total
correctness, and (3) prove formally that the program satisfies the
specification. *T*)

(*T* \usection{A Concrete Frame} *T*)

(*T* We replace the abstract frame |var_abstract| explained in Section
\ref{sect-ssvars} by a concrete frame which starts with the assumptions
stated in the informal explanation of the problem and a specification
of the program given above. In other words, the temporal logic library
is instantiated for a particular class of programs parameterized by
functions |f| and |g| satisfying the assumptions stated above. *T*)

Load init.

(*T* It follows from the informal problem specification that we can
assume two functions |f| and |g| on natural numbers which are
ascending and monotone. *T*)

Variables f,g : nat->nat.
Axiom f_is_ascending : (m:nat)(le m (f m)).
Axiom g_is_ascending : (m:nat)(le m (g m)).
Axiom f_is_monotone : (m,n:nat)(le m n)->(le (f m) (f n)).
Axiom g_is_monotone : (m,n:nat)(le m n)->(le (g m) (g n)).

(*T* The concept of a common meeting time is formulated as a common
fixpoint of |f| and |g|. 

\begin{verbatim}
Definition common := [t:nat] (f t)==t /\ (g t)==t.
\end{verbatim}
*T*)

(*BEGIN-H*)
Definition common := [t:nat] (f t)=t /\ (g t)=t.
(*END-H*)

(*T* Next we assume that a smallest common meeting time, which we
denote by |cmt|, exists, as our informal specification states.  *T*)

Variable cmt : nat.
Axiom cmt_exists : (common cmt).
Axiom cmt_smallest : (m:nat)(common m)->(le cmt m).

(*T* Subsequently, we describe the concrete embedding of the UNITY
program |CMT|, seen as a transition system, into CIC. We carry out the
transformation manually, but it should be obvious that this process
can be easily mechanized. *T*)

(*T* The program contains exactly one program variable |time|. It is
represented by a variable name |time|, which is the only element of the
following inductive type |var|. For simple programs like ours the
inductive type is a simple enumeration type, but there are also
applications in which other kinds of inductive types could be
exploited, e.g. to represent families of program variables. *T*)

Inductive var : Type := time : var.

(*T* We also provide the enumeration function |ith_var| of |var| as
required by the abstract frame together with a proof of finiteness of
|var|. *T*)

Definition vars := (1) .
Definition ith_var := [i:nat] time.

Theorem var_finite : (v:var)
  (ExT [i:nat] (lt i vars) /\ (ith_var i)==v).

Induction v.
Exists  O.
Split.
Unfold vars.
Apply lt_n_Sn.
Unfold ith_var.
Reflexivity.
Qed.

(*T* The abstract frame also requires a decision function for equality
on |var|, which here follows directly from the induction
principle for enumeration types. *T*)

Theorem var_eq_dec : (v,v':var){(v==v')}+{~(v==v')}.

Induction v.
Induction v'.
Left.
Reflexivity.
Qed.

(*T* In addition to a variable name we need names for all types
occurring in the program. Again we have |type_name| as an enumeration
type with a single type name |unat| intended to represent the CIC type
|nat| of natural numbers as specified by the function |type|. *T*)

Inductive type_name : Type := unat : type_name.

Definition type := [n:type_name]
  Cases n of unat => nat end.

(*T* The declaration of program variables is translated into the
function |var_type_name| which maps |time| to its associated type name
|unat|. *T*)

Definition var_type_name := [v:var]
  Cases v of time => unat end.

Definition var_type := [v:var] (type (var_type_name v)).

(*T* Now, after all variables together with their types have been
fixed we define the state space |st| as in the module
|var_abstract|. *T*)

Definition st := (v:var)(var_type v).

Load var_state_ops.

(*T* After setting up the state space we have to represent the
statements of the UNITY program. First, we define |act| as a
enumeration type containing an action for each statement. *T*)

Inductive act : Type :=
  update_f : act | update_g : act.

(*T* Then these actions are related to the statemens of the program by
a transition function |effect|, which specifies the effect of each
action as given by the semantics of its corresponding statement. It
takes the form of a case analysis over all actions. *T*)

Definition effect := [t:act] 
  Cases t of 
          update_f => [s:st] (assign s time (f (s time)))
        | update_g => [s:st] (assign s time (g (s time)))
  end.

(*T* On the basis of this functional transition system representation
the transition relation |trans| can be directly defined: *T*)

Definition trans := [t:act][s,s':st]
  (s' == (effect t s)) .

(*T* Now the type of views is introduced as in |var_abstract|, and
finally the body of the UNITY program |CMT| is represented by its set
of actions, which are |update_f| and |update_g| in our case. *T*)

Definition view := act->Prop.

Definition CMT := 
  (Add act (Add act (Empty_set act) update_g) update_f) .

(*T* Finally, we have to specify the unconditional fairness of UNITY,
which is a special case of weak group fairness. The set |wf| of weakly
fair groups contains by convention the empty group and in addition a
singleton group for each statement.  *T*)

Definition wf := 
  (Add (set act) (Add (set act) (Add (set act) 
  (Empty_set (set act))
  (Empty_set act))
  (Singleton act update_f))
  (Singleton act update_g)).

Theorem wf_contains_empty_set : 
  (In (set act) wf (Empty_set act)).

Unfold wf.
Auto with v62.
Qed.

(*T* On top of our concrete program specification we include the
rest of the general library and also the more specific modules
supporting the state space with typed variables. By including these
modules in the context established above they are instantiated for our
particular application. *T*)

Load state_pred.

Load safety.
Load liveness.

Load var_state_pred.
Load var_elim.


(*BEGIN-H*)

Lemma enabled_vacuous : (t:act)(s:st)(enabled t s) .

Intros.
Unfold enabled.
Split with (effect t s).
Unfold trans.
Trivial.
Qed.

Lemma hoare_sc : (t:act)(p,q:s_prop)
  ((s:st)(enabled t s)->(p s)->(q ((effect t) s))) ->
  (hoare t p q).

Unfold hoare.
Unfold trans.
Intros.
Rewrite H0.
Apply H.
Apply enabled_vacuous.
Trivial.
Qed.

Theorem sys_contains_update_g :
  (Included act (Singleton act update_g) CMT).

Unfold Included CMT.
Intro t.
Intros.
Generalize (Singleton_inv ? ? ? H).
Intros.
Rewrite <- H0.
Auto with v62.
Qed.

Theorem sys_contains_update_f :
  (Included act (Singleton act update_f) CMT).

Unfold Included CMT.
Intro t.
Intros.
Generalize (Singleton_inv ? ? ? H).
Intros.
Rewrite <- H0.
Auto with v62.
Qed.

(*END-H*)

(*T* \usection{Partial Correctness} *T*)

(*T* Our overall strategy is to establish first safety assertions for
partial correctness, and then, on top of such safety assertions, liveness
assertions, that are additionally needed for total correctness, are
proved. The two main theorems we prove will correspond exactly to our
informal specification given before. *T*)

(*T* We start with a lemma which states that if |time| has a value |m|,
then at each successor state |time| will not increase above |(f m)| or
it will not increase above |(g m)|. The proof is done by unfolding
|co| and then verifying the assertions for both actions |update_f| and
|update_g|. *T*)

Lemma CMT_S1 : (m:nat)
  (co CMT ([s:st] (eq nat (s time) m))
          ([s:st] (le (s time) (f m)) \/ (le (s time) (g m)))).

Intros.
Unfold CMT.
Unfold co.
Intros.
Apply hoare_sc.
Intros.
Elim H.
Intros.
Elim H2.
Intros.
Elim H3.

Intros.
Specialize (Singleton_inv ? ? ? H3).
Clear H3.
Intro.
Rewrite <- H3.
Right.
Simpl.
Rewrite assign_changed.
Rewrite H1.
Apply le_n.

Intros.
Left.
Specialize (Singleton_inv ? ? ? H2).
Clear H2.
Intro.
Rewrite <- H2.
Simpl.
Rewrite assign_changed.
Rewrite H1.
Apply le_n.
Qed.

(*T* Following \cite{Misra94,Misra95} we obtain the next lemma |CMT_S2| by applying 
the elimination theorem on the program variable |time|.
To this end, we instantiate |x|, |p| and |q| in Theorem |elimination| by |time|,
|[s:st](common n)->(le (s time) n)| and 
|[m:nat][s:st](le (s time) (f m))\/(le (s time) (g m))|, 
respectively. Independence of
|p| from variables different from |x| is trivially satisfied, as |time|
is the only program variable.  The remaining |co| premise is given exactly by
Lemma |CMT_S1|.  *T*)

Lemma CMT_S2 : (n:nat)
  (co CMT [s:st]((common n)->(le (s time) n))
          (s_ex ? [m:nat] 
           [s:st]((common n)->(le m n))/\
                 ((le (s time) (f m))\/(le (s time) (g m))))).

Intros.
Generalize (elimination CMT time
             [s:st](common n)->(le (s time) n)
             [m:nat]
              [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intro.
Cut (v:var)
     ~v==time
      ->(independent [s:st](common n)->(le (s time) n) v).
Intro.
Cut (m:(var_type time))
     (co CMT [s:st](eq nat (s time) m)
       [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intro.
Cut (m:(var_type time))
     (co CMT [s:st](s time)==m
       [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intros.
Generalize (H H0 H2).
Clear H2.
Clear H.
Intro.
Apply co_implication_r
 with q:=(s_ex (var_type time)
           [m:(var_type time)]
            (s_and
              (subst [s:st](common n)->(le (s time) n) time m)
              [s:st](le (s time) (f m))\/(le (s time) (g m)))).
Unfold everywhere s_imp s_and subst var_type.
Unfold type var_type_name.
Unfold s_ex.
Intros.
Elim H2.
Intros t H3.
Split with t.
Elim H3.
Intros.
Split.
Intro.
Generalize (H4 H6).
Rewrite assign_changed.
Intro.
Assumption.
Assumption.
Assumption.
Intros.
Apply co_implication_l with 2:=(H1 m).
Unfold everywhere s_imp.
Intros.
Rewrite H2.
Reflexivity.
Unfold var_type.
Unfold var_type_name type.
Exact CMT_S1.
Induction v.
Intro.
Apply False_ind.
Unfold not in H0.
Apply H0.
Reflexivity.
Qed.

(*T* The next lemma states that |time|, which is advanced by the
program, cannot skip any common meeting time. The proof starts with
the |co| assertion of the preceding lemma and uses right hand side
weakening to obtain the |stable| assertion. *T*)

Lemma CMT_S3 : (n:nat)
  (stable CMT
     ([s:st] (common n) -> (le (s time) n))).

Intro.
Unfold stable.
Apply co_implication_r with q:=(s_ex ?
                                   [m:nat]
                                    [s:st]
                                     ((common n)->(le m n))
                                     /\((le (s time) (f m))
                                        \/(le (s time) (g m)))).
Unfold everywhere s_imp s_ex.
Intros.
Elim H.
Intros t H1.
Clear  H.
Elim H1.
Intros.
Clear  H1.
Generalize (H H0).
Intro.
Generalize (f_is_monotone t n H1).
Intro.
Generalize (g_is_monotone t n H1).
Intro.
Unfold common in H0.
Elim H0.
Intros.
Rewrite H5 in H3.
Rewrite H6 in H4.
Elim H2.
Intro.
Apply le_trans with (f t).
Assumption.
Assumption.
Intro.
Apply le_trans with (g t).
Assumption.
Assumption.
Apply CMT_S2.
Qed.

(*T* Since
|([s:st] (common n) -> (le (s time) n)))|
holds initially, i.e. it is implied by |[s:st](s time)=O|, we
can establish an inductive invariant. *T*)

Lemma CMT_S4 : (n:nat)
  (ind_invariant CMT [s:st](eq nat (s time) O)
     ([s:st] (common n) -> (le (s time) n))).

Intro.
Unfold ind_invariant.
Split.
Unfold everywhere s_imp.
Intros.
Rewrite -> H.
Apply le_O_n.
Apply CMT_S3.
Qed.

(*T* Substituting |cmt| for |n| we obtain Theorem |CMT_5| establishing
the fact that |time| cannot increase beyond the smallest common
meeting time |cmt|.

\begin{verbatim}
Theorem CMT_S5 : (ind_invariant CMT 
  [s:st](s time)==O [s:st](le (s time) cmt)).
\end{verbatim}
*T*)

(*BEGIN-H*)
Theorem CMT_S5 : (ind_invariant CMT 
  [s:st](s time)=O [s:st](le (s time) cmt)).
(*END-H*)

Generalize (CMT_S4 cmt).
Intros.
Apply ind_invariant_subst with 3:=H.
Unfold everywhere s_imp.
Auto with v62.
Unfold everywhere s_iff.
Intros.
Split.
Intros.
Apply H0.
Apply cmt_exists.
Intros.
Trivial.
Qed.

(*T* Finally, we prove Theorem |CMT_S6|, stating that |time| can only
increase but never decreases. The proof is done by unfolding |co| and
then by considering each of the two actions |update_f| and |update_g|,
using the axioms |f_is_ascending| and |g_is_ascending|,
respectively. *T*)

Theorem CMT_S6 : (m:nat)
  (co CMT [s:st](eq nat m (s time)) 
          [s:st](le m (s time))).

Unfold CMT.
Unfold co.
Intros.
Apply hoare_sc.
Intros.
Elim H.
Intros.
Elim H2.
Intros.
Elim H3.

Intros.
Specialize (Singleton_inv ? ? ? H3).
Clear H3.
Intro.
Rewrite <- H3.
Simpl.
Rewrite (assign_changed s time (g (s time))).
Rewrite <- H1.
Apply g_is_ascending.

Intros.
Specialize (Singleton_inv ? ? ? H2).
Clear H2.
Intro.
Rewrite <- H2.
Simpl.
Rewrite (assign_changed s time (f (s time))).
Rewrite <- H1.
Apply f_is_ascending.
Qed.

(*T* Together the theorems |CMT_S5| and |CMT_S6| state partial correctness
according to our informal specification. *T*)

(*T* \usection{Total Correctness} *T*)

(*T* In order to establish total correctness we have to prove the
liveness assertion stating that the smallest common meeting time |cmt|
is reached eventually if the program starts in a sate satisfying the
initialization condition. *T*)

(*T* Formally, we wish to prove
\begin{verbatim}
(leads_to CMT ([s:st](eq nat (s time) O))
              ([s:st](eq nat (s time) cmt)))
\end{verbatim}
as formulated in Theorem |CMT_L14|. To this end we employ
(reverse) induction on natural numbers according
to Theorem |leads_to_rev_nat_induction|. We have to supply 
a variant which increases up to some maximum value.
An obvious choice is the value of the variable
|time|, together with the smallest common meting time
|cmt| as its maximum value. *T*)

Definition variant := [s:st](s time).

(*T* Below we need the following lemma |CMT_S7|, a special case
obtained from Lemma |CMT_S3| by instantiating |n| with |cmt|. *T*)

Lemma CMT_S7 : (stable CMT [s:st](le (variant s) cmt)).

Unfold variant.
Generalize (CMT_S3 cmt).
Intros.
Apply (stable_subst CMT) with p:=[s:st]
                                     (common cmt)->(le (s time) cmt).
Unfold everywhere s_iff.
Intros.
Split.
Intros.
Apply (H0 cmt_exists).
Intros.
Auto with v62.
Auto with v62.
Qed.

(*T* In the following we prepare the application of the reverse
induction rule |leads_| \linebreak |to_rev_nat_induction|, which will
be used later to prove Lemma |CMT_L13|, which in turn immediately
implies the final liveness property |CMT_L14|. The |leads_to|
assertion in the premise of the reverse induction rule is proved in
Lemma |CMT_L12| directly, as an |ensures| assertion. *T*)

(*T* We begin with the proof of the safety part of this |ensures|
assertion, which is the |unless| assertion given in Lemma |CMT_S8|: If
|time| is not beyond |cmt|, then there are only two possibilities for
the next state: Either we reach |cmt|, or |time| increases but not
beyond |cmt|. The proof unfolds |unless| and applies
|co_stable_conjunction| to |CMT_S7| and |CMT_S6|. Then
|co_implication| is used to obtain the goal. *T*)

Lemma CMT_S8 : (m:nat)
  (unless CMT
     (s_and [s:st](le (s time) cmt) 
            [s:st](eq nat m (s time)))
     (s_or
       (s_and [s:st](le (s time) cmt) 
              [s:st](lt m (s time)))
       [s:st](eq nat (s time) cmt))).

Intros.
Generalize (co_stable_conjunction CMT [s:st](eq nat m (s time))
             [s:st](le m (s time)) [s:st](le (variant s) cmt)
             CMT_S7 (CMT_S6 m)).
Intros.
Unfold unless.
Apply co_implication with p':=(s_and [s:st](eq nat m (s time))
                                  [s:st](le (variant s) cmt)) q:=(
s_and [s:st](le m (s time)) [s:st](le (variant s) cmt)).
Unfold everywhere s_imp s_or s_and.
Intros.
Unfold variant.
Elim H0.
Intros.
Elim H1.
Intros.
Split.
Auto with v62.
Auto with v62.
Unfold everywhere s_imp s_and s_or.
Intros.
Elim H0.
Intros.
Clear  H H0.
Unfold variant in H2.
Elim (eq_nat_dec m (s time)).
Intros.
Left.
Split.
Auto with v62.
Auto with v62.
Intros.
Right.
Left.
Split.
Auto with v62.
Elim (le_lt_or_eq m (s time)).
Intros.
Auto with v62.
Intros.
Elim y.
Auto with v62.
Auto with v62.
Auto with v62.
Qed.

(*T* The liveness part of the aforementioned |ensures| assertion will
be provided by the |transient| assertion in Lemma |CMT_L11|, which in
turn will be proved from the following lemma |CMT_L10| via an
intermediate lemma |CMT_L9| which states: If |time| is not a common
meeting time, then |time| will eventually change. *T*)

Lemma CMT_L9 : (m:nat) (transient CMT 
  [s:st](not (common (s time))) /\ (eq nat m (s time))).

Intros.
Unfold transient.
Unfold transient.
Elim (eq_nat_dec m (f m)).
Intros.
Split with (Singleton ? update_g).
Split.
Unfold wf.
Auto with v62.

Split.
Exact sys_contains_update_g.

Unfold sco.
Intros.
Unfold en.
Split.
Intros.
Split with update_g.
Split.
Auto with v62.

Apply enabled_vacuous.

Unfold co.
Intro.
Intro.
Apply hoare_sc.
Intros.
Unfold s_not.
Unfold not.
Specialize (Singleton_inv ? update_g e H).
Intros.
Rewrite <- H2 in H3.
Unfold effect in H3.
Unfold common in H3.
Elim H1.
Intros.
Unfold common in H4.
Elim H3.
Clear H0.
Intros.
Clear H3.
Apply H0.
Clear H0.
Rewrite <- H6.
Split.
Auto.

Rewrite <- H5 in H6.
Rewrite (assign_changed s time (g m)) in H6.
Auto.

Intros.
Split with (Singleton ? update_f).
Split.
Unfold wf.
Auto with v62.

Split.
Exact sys_contains_update_f.

Unfold sco.
Split.
Unfold en.
Intros.
Split with update_f.
Split.
Auto with v62.

Apply enabled_vacuous.

Unfold co.
Intros.
Apply hoare_sc.
Intros.
Specialize (Singleton_inv ? update_f e H).
Clear H.
Intros.
Unfold s_not.
Unfold not.
Intros.
Elim H2.
Clear H2.
Intros.
Rewrite <- H in H2.
Rewrite <- H in H3.
Clear H.
Unfold effect in H2.
Unfold effect in H3.
Rewrite assign_changed in H2.
Rewrite assign_changed in H3.
Elim H1.
Clear H1.
Intros.
Rewrite <- H1 in H3.
Apply (y H3).
Qed.

(*T* The proof is done by unfolding |transient| and distinguishing two
cases: If |m| equals |(f m)| then |update_g| is responsible for
progress, otherwise |update_f| is the witness of progress.  *T*)

(*T* Using |transient_implication| and the fact that |cmt| is the
smallest common meeting time we obtain Lemma |CMT_L10|. *T*)

Lemma CMT_L10 : (m:nat) (transient CMT 
  [s:st]((lt (s time) cmt) /\ (eq nat m (s time)))).

Intros.
Apply transient_implication with p:=[s:st]
                                       ~(common (s time))
                                       /\(eq nat m (s time)).
Apply CMT_L9.
Unfold everywhere s_imp.
Intros.
Elim H.
Clear  H.
Intros.
Split.
Unfold not.
Intros.
Generalize (cmt_smallest (s time) H1).
Intros.
Generalize (le_lt_trans cmt (s time) cmt H2 H).
Intros.
Apply (lt_n_n cmt H3).
Auto with v62.
Qed.

(*T* Another application of |transient_implication| together with some
case analysis on |time| finally yields |CMT_L11|, which is exactly what
we need for the proof of Lemma |CMT_L12|. *T*)

Lemma CMT_L11 : (m:nat)(transient CMT
   (s_and (s_and [s:st](le (s time) cmt) 
                 [s:st](eq nat m (s time)))
     (s_not
       (s_or
         (s_and [s:st](le (s time) cmt) 
                [s:st](lt m (s time)))
         [s:st](eq nat (s time) cmt))))).

Intros.
Apply transient_implication with p:=[s:st]
                                       (lt (s time) cmt)
                                       /\(eq nat m (s time)).
Apply CMT_L10.
Unfold everywhere s_imp s_and s_or s_not.
Intros.
Elim H.
Clear  H.
Intros.
Elim H.
Clear  H.
Intros.
Split.
Elim (eq_nat_dec (s time) cmt).
Intros.
Elim H0.
Right.
Auto with v62.
Intros.
Elim (le_lt_or_eq (s time) cmt H).
Intros.
Auto with v62.
Intros.
Elim y.
Auto with v62.
Auto with v62.
Qed.

(*T* Now we can combine safety (Lemma |CMT_S8|) and liveness (Lemma
|CMT_L11|) assertions to obtain the |ensures| assertion that can be
directly used to prove the following Lemma via |leads_to_basis| (see
the inductive definition of |leads_to|). *T*)

Lemma CMT_L12 : (m:nat)
  (leads_to CMT
    (s_and [s:st](le (s time) cmt) 
           [s:st](eq nat m (variant s)))
    (s_or
      (s_and [s:st](le (s time) cmt) 
             [s:st](lt m (variant s)))
      [s:st](eq nat (s time) cmt))).

Intros.
Unfold variant.
Apply leads_to_basis.
Unfold ensures.
Split.
Apply CMT_S8.
Apply CMT_L11.
Qed.

(*T* Finally, we can prove |CMT_L13| using the reverse induction rule
|leads_to_| \linebreak |rev_nat_induction|. We instantiate |maximum|
by |cmt|, and |variant| by |variant| as defined above. The |leads_to|
premise is exactly |CMT_L12|. Lemma |CMT_L13| states that if |time| is
not beyond the smallest meeting time |cmt|, then it will reach |cmt|
sometime in the future. *T*)

Lemma CMT_L13 : (leads_to CMT 
  ([s:st](le (s time) cmt)) 
  ([s:st](eq nat (s time) cmt))).

Apply (leads_to_rev_nat_induction CMT variant cmt).
Unfold variant.
Apply s_imp_p_p.
Intros.
Apply CMT_L12.
Qed.

(*T* Of course, this left hand side of |leads_to| covers specifically
the initialization condition of our original program.  So, we obtain 
our final liveness result |CMT_L14| by weakening the left hand side
using |leads_to_implication|. *T*)

Theorem CMT_L14 : (leads_to CMT 
  ([s:st](eq nat (s time) O)) 
  ([s:st](eq nat (s time) cmt))).

Apply (leads_to_implication_l CMT [s:st](eq nat (s time) O)
        [s:st](le (s time) cmt) [s:st](eq nat (s time) cmt)).
Unfold everywhere s_imp.
Intros.
Rewrite -> H.
Apply le_O_n.
Apply CMT_L13.
Qed.

(*T* Together, the theorems |CMT_S5|, |CMT_S6|, and |CMT_L14| prove
total correctness of the program as formulated in informal
specification. *T*)