(*T* \usection{Operations on States and Variables}\label{sect-states} *T*)

(*T* Assuming a state space with typed variables as introduced in the
previous section, the module |var_state_ops| to be disscussed below
introduces extensional equality on states and provides an assignment
operation to modify typed variables in a given state. While the
definition of such an operation in set theory is straightforward, this
is not the case in a framework with static types such as CIC. *T*)

(*T* Equality of states is extensional, i.e. it can be reduced to
equality of the associated values for all variables.  The proposition
|(val_eq n x n' x')| defined below means that the value |x| of type
|n| is equal to the value |x'| of type |n'|. Its definition uses
dependent equality |eqT_dep| from the module |EqdepT|, which is also
used in the proofs of the subsequent theorems.\footnote{One should be
aware of the fact that the dependent equality module |EqdepT| is not a
conservative extension of CIC.} *T*)

Definition val_eq :=
  [n:type_name][x:(type n)][n':type_name][x':(type n')]
  (eqT_dep type_name type n x n' x').

(*T* Obviously, the types of |x| and |x'| which will be extracted from
variables, say |v| and |v'|, will depend on the types associated to
|v| and |v'|, respectively. That both of these types will always be
logically equal in a term |(val_eq n x n' x')| is not visible to the
typechecker, which can only check computational equality. Hence,
instead of the standard polymorphic equality |==|, which requires that
the argument types are computationally equal, we use the more flexible
dependent equality |eqT_dep|, which only requires logical equality.
*T*)

(*T* Of course, standard equality implies value equality, since
dependent equality |eqT_dep| is (inductively) defined to be reflexive,
if both sides are instantiated by the same type. *T*)

Theorem eq_imp_val_eq:(n:type_name)
  (x,y:(type n))(x==y)->(val_eq n x n y).

Induction 1.
Unfold val_eq.
Constructor 1.
Qed.

(*T* The theorem |val_eq_imp_eq| is the converse of the previous
implication. It corresponds to a lemma |eqT_dep_eq| from
the module |EqdepT| specialized to our setting. *T*)

Theorem val_eq_imp_eq:(n:type_name)
  (x,y:(type n))(val_eq n x n y)->(x==y).

Unfold val_eq.
Exact (eqT_dep_eq type_name type).
Qed.

(*T* In the presence of an equality of type names |n| and |n'| it
should be possible to cast an element |x| of |n| to an equal element
of |n'|. This is achieved by |(cast n n' e x)| which converts a value
|x| of type |n| to a value of type |n'| given an equality proof
|e:n==n'|. In fact, |cast| is a particular instance of |eqT_rec|
as introduced in Section \ref{sect-init}. *T*)

Definition cast := [n,n':type_name][e:(n==n')][x:(type n)]
  (eqT_rec type_name n type x n' e).

(*T* By instantiating a general axiom |eq_rec_eq| from the module
|EqdepT| we obtain the theorem |cast_thm|, stating that type casting
between identical types does not change the value. *T*)

Theorem cast_thm : (n:type_name)(e:(n==n))(x:(type n))
  ((cast n n e x)==x).

Intros.
Unfold cast.
Symmetry.
Apply eqT_rec_eq.
Qed.

(*BEGIN-H*)

Lemma eq_lemma : 
  (T:Type)(P:T->T->Prop)((x:T)(P x x))->((x,y:T)(x==y)->(P x y)).

Intros.
Rewrite -> H0.
Apply H.
Qed.

(*END-H*)

(*T* We also prove the following theorem stating that type casting
between equal types |n| and |n'| respects value equality. *T*)
  
Theorem cast_resp_eq:(n,n':type_name)(x:(type n))(e:(n==n'))
    (val_eq n' (cast n n' e x) n x).

