(*T* \usection{Elimination Theorem}\label{sect-elim} *T*)

(*T* As an application of the state space with typed variables and its
supporting modules |var_state_ops| and |var_state_pred| we present a
formalization of the elimination theorem. This theorem has been
introduced in the context of New UNITY in \cite{Misra94,Misra95}, but
we give it here in the more general setting of transition systems.
The elimination theorem will be used in the example of Section
\ref{chap-example} for the verification of safety properties. *T*)

(*T* In fact, we have chosen the elimination theorem as an example of
a generic proof rule which can be used e.g. for arbitrary
programs. Formalizing such proof rules and reasoning about them
becomes possible inside CIC, since the notion of an abstract state
space with typed variables can be expressed inside the logic as
explained before. *T*)

(*T* We need two lemmas for the proof of the elimination theorem. The
first one essentially states that substituting |v| in |p| by its own
value |(s v)==m| yields a predicate equivalent to |p|. Notice the use
of the existential quantifier |s_ex| to introduce an auxiliary
variable |m| local to the expression. *T*)

Lemma elimination_1 : (v:var)(p:s_prop)(everywhere 
  (s_iff 
    (s_ex (var_type v) 
      ([m:(var_type v)](s_and (subst p v m) [s:st](s v)==m))) 
    p)).

Intros.
Unfold everywhere s_iff.
Intros.
Unfold s_ex.
Split.
Intro.
Elim H.
Intros m.
Intro.
Unfold s_and in H0.
Elim H0.
Intros.
Unfold subst in H1.
Rewrite <- H2 in H1.
Generalize (assign_unchanged s v).
Intro.
Rewrite H3 in H1.
Assumption.
Intro.
Exists  (s v).
Split.
Unfold subst.
Rewrite -> (assign_unchanged s v).
Assumption.
Reflexivity.
Qed.

(*T* The second lemma will be proved using the following theorem,
which is be useful in its own right: If a predicate |p| is independent
of all variables then it must be stable. *T*)

Theorem indep_imp_stable : (E:view)(p:s_prop)
  ((v':var)(independent p v'))->(stable E p).

Intros.
Unfold stable.
Apply sc_co.
Intros.
Apply fully_independent with p:=p s:=s.
Assumption.
Assumption.
Qed.

(*T* The second lemma states: Given a predicate |p| which may depend
only on a variable |v|, the predicate |(subst p v m)| substituting any
constant |m| for |v| is stable. The proof involves
|indep_imp_stable| and |indep_imp_indep_subst|. *T*)


Lemma elimination_2 : (E:view)(v:var)(p:s_prop)
  ((v':var)~(v'==v)->(independent p v')) ->
  (m:(var_type v))(stable E (subst p v m)).

Intros.
Apply indep_imp_stable.
Intro.
Elim (var_eq_dec v' v).
Intros H1.
Rewrite -> H1.
Apply indep_subst.
Intros H1.
Generalize (H v' H1).
Intro.
Apply indep_imp_indep_subst.
Assumption.
Qed.

(*T* Now we are prepared to prove the elimination theorem. First we
convey the intuitive idea: Assume that we have a predicate |p| which
depends on no other variable than |v|. We would like to conclude that
if |p| holds at some state, then at each successor state there is some
|m| such that |(subst p v m)|, meaning that |p| holds with |m|
substituted for |v|. So far this simply states that if |p| was true in
the past there must have been some value |m| for |v| when |p| was
true.  Notice, however, that we do not know anything else about |m|.
Now assume we have the additional information that when the variable
|v| contains |m| then the predicate |(q m)| holds in the next state. Then
we can strengthen our conclusion: If |p| holds at some state then at
each successor state there is some |m| such that |(subst p v m)| and
also |(q m)| holds. *T*)

Theorem elimination : 
  (E:view)(v:var)(p:s_prop)(q:(var_type v)->s_prop)
  ((v':var)~(v'==v)->(independent p v')) ->
  ((m:(var_type v))(co E [s:st]((s v)==m) (q m))) ->
  (co E p (s_ex ? [m:(var_type v)]
                     (s_and (subst p v m) (q m)))).

Intros.
Cut (m:(var_type v))
     (co E (s_and (subst p v m) [s:st](s v)==m)
       (s_and (subst p v m) (q m))).
Intro.
Apply co_implication_l with (s_ex ?
                                [m:(var_type v)]
                                 (s_and (subst p v m) [s:st](s v)==m)).
Apply s_iff_imp.
Apply s_iff_sym.
Apply elimination_1.
Apply co_big_disjunction.
Assumption.
Intro.
Apply co_conjunction.
Change (stable E (subst p v m)).
Apply elimination_2.
Assumption.
Apply H0.
Qed.

(*T* The proof uses |co_big_disjunction|, |co_conjunction| and the
previous two lemmas. *T*)