(*T* \usection{State Predicates and Variables} *T*)

(*T* Again assuming an underlying state space with typed variables,
this section presents the module |var_state_pred|. This module formalizes
dependence and independence of state predicates on variables and
introduces a (semantical) notion of variable substitution in state
predicates. These concepts are needed to express some proof rules that
make explicit use of variables, an example being the elimination
theorem of New UNITY \cite{Misra94,Misra95} which is the subject of
Section \ref{sect-elim}. *T*)

(*T* First, we introduce some technical tools for reasoning
inductively about system variables. In order to refer to variables in
a uniform way, independently of the set of variables of a
concrete system, we use the enumeration |ith_var| of variables
declared in |abstract|.  The next theorem allows us to infer that a
property holds for all variables if it holds for all variables up to
the maximum index |vars|.  Subsequently this theorem will be useful to
prove properties of all variables by induction over natural
numbers. *T*)

Theorem var_index_thm : (P:var->Prop)
  ((i:nat)(lt i vars)->(P (ith_var i)))->(v:var)(P v).

Intros.
Generalize (var_finite v).
Intro.
Elim H0.
Intros i H1.
Elim H1.
Intros.
Rewrite <- H3.
Apply H.
Assumption.
Qed.

(*T* The following auxiliary operation is used to merge two states in
the following sense: Given an index |n| and states |s| and |s'| the
term |(equalize_vars n s| \linebreak |s')| returns a new state which is
equal to |s| with the exception that the contents of all variables
up to index |n| is copied from |s'| to |s|. *T*)

Fixpoint equalize_vars [n:nat] : st->st->st :=
  [s,s':st] Case n of 
    (* O *) s 
    (* (S p) *) [p:nat] (assign (equalize_vars p s s') 
                                  (ith_var p) (s' (ith_var p)))
  end.

Lemma equalize_lemma : (s,s':st)(n:nat)(i:nat)(lt i n)->
((equalize_vars n s s') (ith_var i))==(s' (ith_var i)).

Intros s s'.
Induction n.
Intros.
Apply False_ind.
Apply (lt_n_O i H).
Intros.
Simpl.
Generalize (lt_n_Sm_le i n0 H0).
Intro.
Generalize (le_lt_or_eq i n0 H1).
Intro.
Elim H2.
Intro.
Elim (var_eq_dec (ith_var n0) (ith_var i)).
Intros H4.
Rewrite -> H4.
Rewrite -> assign_changed.
Reflexivity.
Intro.
Rewrite -> assign_indep.
Apply H.
Assumption.
Assumption.
Intro.
Rewrite <- H3.
Rewrite -> assign_changed.
Reflexivity.
Qed.

(*T* The operation |equalize_vars| applied to the number of relevant
variable indices |vars| allows to copy a state in a stepwise fashion
that is suitable for inductive proofs as we will see below.  *T*)

Theorem equalize_vars_char : (s,s':st) 
  (equalize_vars vars s s')==s'.

Intros.
Apply st_extensionality.
Intro.
Apply (var_index_thm
        [v:var](equalize_vars vars s s' v)==(s' v)).
Intros i H.
Apply equalize_lemma.
Assumption.
Qed.

(*T* Temporal proof rules sometimes require preconditions stating the
independence of certain state predicates from particular variables. To
express a such conditions the following definition of independence
will be useful. Given a state predicate |p| and a variable |v|,
|(independent p v)| states that |p| does not depend on |v|. *T*)

Definition independent := [p:s_prop][v:var]
  (s:st)(x,y:(var_type v)) 
  (p (assign s v x)) -> (p (assign s v y)).

(*T* An immediate consequence of this definition is that if |p| is
independent of |v| then the fact that |p| holds at |s| is preserved
under arbitrary modifications of |s| at |v|. *T*)

Theorem  independent_imp : (p:s_prop)(v:var)
  (independent p v)->
  (s:st)(p s)->(x:(var_type v))(p (assign s v x)).

Intros.
Unfold independent in H.
Apply (H s (s v) x).
Rewrite -> assign_unchanged.
Assumption.
Qed.

(*T* Using induction over |nat| and the previous theorem we can prove
a technical lemma: If a state predicate |p| is independent of all
variables (up to some index) and |p| holds at some state |s| we can
modify all these variables, here by using their values from another
state |s'|, without changing the validity of |p|. *T*)

Lemma independent_and_equalize : (p:s_prop)
  ((v:var) (independent p v))->
  (s,s':st)(i:nat)(le i vars)->
  (p s)->(p (equalize_vars i s s')).

Intros p H s s'.
Induction i.
Intros.
Simpl.
Assumption.
Intros.
Simpl.
Generalize (H (ith_var n)).
Intro.
Generalize (independent_imp p (ith_var n) H3).
Intro.
Apply H4.
Apply H0.
Apply le_trans with (S n).
Apply le_n_Sn.
Assumption.
Assumption.
Qed.

(*T* Using this lemma it is easy to prove that if a state predicate is
independent of each variable then it does not depend on the state at
all. *T*)

Theorem fully_independent : (p:s_prop)
  ((v:var)(independent p v))->(s,s':st)(p s)->(p s').

Intros.
Rewrite <- (equalize_vars_char s s').
Apply independent_and_equalize.
Assumption.
Apply le_n.
Assumption.
Qed.

(*T* In addition to the capability of expressing independence we would
also like to express preconditions stating that a predicate may depend
on a particular variable but definitely does not depend on further
ones. This is achieved by |(may_depend_on p v)| given a state
predicate |p| and a variable |v|. *T*)

Definition may_depend_on := [p:s_prop][v:var]
  (m:(var_type v))(s,s':st) 
  (p (assign s v m))->(p (assign s' v m)).


(*BEGIN-H*)

Lemma make_independent : (p:s_prop)(v:var)(m:(var_type v))
  (independent [s:st](p (assign s v m)) v).

Intros.
Unfold independent.
Intros s x y.
Rewrite -> assign_twice.
Rewrite -> assign_twice.
Intro.
Assumption.
Qed.

(*END-H*)

(*T* The obvious relation between |independent| and
|may_depend_on| is verified in the following theorem. It |p| is
independent of all variables except for |v'| it follows that |p| may
only depend on |v'|. Observe that this does not exclude the case in which |p| is
independent of |v'|. *T*)

Theorem dependent : (v':var)(p:s_prop)
  ((v:var)~(v==v')->(independent p v)) -> (may_depend_on p v').

Intros.
Unfold may_depend_on.
Intros.
Generalize (fully_independent [s:st](p (assign s v' m))).
Intro.
Apply H1 with s:=s.
Intro.
Elim (var_eq_dec v v').
Intros H2.
Rewrite -> H2.
Apply make_independent.
Intro.
Generalize (H v y).
Intro.
Unfold independent.
Unfold independent in H2.
Intros s'' x0 y0.
Rewrite -> assign_commutes.
Pattern (assign (assign s'' v y0) v' m) .
Rewrite -> assign_commutes.
Intro.
Apply (H2 (assign s'' v' m) x0 y0).
Assumption.
Assumption.
Assumption.
Assumption.
Qed.

(*T* Given a predicate |p| there is a natural way to define a new
predicate independent of an arbitrary variable |v|. The new predicate
|[s:st](p (assign s v m))| behaves as |p|, except for the fact that it
does not use the contents of |v| but a constant |m| instead. We denote
this predicate by |(subst p v m)|, since it can be seen as a semantic
counterpart of variable substitution. *T*)

Definition subst := [p:s_prop][v:var][m:(var_type v)]
  [s:st](p (assign s v m)).  

(*T* Obviously, |(subst p v m)| is independent of |v|, and 
independence is preserved by |subst|. *T*)

Theorem indep_subst : (p:s_prop)(v:var)(m:(var_type v))
  (independent (subst p v m) v).

Intros.
Unfold subst.
Apply make_independent.
Qed.

Theorem indep_imp_indep_subst : (p:s_prop)
  (v,v':var)(m:(var_type v))
  (independent p v')->(independent (subst p v m) v').

Intros.
Unfold subst.
Unfold independent.
Unfold independent in H.
Intros s.
Elim (var_eq_dec v v').
Intros H1.
Rewrite <- H1.
Intros x y.
Rewrite -> assign_twice.
Rewrite -> assign_twice.
Intro.
Assumption.
Intros H1 x y.
Rewrite -> assign_commutes.
Pattern (assign (assign s v' y) v m) .
Rewrite -> assign_commutes.
Intro.
Apply (H (assign s v m) x y).
Assumption.
Unfold not.
Intro.
Rewrite H0 in H1.
Apply H1.
Reflexivity.
Unfold not.
Intro.
Rewrite H0 in H1.
Apply H1.
Reflexivity.
Qed.