Cut (n,n':type_name)
     (e:n==n')(x:(type n))(val_eq n' (cast n n' e x) n x).
Intro.
Intros.
Apply H.
Generalize (eq_lemma type_name
             [n,n':type_name]
              (e:n==n')(x:(type n))(val_eq n' (cast n n' e x) n x)).
Intros.
Apply H.
Intros.
Rewrite -> cast_thm.
Constructor 1.
Assumption.
Qed.

(*T* After these preparations we come to the main part of this module.
First of all we assume extensionality for states |st|, i.e. two states
are identified if their values coincide at all
variables.\footnote{This nonconservative axiom could be avoided by
defining an appropriate equivalence on |st|, or more generally by
equipping |st| with a categorical structure. This however would
complicate proofs and would require additional theorems stating that this
additional structure is respected by operations on states.} *T*)

Axiom st_extensionality : (s,s':st)
  ((v:var)((s v)==(s' v)))->(s==s').

(* A more abstract treatment of values and states which is not
realized in the present version of the library should allow an
arbitrary equivalence on subsets of values to admit variable types
which are (subsets of) inductive data types with additional equations,
e.g. multisets. Then this (dependent) equivalence on values should be
lifted to an equivalence on states. A type theory with subtypes and
quotient types would support this directly.  An alternative for CIC
(or type theories with $\Sigma$-types in general) is to use setoids,
i.e. types equipped with a (partial) equivalence relations. *)

(*T* The next lemma expresses the fact that equal variables have equal
types. In spite of its triviality we name it explicitly in order to
use it below. *T*)

Lemma var_eq_to_type_name_eq : (v,v':var)
  (v==v')->(var_type_name v)==(var_type_name v').

Intros.
Rewrite -> H.
Reflexivity.
Qed.

(*T* Below the assignment operation is introduced as the only
operation that can modify a state.  Given a state |s|, a variable |v|
and a new value |x| compatible with the type of |v|, the term 
|(assign s v x)| denotes the new state obtained from |s| by assigning the value
of |x| to |v|. *T*)

Definition assign := [s:st][v:var][x:(var_type v)]
  [v':var] <var_type v'>Case (var_eq_dec v v') of 
  (*v==v'*) [p:(v==v')] (cast (var_type_name v) (var_type_name v') 
                              (var_eq_to_type_name_eq v v' p) x) 
  (*~(v==v')*) [_](s v')
  end.  

(*T* Observe that the operation |var_eq_dec| deciding equality of
variables and the type casting operation |cast| are used in an
essential way to make |assign| properly typed. As explained above,
|cast| needs an equality proof for the types involved as a
justification for type casting. This equality proof is obtained by
applying the previous lemma |var_eq_to_type_name_eq| to the equality
proof on variables |p:(v==v')| provided by |(var_eq_dec v v')|. *T*)

(*T* The remaining theorems of this module are basic properties of the
assignment operation, which are needed for most applications. The
extensionality axiom |st_extensionality| is a major ingredient of
their proofs. *T*)

(*T* The first theorem states that assigning the contents of a
variable to itself does not change the state.  *T*)

Theorem assign_unchanged : (s:st)(v:var)
  ((assign s v (s v))==s).

Intros.
Apply st_extensionality.
Intros v'.
Unfold assign.
Elim (var_eq_dec v v').
Intros H.
Apply (val_eq_imp_eq (var_type_name v')).
Pattern 4 5 v' .
Rewrite <- H.
Apply cast_resp_eq.
Intro.
Reflexivity.
Qed.


(*T* The next theorem states that a variable |v| which has just
received the value |x| by assignment will contain that value |x|. *T*)

Theorem assign_changed : (s:st)(v:var)(x:(var_type v))
  (((assign s v x) v)==x).

Unfold assign.
Intros.
Elim (var_eq_dec v v).
Intros H.
Apply (cast_thm (var_type_name v)).
Intro.
Unfold not in y.
Apply False_ind.
Apply y.
Reflexivity.
Qed.

(*T* On the other hand, modifying a variable |v| does not change the
value of any variable |v'| distinct from |v|. *T*)

Theorem assign_indep : (s:st)(v,v':var)(x:(var_type v)) ~(v==v')->
  ((assign s v x) v')==(s v').

Intros.
Unfold assign.
Elim (var_eq_dec v v').
Intros H1.
Apply False_ind.
Apply (H H1).
Intro.
Reflexivity.
Qed.

(*T* After repeated assignment of a value to a variable |v| the
contents of |v| is the value of the last assignment. *T*)

Theorem assign_twice : (s:st)(v:var)(x,y:(var_type v))
  (assign (assign s v x) v y)==(assign s v y).

Intros.
Apply st_extensionality.
Intros v'.
Elim (var_eq_dec v v').
Intros H.
Rewrite <- H.
Rewrite -> assign_changed.
Rewrite -> assign_changed.
Reflexivity.
Intros H.
Rewrite -> assign_indep.
Rewrite -> assign_indep.
Rewrite -> assign_indep.
Reflexivity.
Assumption.
Assumption.
Assumption.
Qed.

(*T* And finally we prove that the order of assigning values to two
distinct variables does not matter. In such a situation the two
assignments commute. *T*)

Theorem assign_commutes : (s:st)
  (v,v':var)(x:(var_type v))(y:(var_type v')) ~(v==v')->
  (assign (assign s v x) v' y)==(assign (assign s v' y) v x).

Intros.
Apply st_extensionality.
Intros v''.
Elim (var_eq_dec v' v'').
Intros H1.
Rewrite <- H1.
Rewrite -> assign_changed.
Rewrite -> assign_indep.
Rewrite -> assign_changed.
Reflexivity.
Assumption.
Intro.
Rewrite -> assign_indep.
Elim (var_eq_dec v v'').
Intro.
Rewrite <- y1.
Rewrite -> assign_changed.
Rewrite -> assign_changed.
Reflexivity.
Intro.
Rewrite -> assign_indep.
Rewrite -> assign_indep.
Rewrite -> assign_indep.
Reflexivity.
Assumption.
Assumption.
Assumption.
Assumption.
Qed.