(*T* \usection{Safety Assertions}\label{sect-safety} *T*)

(*T* The module |safety| contains the definitions of the temporal
logic operators |co|, |unless|, |stable|, |invariant| and |invariant|
for safety assertions.  As explained before, we follow the New UNITY
approach \cite{Misra94}, where |co| is chosen as the basic safety
operator and the other operators are defined on top of it. This is not
a major deviation from \cite{ChandyMisra88} but rather a more
systematic way to structure the definitions. *T*)

(*T* We start with the definition of the |co| operator. Recall that
for two predicates |p| and |q| the assertion |(co E p q)| means that
if |p| holds at some state then |q| holds at each possible successor
state in |E| no matter which action occurs. *T*)

Definition hoare := [e:act][p,q:s_prop]
  ((s,s':st)(trans e s s')->(p s)->(q s')).

Definition co := [E:view][p,q:s_prop]
  (e:act)(In act E e)->(hoare e p q).

(*BEGIN-H*)

Theorem nc_co : (E:view)(p,q:s_prop)
  (co E p q) ->
  ((e:act)(s,s':st)(In act E e)->(trans e s s')->
      (p s)->(q s')).

Unfold co.
Unfold hoare.
Auto.
Intros E p q.
Intro.
Intros.
Apply (H e H0 s s' H1 H2).
Qed.

Theorem sc_co : (E:view)(p,q:s_prop)
  ((e:act)(s,s':st)(In act E e)->(trans e s s')->
    (p s)->(q s'))->
  (co E p q).

Unfold co.
Unfold hoare.
Intros.
Apply (H e s s' H0 H1 H2).
Qed.
(*END-H*)

(*T* Subsequently, we define further operators in terms of |co|.
Notice that all operators are relative to a view |E| specified as the
first argument. The other arguments of the temporal operators are
state predicates, usually denoted by |p|, |q| and |r|. *T*)

(*T* Remember that the assertion |(unless E p q)| states that in |E|,
|p| holds unless |q| holds, or more precisely, if |p| holds at some
state and |q| does not hold then at the next step |p| remains true or
|q| becomes true. It is important to see that progress does not have
to take place, i.e. the assertion does not exclude the possibility
that |p| remains true forever and |q| never holds. *T*)

Definition unless := [E:view][p,q:s_prop] 
  (co E (s_and p (s_not q)) (s_or p q)).

(*T* The assertion |(stable E p)| asserts that |p| is stable, i.e.
once |p| becomes true in |E| it continues to hold. *T*)

Definition stable := [E:view][p:s_prop] (co E p p).

(*T* The stronger assertion |(ind_invariant E IC p)| states that |p|
is an inductive invariant in |E| w.r.t. an initialization condition |IC|. In
addition to stability of |p| it is required that |p| is implied by the
|IC|.  *T*)

Definition ind_invariant := 
  [E:view][IC:s_prop][p:s_prop] 
  (everywhere (s_imp IC p)) /\ (stable E p).

(*T* We also introduce assertions of the form |(invariant E IC p)|
which state that |p| is implied by some inductive invariant
in |E| w.r.t. an initialization condition |IC|. *T*)

Definition invariant := 
  [E:view][IC:s_prop][p:s_prop]
  (ExT [inv:s_prop] (ind_invariant E IC inv) /\
                    (everywhere (s_imp inv p))).

(*T* Finally, we have the state predicate |(si E IC)|, called
the strongest invariant \cite{Lamport90}, which characterizes
the set of reachable states.  *T*)

Definition si := 
  [E:view][IC:s_prop][s:st]
  (p:s_prop)(ind_invariant E IC p)->(p s).

(*T* This concludes the list of temporal operators used to formulate
safety assertions. The remainder of this module proves a variety of
theorems about these operators and their mutual relationship.  Most
proof rules contained in \cite{ChandyMisra88} are among these
theorems. Also many proof rules for |co| are proved here, among them
also rules given in \cite{Misra94}. *T*)

(*T* We start with a combined left hand side strengthening and 
right hand side weakening rule for |co| assertions.  *T*)

(*BEGIN-H*)
Theorem hoare_implication : (e:act)(p,p',q,q':s_prop)
  (everywhere (s_imp p p')) ->
  (everywhere (s_imp q q')) ->
  (hoare e p' q) -> (hoare e p q').

Unfold everywhere s_imp.
Unfold hoare.
Intros.
Apply H0.
Apply (H1 s s' H2).
Apply H.
Trivial.
Qed.
(*END-H*)

Theorem co_implication : (E:view)(p,p',q,q':s_prop)
  (everywhere (s_imp p p')) ->
  (everywhere (s_imp q q')) ->
  (co E p' q) -> (co E p q').

Unfold co.
Intros.
Apply hoare_implication with 1:=H 2:=H0.
Apply H1.
Trivial.
Qed.

(*BEGIN-H*)

Theorem hoare_implication_r : (e:act)(p,q,r:s_prop)
  (everywhere (s_imp q r)) ->
  (hoare e p q) -> (hoare e p r).

Intros.
Apply (hoare_implication e p p q r).
Apply s_imp_p_p.
Assumption.
Assumption.
Qed.

Theorem co_implication_r : (E:view)(p,q,r:s_prop)
  (everywhere (s_imp q r)) ->
  (co E p q) -> (co E p r).

Intros.
Apply (co_implication E p p q r).
Apply s_imp_p_p.
Assumption.
Assumption.
Qed.

Theorem hoare_implication_l : (e:act)(p,q,r:s_prop)
  (everywhere (s_imp p q)) ->
  (hoare e q r) -> (hoare e p r).

Intros.
Apply (hoare_implication e p q r r).
Assumption.
Apply s_imp_p_p.
Assumption.
Qed.

Theorem co_implication_l : (E:view)(p,q,r:s_prop)
  (everywhere (s_imp p q)) ->
  (co E q r) -> (co E p r).

Intros.
Apply (co_implication E p q r r).
Assumption.
Apply s_imp_p_p.
Assumption.
Qed.

(*END-H*)

(*BEGIN-H*)

Theorem co_subst_r : (E:view)(p,q,q':s_prop)
  (everywhere (s_iff q q'))->(co E p q)->(co E p q').

Intros.
Apply co_implication_r with q:=q.
Red.
Red in H.
Intros.
Specialize (H s).
Intros.
Unfold s_imp.
Unfold s_iff in H1.
Elim H1.
Intros H2 H3.
Exact H2.
Exact H0.
Qed.

Theorem co_subst_l : (E:view)(p,p',q:s_prop)
  (everywhere (s_iff p p'))->(co E p q)->(co E p' q).

Intros.
EApply co_implication_l.
Unfold everywhere.
Unfold everywhere in H.
Unfold s_imp.
Unfold s_iff in H.
Intros.
Specialize (H s).
Intros.
Unfold iff in H2.
Elim H2.
Intros.
Apply H4.
Exact H1.
Exact H0.
Qed.

(* Such substitution rules express that within an assertion (here
|co|) it should be possible to substitute state predicates by
equivalent ones. Here state predicates are said to be equivalent iff
they are equivalent for all states. In an intensional type theory like
CIC logical equivalence does not imply equality in general. So
substitution theorems for logical equivalent formulas and state
predicates have to be proved explicitly as above. An alternative
solution is a non-conservative extension of CIC by adding logical
extensionality axioms. *)

(*END-H*)

(*T* Two |co| assertions can be combined into a new one by taking the
conjunction of their left hand sides and their right hand sides,
respectively. *T*)

(*BEGIN-H*)
Theorem hoare_conjunction : (e:act)(p,p',q,q':s_prop)
  (hoare e p q) -> (hoare e p' q') -> 
  (hoare e (s_and p p') (s_and q q')).

Unfold hoare.
Unfold s_and.
Intros.
Split.
Elim H2.
Intros.
Apply (H s s' H1 H3).

Elim H2.
Intros.
Trivial.
Apply (H0 s s' H1 H4).
Qed.
(*END-H*)

Theorem co_conjunction : (E:view)(p,p',q,q':s_prop)
  (co E p q) -> (co E p' q') -> 
  (co E (s_and p p') (s_and q q')).

Unfold co.
Intros.
Specialize (H e H1).
Intros.
Specialize (H0 e H1).
Intros.
Apply hoare_conjunction with 1:=H2 2:=H3.
Qed.

(*BEGIN-H*)

Theorem stable_subst : (E:view)(p,q:s_prop)
  (everywhere (s_iff p q)) ->
  (stable E p) -> (stable E q).

Unfold stable.
Intros.
Apply (co_implication E) with p':=p q:=p.
Apply s_iff_imp.
Apply s_iff_sym.
Auto.
Apply s_iff_imp.
Auto.
Auto.
Qed.

Theorem ind_invariant_subst : (E:view)(r,r',p,q:s_prop)
  (everywhere (s_imp r' r))->(everywhere (s_iff p q)) ->
  (ind_invariant E r p) -> (ind_invariant E r' q).

Unfold ind_invariant.
Intros.
Elim H1.
Clear H1.
Intros.
Split.
Unfold everywhere s_imp.
Unfold everywhere s_imp in H.
Unfold everywhere s_iff in H0.
Unfold everywhere s_imp in H1.
Intros.
Generalize (H0 s).
Intros.
Elim H4.
Intros.
Apply H5.
Apply H1.
Apply H.
Trivial.
Apply stable_subst with 1:=H0.
Trivial.
Qed.

(*END-H*)

(*T* The rule |co_conjunction| can be specialized for |stable| as
follows. *T*)

(*BEGIN-H*)
Theorem hoare_stable_conjunction : (E:view)(e:act)(In act E e)->
  (p,q,r:s_prop)
  (stable E r) -> (hoare e p q) -> 
  (hoare e (s_and p r) (s_and q r)).

Intros.
Apply (hoare_conjunction e p r q r).
Auto.
Unfold stable in H0.
Unfold co in H0.
Apply H0.
Trivial.
Qed.
(*END-H*)

Theorem co_stable_conjunction : (E:view)(p,q,r:s_prop)
  (stable E r) -> (co E p q) -> 
  (co E (s_and p r) (s_and q r)).

Intros.
Unfold stable in H.
Apply (co_conjunction E p r q r).
Auto.
Auto.
Qed.

(*T* The following rules are useful to derive {\em relativized
assertions}, i.e. assertions which do not make statements about all
states but only about a subset of states usually specified by some
inductive invariant. Formally, we conceive relativized assertions as
ordinary assertions with some additional restriction expressed by
conjunction.  For instance, |(co E (s_and r p) (s_and r q)| and
|(stable E (s_and r p))| are relativations of |(co E p q)| and
|(stable E p)| w.r.t.  some inductive invariant |r|, respectively. The
following two theorems show that, given a goal that is a relativized
assertion of one of these kinds, we can prove this goal by exploiting
|r| not only on the left hand side but also as an assumption on the
right hand side if we know at least that |r| is stable. *T*)

Theorem rel_co : (E:view)(p,q,r:s_prop)
  (stable E r)->(co E (s_and r p) (s_imp r q))->
  (co E (s_and r p) (s_and r q)).

Intros.
Generalize (co_stable_conjunction ? ? ? ? H H0).
Intros.
Clear H0.
Apply co_implication with 3:=H1.
Clear H H1.
Unfold everywhere s_imp s_and.
Tauto.
Unfold everywhere s_imp s_and.
Tauto.
Qed.

Theorem rel_stable : (E:view)(p,r:s_prop)
  (stable E r)->(co E (s_and r p) (s_imp r p))->
  (stable E (s_and r p)).

Intros.
Unfold stable.
Apply rel_co.
Trivial.
Apply co_implication_r with 2:=H0.
Clear H H0.
Unfold everywhere s_imp s_and.
Tauto.
Qed.

(*BEGIN-H*)
Theorem rel_hoare_dep : (E:view)(e:act)(In act E e)->
  (r:s_prop)(stable E r)->(p,q:(s:st)(r s)->Prop)
  (hoare e (ds_ex r p) (ds_all r q))->
  (hoare e (ds_ex r p) (ds_ex r q)).

Intros.
Generalize (hoare_stable_conjunction ? ? H ? ? ? H0 H1).
Intros.
Clear H0.
Apply hoare_implication with 3:=H2.
Clear H1 H2.
Unfold everywhere s_imp s_and.
Tauto.
Unfold everywhere s_imp s_and.
Clear H1 H2.
Intros.
Elim H0.
Clear H0.
Intros.
Split with H1.
Apply H0.
Qed.
(*END-H*)

(*T* Rules of this kind for other forms of relatived assertions will
be given later.  In general, such rules allow us to use a state
predicate |r|, which is typically an inductive invariant, as an
assumption on both sides of the underlying implication rather than
leading to proof obligation for |r| on the right hand side. The
purpose of these rules is similar to that of the substitution axiom
(cf. \cite{ChandyMisra88}), but allows us to use inductive invariants
as assumptions in a more disciplined way. Recall that the substitution
axiom allows us to use UNITY invariants everywhere, i.e. it assumes
that they are true in all states, which leads to the problems
discussed in Section \ref{section-unity}.  In fact, relativized
assertions as they are introduced in this chapter correspond closely
to the relativized assertions introduced in \cite{Sanders91} (and
corrected in \cite{Prasetya94}) as one solution to the dilemma posed by
the substitution axiom. However, instead of introducing new families
of temporal operators indexed by inductive invariants, we prefer to use
the original UNITY-style operators to express them. *T*)

(*T* We also have the following generalizations of the previous two
proof rules from state predicates to dependent state predicates |p|
and |q|.  Relativized assertions of the form |(co E (ds_ex r p) (ds_ex r q))| 
as in the conlusion of these rules are often needed if the
propositions |(p s)| and |(q s)| depend on the proof of |(r s)|.  We
first added dependent state predicates and corresponding relativized
assertions in order to cope with problems related to the static
character of the type theory.\footnote{in the context of formal
reasoning about Petri nets} A typical example would be the use of a
partial function which is only meaningful under the premise |(r s)|. 
In CIC such a function is naturally represented as a total
function that depends on a proof of |(r s)|.  More generally, we view
dependent state predicates as a solution to the difficulties arising
from the use of type theory rather than set-theory for formal
program/system verification (cf. \cite{LamportPaulson97}). Such
generalized proof rules for relativized assertions can be proved for
all temporal operators, but for the sake of brevity we only state
them here. *T*)

Theorem rel_co_dep : (E:view)(r:s_prop)
  (stable E r)->(p,q:(s:st)(r s)->Prop)
  (co E (ds_ex r p) (ds_all r q))->
  (co E (ds_ex r p) (ds_ex r q)).

Intros.
Generalize (co_stable_conjunction ? ? ? ? H H0).
Intros.
Clear H0.
Apply co_implication with 3:=H1.
Clear H H1.
Unfold everywhere s_imp s_and.
Tauto.
Unfold everywhere s_imp s_and.
Clear H1.
Intros.
Elim H0.
Clear H0.
Intros.
Split with H1.
Apply H0.
Qed.


Theorem rel_stable_dep : (E:view)(r:s_prop)
  (stable E r)->(p:(s:st)(r s)->Prop)
  (co E (ds_ex r p) (ds_all r p))->
  (stable E (ds_ex r p)).

Intros.
Unfold stable.
Apply rel_co_dep.
Trivial.
Apply co_implication_r with 2:=H0.
Clear H H0.
Unfold everywhere s_imp s_and.
Tauto.
Qed.

(*T* For assertions involving dependent state predicates we often have
rules to strengthen the condition the predicates depends on such as
the following: *T*)

Theorem rel_co_dep_strengthen : (E:view)(r,r':s_prop)
  (stable E r)->
  (ev:(everywhere (s_imp r r')))
  (p,q:(s:st)(r' s)->Prop)
  (co E (ds_ex r' p)
        (ds_ex r' q))->
  (co E (ds_ex r [s:st][prf:(r s)](p s (ev s prf))) 
        (ds_ex r [s:st][prf:(r s)](q s (ev s prf)))).

Unfold stable everywhere co ds_ex.
Unfold hoare.
Intros.
Elim H3.
Intros.
Split with (H e H1 s s' H2 x).
Generalize (H0 e H1 s s' H2).
Intros.
Cut (EXT prf:(r' s) | (p s prf)).
Intros.
Generalize (H5 H6).
Intros.
Elim H7.
Intros.
Rewrite (proof_irrelevance ? (ev s' (H e H1 s s' H2 x)) x0).
Trivial.

Elim H3.
Intros.
Split with (ev s x).
Rewrite (proof_irrelevance ? (ev s x) (ev s x0)).
Trivial.
Qed.


Theorem rel_stable_dep_strengthen : (E:view)(r,r':s_prop)
  (stable E r)->
  (ev:(everywhere (s_imp r r')))
  (p:(s:st)(r' s)->Prop)
  (stable E (ds_ex r' p))->
  (stable E (ds_ex r [s:st][prf:(r s)](p s (ev s prf)))).

Intros.
Unfold stable.
Apply (rel_co_dep_strengthen E r r' H ev).
Exact H0.
Qed.


(*T* Above we have introduced the strongest invariant |(si E IC)|,
which is a state predicate characterizing the set of states reachable
from some state statisfying |IC|. It is interesting to note that the
use of |si| makes it unecessary to deal with reachable states
directly, just as there will be no need to assume and formalize a
particular execution semantics. In the following some basic facts
about the relationship between |si|, |ind_inv| and |invariant| will be
given. *T*)

Theorem ind_inv_is_inv : (E:view)(IC:s_prop)(p:s_prop)
  (ind_invariant E IC p)->(invariant E IC p).

Intros.
Unfold invariant.
Split with p.
Split.
Trivial.
Unfold everywhere s_imp.
Auto.
Qed.

Theorem si_is_indinv : (E:view)(IC:s_prop)
  (ind_invariant E IC (si E IC)).

Unfold si.
Intros.
Unfold ind_invariant.
Split.
Unfold everywhere s_imp.
Intros.
Elim H0.
Intros.
Apply H1.
Trivial.

Unfold stable everywhere s_imp.
Apply sc_co.
Intros.
Generalize (H1 p).
Clear H1.
Intros.
Cut (p s).
Intros.
Elim H2.
Intros.
Generalize (nc_co ? ? ? H5).
Intros.
Apply H6 with 1:=H 2:=H0 3:=H3.

Apply H1.
Trivial.
Qed.

Theorem si_is_inv : (E:view)(IC:s_prop)
  (invariant E IC (si E IC)).

Intros.
Unfold invariant.
Split with (si E IC).
Split.
Apply si_is_indinv.
Unfold everywhere s_imp.
Tauto.
Qed.

Theorem indinv_imp_si : (E:view)(IC:s_prop)(p:s_prop)
  (ind_invariant E IC p)->
  (everywhere (s_imp (si E IC) p)).

Unfold everywhere s_imp si.
Intros.
Apply H0.
Apply ind_invariant_subst with 3:=H.
Unfold everywhere s_imp.
Auto.
Unfold everywhere s_iff.
Clear H H0.
Tauto.
Qed.

(*T* The next two results together provide a
characterization of |invariant| in terms of the strongest invariant
given by |si|. Since, |(si E IC)| characterizes
the set of states reachable w.r.t. |IC| in |E|, the result says that 
|(invariant E IC p)| holds iff |p| is true at all 
such reachable states. *T*)

Theorem inv_imp_si : (E:view)(IC:s_prop)(p:s_prop)
  (invariant E IC p)->
  (everywhere (s_imp (si E IC) p)).

Intros.
Elim H.
Clear H.
Intros.
Elim H.
Clear H.
Intros.
Cut (everywhere (s_imp (si E IC) x)).
Generalize H0.
Unfold everywhere s_imp.
Clear H H0.
Intros.
Apply H0.
Apply H.
Trivial.
Apply indinv_imp_si.
Trivial.
Qed.


Theorem si_imp_inv : (E:view)(IC:s_prop)(p:s_prop)
  (everywhere (s_imp (si E IC) p))->
  (invariant E IC p).

Intros.
Unfold invariant.
Split with (si E IC).
Split.
Apply si_is_indinv.
Trivial.
Qed.

(*BEGIN-H*)

Theorem inv_char : (E:view)(IC:s_prop)(p:s_prop)
  (invariant E IC p)<->
  (everywhere (s_imp (si E IC) p)).

Intros.
Split.
Intros.
Apply inv_imp_si.
Trivial.
Intros.
Apply si_imp_inv.
Trivial.
Qed.

(*END-H*)

(*T* The following theorem specializes the theorem |rel_stable| given
before to relativized inductive invariants. Here it is necessary to
require that |r| is not only stable but is also an inductive invariant. The
theorem is particularly useful to prove and strengthen invariants
incrementally. Notice that |r| cannot only be exploited in the proof
of the right hand side of the |co| premise but also to establish that
|p| holds initially. *T*)

Theorem rel_inv : (E:view)(IC,p,r:s_prop)
  (ind_invariant E IC r)->
  (everywhere (s_imp (s_and IC r) p))->
  (co E (s_and r p) (s_imp r p))->
  (ind_invariant E IC (s_and r p)).

Intros.
Unfold ind_invariant.
Split.
Unfold ind_invariant in H.
Elim H.
Intros.
Clear H3 H1 H.
Unfold everywhere s_imp s_and.
Unfold everywhere s_imp s_and in H0.
Unfold everywhere s_imp in H2.
Intros.
Split.
Apply H2.
Trivial.
Apply H0.
Split.
Trivial.
Apply H2.
Trivial.
Apply rel_stable.
Unfold ind_invariant in H.
Elim H.
Intros.
Trivial.
Trivial.
Qed.

(*T* Using |co_stable_conjunction| and |co_implication| we can
prove a conjunction rule for |stable| and |unless|, stating that a
stable state predicate |r| can be added by conjunction to both sides
of an existing |unless| assertion. *T*)

Theorem unless_stable_conjunction : (E:view)(p,q,r:s_prop)
  (stable E r) -> (unless E p q) -> 
  (unless E (s_and p r) (s_and q r)).

Unfold unless.
Intros.
Generalize (co_stable_conjunction E (s_and p (s_not q)) (s_or p q) r
             H H0).
Intros.
Clear  H0.
Apply co_implication with p':=(s_and (s_and p (s_not q)) r) q:=(
s_and (s_or p q) r).
Unfold everywhere s_imp s_and s_not.
Intros.
Split.
Elim H0.
Intros.
Split.
Elim H2.
Intros.
Auto.
Unfold not.
Intros.
Elim H3.
Split.
Auto.
Elim H2.
Intros.
Auto.
Elim H0.
Intros.
Elim H2.
Intros.
Auto.
Unfold everywhere s_imp s_and s_or.
Intros.
Elim H0.
Intros.
Elim H2.
Intros.
Left.
Split.
Auto.
Auto.
Intros.
Right.
Split.
Auto.
Auto.
Auto.
Qed.

(*T* Extending the collection of proof rules for relativized assertions
|rel_co|, \linebreak |rel_stable| and |rel_inv| we add corresponding rules
for relativized |unless| assertions. *T*)

Theorem rel_unless : (E:view)(p,q,r:s_prop)
  (stable E r)->
  (co E (s_and3 r p (s_not q)) (s_imp r (s_or p q)))->
  (unless E (s_and r p) (s_and r q)).

Intros.
Unfold unless.
Generalize (co_stable_conjunction ? ? ? ? H H0).
Clear H H0.
Intros.
Apply co_implication with 3:=H.
Clear H.
Unfold everywhere s_imp s_and s_and3.
Unfold s_not.
Tauto.
Unfold everywhere s_imp s_and s_or.
Tauto.
Qed.

Theorem rel_unless_dep : (E:view)(r:s_prop)
  (stable E r)->(p,q:(s:st)(r s)->Prop)
  (co E (ds_ex r (ds_and r p (ds_not r q)))
        (ds_all r (ds_or r p q)))->
  (unless E (ds_ex r p) (ds_ex r q)).

Intros.
Unfold unless.
Generalize (co_stable_conjunction ? ? ? ? H H0).
Clear H H0.
Intros.
Apply co_implication with 3:=H.
Clear H.
Unfold everywhere s_imp s_and s_or s_not.
Intros.
Elim H.
Clear H.
Intros.
Elim H.
Intro prf'.
Intro.
Split.
Split with prf'.
Split.
Trivial.
Unfold not.
Intros.
Unfold ds_not.
Unfold not.
Intros.
Apply H0.
Split with prf'.
Trivial.
Trivial.
Unfold everywhere s_imp s_and s_or.
Intros.
Elim H0.
Clear H0.
Intros.
Elim (H0 H1).
Clear H0.
Intros.
Left .
Split with H1.
Trivial.
Intros.
Right .
Split with H1.
Trivial.
Qed.

(*BEGIN-H*)

Theorem rel_co_imp_unless_dep : (E:view)(r:s_prop)
  (stable E r)->(p,q:(s:st)(r s)->Prop)
  (co E (ds_ex r (ds_and r p (ds_not r q)))
        (ds_ex r (ds_or r p q)))->
  (unless E (ds_ex r p) (ds_ex r q)).

Intros.
Unfold unless.
Generalize (co_stable_conjunction ? ? ? ? H H0).
Clear H H0.
Intros.
Apply co_implication with 3:=H.
Clear H.
Unfold everywhere s_imp s_and s_or s_not.
Intros.
Elim H.
Clear H.
Intros.
Elim H.
Intro prf'.
Intro.
Split.
Split with prf'.
Split.
Trivial.

Unfold ds_not.
Unfold not.
Intros.
Apply H0.
Split with prf'.
Trivial.

Trivial.

Unfold everywhere s_imp s_and s_or.
Intros.
Elim H0.
Clear H0.
Intros.
Elim H0.
Clear H0.
Intros.
Elim H0.
Intros.
Left .
Unfold ds_ex.
Split with x.
Trivial.

Intros.
Right .
Split with x.
Trivial.
Qed.

Theorem rel_unless_imp_co_dep : (E:view)(r:s_prop)
  (p,q:(s:st)(r s)->Prop)
  (unless E (ds_ex r p) (ds_ex r q))->
  (co E (ds_ex r (ds_and r p (ds_not r q)))
        (ds_ex r (ds_or r p q))).

Unfold unless.
Intros.
Apply co_implication with 3:=H.
Clear H.
log_unfold .
Intros.
ECI H.
ECI H.
Split.
Split with x.
Trivial.

Unfold not.
Intros.
Elim H1.
Intros.
Apply H0.
Rewrite (proof_irrelevance ? x x0).
Trivial.

Clear H.
log_unfold .
Intros.
ECI H.
ECI H.
Split with x.
Auto.

ECI H.
Split with x.
Auto.
Qed.

(*END-H*)

Theorem rel_unless_dep_strengthen : (E:view)(r,r':s_prop)
  (stable E r)->
  (ev:(everywhere (s_imp r r')))
  (p,q:(s:st)(r' s)->Prop)
  (unless E (ds_ex r' p)
            (ds_ex r' q))->
  (unless E (ds_ex r (ds_cast r r' ev p)) 
            (ds_ex r (ds_cast r r' ev q))).


Intros.
Apply rel_co_imp_unless_dep.
Trivial.

Generalize (rel_unless_imp_co_dep ? ? ? ? H0).
Clear H0.
Intros.
Generalize (rel_co_dep_strengthen E r r' H ev ? ? H0).
Clear H0.
Intros.
Apply co_implication with 3:=H0.
Clear H0.
log_unfold .
Auto.

log_unfold .
Auto.
Qed.

(*T* The following theorem |co_big_conjunction| provides a conjunction
rule for an arbitrary family of |co| assertions indexed by a type |T|
which may be infinite in general. Notice that |(s_all T P)| is the
conjunction over the family |P| of state predicates indexed by
|T|. *T*)

Theorem co_big_conjunction : (T:Type)(E:view)(P,Q:T->s_prop)
  ((t:T)(co E (P t) (Q t)))->
  (co E (s_all T P) (s_all T Q)).

Unfold co.
Intros.
Unfold s_all.
Unfold hoare.
Unfold hoare in H.
Intros.
Apply (H t e H0 s s' H1).
Apply H2.
Qed.

(*T* There are rules for disjunction similar to those for the
conjunction of |co| assertions. Again we have a finitary version and a
general version for an arbitrary family of premises. 
Below |(s_ex T P)| is the disjunction over the family |P| of state predicates 
indexed by |T|. *T*)

Theorem co_big_disjunction : (T:Type)(E:view)(P,Q:T->s_prop)
  ((t:T)(co E (P t) (Q t)))->
  (co E (s_ex T P) (s_ex T Q)).

Unfold co.
Unfold s_ex.
Unfold hoare.
Intro.
Intros.
Elim H2.
Intros.
Split with x.
Apply (H x e H0 s s' H1).
Trivial.
Qed.

Theorem co_disjunction : (E:view)(p,p',q,q':s_prop)
  (co E p q) -> (co E p' q') -> 
  (co E (s_or p p') (s_or q q')).

Intros.
Generalize (co_big_disjunction bool E).
Intros.
Generalize (H1 [x:bool](bool_rect [_:bool]s_prop p p' x)).
Intros.
Generalize (H2 [x:bool](bool_rect [_:bool]s_prop q q' x)).
Intros.
Apply co_implication
 with p':=(s_ex bool [x:bool](bool_rect [_:bool]s_prop p p' x))
      q:=(s_ex bool [x:bool](bool_rect [_:bool]s_prop q q' x)).
Red.
(Intros; Red).
Intros.
Red.
Red in H4.
Elim H4.
Intro.
Split with true.
Red.
Trivial.
(Intro; Split with false; Red; Trivial).
Red.
(Unfold s_imp; Intros).
Red in H4.
Elim H4.
Induction x.
Intro.
Red.
Red in H5.
(Left ; Assumption).
Intro.
Red in H5.
Red.
Right .
Assumption.
Clear H2.
Apply H3.
Clear H3.
Intros.
Clear H1.
Elim t.
Simpl.
Trivial.
(Simpl; Assumption).
Qed.


(*T* Remember that |s_false| and |s_true| are state propositions which
are true and false for all states, respectively. Here we use them to
state a few trivial properties of |co| and |unless|. *T*)

Theorem co_false : (E:view)(p:s_prop)
  (co E s_false p).

Unfold co s_false.
Unfold hoare.
Intros.
Elim H1.
Qed.

(*BEGIN-H*)

Theorem co_not_l : (E:view)(p,q:s_prop)
  (everywhere (s_not p))->(co E p q).

Intros.
Apply co_implication_l with 2:=(co_false E q).
Unfold everywhere s_not in H.
Unfold everywhere s_imp s_not.
Unfold s_false.
Auto.
Qed.

(*END-H*)

Theorem co_true : (E:view)(p:s_prop)
  (co E p s_true).

Intros.
Apply sc_co.
Intros.
Unfold s_true.
Try Trivial.
Qed.

(*BEGIN-H*)

Theorem co_everywhere : (E:view)(p,q:s_prop)
  (everywhere q)->(co E p q).

Intros.
Apply co_implication_r with 2:=(co_true E p).
Unfold everywhere in H.
log_unfold .
Intros.
Apply H.
Qed.

(*END-H*)

Theorem unless_true : (E:view)(p:s_prop)
  (unless E p s_true).

Unfold unless.
Intros.
Specialize (co_true E (s_and p (s_not s_true))).
Intros.
Apply co_implication_r with 2:=H.
Unfold everywhere s_imp s_or.
Unfold s_true.
Tauto.
Qed.


(*BEGIN-H*)

Theorem unless_subst_r : (E:view)(p,q,q':s_prop)
  (everywhere (s_iff q q'))->(unless E p q)->(unless E p q').

Unfold unless.
Intros.
Apply co_implication_r with q:=(s_or p q).
Unfold everywhere s_imp s_or s_or.
Unfold everywhere s_iff in H.
Intros.
Elim (H s).
Intros.
Elim H1.
Intros.
Left.
Assumption.
Intros.
Right.
Apply H2.
Assumption.
Apply co_implication_l with q:=(s_and p (s_not q)).
Unfold everywhere s_imp s_and s_not.
Unfold everywhere s_iff in H.
Intros.
Elim (H s).
Intros.
Elim H1.
Intros.
Split.
Assumption.
Unfold not in H5.
Unfold not.
Intros.
Apply H5.
Apply H2.
Assumption.
Assumption.
Qed.

Theorem unless_subst_l : (E:view)(p,p',q:s_prop)
  (everywhere (s_iff p p'))->(unless E p q)->(unless E p' q).

Unfold unless.
Intros.
Apply co_implication_r with q:=(s_or p q).
Unfold everywhere s_imp s_or s_or.
Unfold everywhere s_iff in H.
Intros.
Elim (H s).
Intros.
Elim H1.
Intros.
Left.
Apply H2.
Assumption.
Intros.
Right.
Assumption.
Apply co_implication_l with q:=(s_and p (s_not q)).
Unfold everywhere s_imp s_and s_not.
Unfold everywhere s_iff in H.
Intros.
Elim (H s).
Intros.
Elim H1.
Intros.
Split.
Apply H3.
Assumption.
Assumption.
Assumption.
Qed.

Axiom unless_subst : (E:view)(p,q,p',q':s_prop)
  (everywhere (s_iff p p'))->
  (everywhere (s_iff q q'))->
  (unless E p q)->(unless E p' q').

(*END-H*)


(*BEGIN-H*)

(* The operator |unless| is reflexive on state predicates as
stated in the following theorem. *)

Theorem unless_refl : (E:view)(p:s_prop)(unless E p p).

Intros.
Unfold unless.
Apply co_implication_l with q:=s_false.
Unfold everywhere s_imp s_and s_not s_false.
Intros.
Elim H.
Intros.
Apply (H1 H0).
Apply co_false.
Qed.

(*END-H*)

(*T* In the simplest case, |unless| assertions can be derived from
implications. *T*)

Theorem unless_imp : (E:view)(p,q:s_prop)
  (everywhere (s_imp p q))->(unless E p q).

Unfold everywhere unless.
Unfold co s_and s_not s_or.
Unfold hoare.
Unfold s_imp.
Intros.
Elim H2.
Intros.
Specialize (H s H3).
Intros.
Elim H4.
Trivial.
Qed.

(*T* An equivalence between |(stable E p)| and 
|(unless E p s_false)| is proved by the following two implications.  In
\cite{ChandyMisra88} this equivalence is taken to define
|stable|. *T*)

Theorem stable_imp_unless : (E:view)(p,q:s_prop)
  (stable E p)->(unless E p q).

Unfold stable unless.
Intros.
Apply co_implication with 3:=H.
Unfold everywhere s_imp s_and s_not.
Tauto.
Unfold everywhere s_imp s_or.
Tauto.
Qed.

Theorem unless_imp_stable : (E:view)(p:s_prop)
  (unless E p s_false)->(stable E p).

Unfold unless stable.
Intros.
Apply co_implication with p':=(s_and p (s_not s_false)) q:=(s_or p
                                                              s_false).
Unfold everywhere s_imp s_and s_not s_false.
Intros.
Split.
Auto.
Unfold False.
Unfold not.
Auto.
Unfold everywhere s_imp s_or s_false.
Intros.
Elim H0.
Auto.
Intros.
Elim H1.
Auto.
Qed.

(*T* Using the general disjunction rule |co_big_disjunction| for
|co| we can prove a similar rule for |unless|. *T*)

Theorem unless_big_disjunction : 
  (E:view)(T:Type)(P,Q:T->s_prop)
  ((i:T)(unless E (P i) (Q i)))->
  (unless E (s_ex T P) (s_ex T Q)).

Intros.
Unfold unless.
Unfold unless in H.
Generalize (co_big_disjunction T E [i:T](s_and (P i) (s_not (Q i)))
             [i:T](s_or (P i) (Q i)) H).
Intro.
Apply co_implication with p':=(s_ex T
                                  [i:T](s_and (P i) (s_not (Q i)))) q:=(
s_ex T [i:T](s_or (P i) (Q i))).
Unfold everywhere s_imp s_and s_ex s_not.
Intros.
Elim H1.
Intros.
Elim H2.
Intros t.
Intros.
Exists  t.
Split.
Assumption.
Unfold not.
Intros.
Unfold not in H3.
Apply H3.
Exists  t.
Assumption.
Unfold everywhere s_imp s_ex s_or.
Intros.
Elim H1.
Intros t.
Intros.
Elim H2.
Intros.
Left.
Exists  t.
Assumption.
Intros.
Right.
Exists  t.
Assumption.
Assumption.
Qed.

(*T* The following rule allows weakening of the right hand side of
|unless|. It is known as the consequence weakening rule. *T*)

Theorem unless_implication_r : (E:view)(p,q,r:s_prop)
  (everywhere (s_imp q r)) ->
  (unless E p q) -> (unless E p r).

Unfold everywhere s_imp unless.
Unfold co s_and s_not s_or.
Unfold hoare.
Intros.
Cut (s_or p q s').
Unfold s_or.
Intros.
Elim H4.
Intros.
Left.
Trivial.

Intros.
Right.
Apply H.
Trivial.

Apply (H0 e H1 s s' H2).
Elim H3.
Intros.
Split.
Trivial.

Unfold not.
Intros.
Elim H5.
Apply H.
Trivial.
Qed.

(*T* We also have a conjunction rule for |unless|, but notice that, in
contrast to the conjunction rule for |co|, we have a disjunction of
three state predicates on the right hand side depending on whether
progress takes place in the second, in the first or in both
premises. *T*)

Theorem unless_conjunction : (E:view)(p,p',q,q':s_prop)
  (unless E p q) -> (unless E p' q') -> 
  (unless E (s_and p p') 
     (s_or3 (s_and p q') (s_and p' q) (s_and q q'))).

Unfold unless.
Unfold co.
Unfold hoare.
log_unfold .
Intros.
Generalize (H e H1 s s' H2).
Clear H.
Intros.
Generalize (H0 e H1 s s' H2).
Clear H0.
Intros.
Clear H2 H1.
Tauto.
Qed.

(*T* Right hand side weakening of the previous conjunction rule yields
the simple conjunction rule. *T*)

Theorem unless_simple_conjunction : (E:view)(p,p',q,q':s_prop)
  (unless E p q) -> (unless E p' q') -> 
  (unless E (s_and p p') (s_or q q')).

Intros.
Apply unless_implication_r with q:=(s_or3 (s_and p q') (s_and p' q)
                                       (s_and q q')).
Unfold everywhere s_imp s_or3 s_and.
Intros.
Unfold s_or.
Elim H1.
Intros.
Elim H2.
Intros.
Right.
Assumption.
Intros.
Elim H2.
Intros.
Elim H3.
Intros.
Left.
Assumption.
Intros.
Left.
Elim H3.
Intros.
Assumption.
Apply unless_conjunction.
Assumption.
Assumption.
Qed.

(*T* As a special case of |unless_simple_conjunction| we obtain the
following binary conjunction rule for |unless|, which is
generalized by induction to a finite family of premises in
the theorem |unless_left_big_conjunction|. *T*)

Theorem unless_left_conjunction : (E:view)(p,p',q:s_prop)
  (unless E p q) -> (unless E p' q) -> 
  (unless E (s_and p p') q).

Intros.
Apply unless_implication_r with q:=(s_or q q).
Unfold everywhere s_imp s_or.
Tauto.
Apply unless_simple_conjunction.
Trivial.
Trivial.
Qed.

Theorem unless_left_big_conjunction : (E:view)
  (b:nat)(Q:nat->s_prop)(r:s_prop)
  ((i:nat)(lt i b)->(unless E (Q i) r))->
  (unless E (s_all_nat b Q) r).

Intro E.
Intro b.
Intro Q.
Generalize b.
Clear b.
Induction b.
Intros.
Clear H.
Unfold unless.
Apply (co_implication_r E (s_and (s_all_nat (0) Q) (s_not r)) s_true
        (s_or (s_all_nat (0) Q) r)).
Unfold everywhere s_imp s_true s_or s_all_nat.
Intros.
Left .
Intros.
Elim (lt_n_O ? H0).
Apply co_true.
Intros.
Cut (unless E (Q n) r).
Intros.
Cut (i:nat)(lt i n)->(unless E (Q i) r).
Intros.
Specialize (H r H2).
Intros.
Specialize (unless_left_conjunction E ? ? ? H1 H3).
Intros.
Apply unless_subst_l with 2:=H4.
Unfold everywhere s_iff s_and s_all_nat.
Intros.
Split.
Intros.
Elim H5.
Intros.
Cut (le i n).
Intros.
Elim (le_lt_or_eq i n H9).
Intros.
Apply H8.
Trivial.
Intros.
Rewrite H10.
Trivial.
Apply lt_n_Sm_le.
Trivial.
Intros.
Split.
Apply H5.
Apply lt_n_Sn.
Intros.
Apply H5.
Apply lt_S.
Trivial.
Intros.
Apply H0.
Auto.
Apply H0.
Apply lt_n_Sn.
Qed.

(*T* In analogy to |unless_simple_conjunction| there is a simple
disjunction rule for |unless| formulated in the following theorem. *T*)

Theorem unless_simple_disjunction : (E:view)(p,p',q,q':s_prop)
  (unless E p q) -> (unless E p' q') -> 
  (unless E (s_or p p') (s_or q q')).

Intros.
Unfold unless in H.
Unfold unless in H0.
Unfold unless.
Generalize (co_disjunction E ? ? ? ? H H0).
Intros.
Clear H H0.
Apply co_implication
 with p':=(s_or (s_and p (s_not q)) (s_and p' (s_not q')))
      q:=(s_or (s_or p q) (s_or p' q')).
Unfold everywhere s_imp s_and s_not s_or.
Intros.
Elim H.
Intros.
Clear H.
Elim H0.
Intros.
Left .
Split.
Trivial.
Unfold not.
Intros.
Apply H2.
Left .
Trivial.
Intros.
Right .
Split.
Trivial.
Unfold not.
Intros.
Apply H2.
Right .
Trivial.
Unfold everywhere s_imp s_or.
Intros.
Elim H.
Intros.
Elim H0.
Intros.
Left .
Left .
Trivial.
Intros.
Right .
Left .
Trivial.
Intros.
Elim H0.
Intros.
Left .
Right .
Trivial.
Intros.
Right .
Right .
Trivial.
Trivial.
Qed.


(*T* Similar to |unless_conjunction| we can combine two |unless|
assertions in a disjunctive fashion using the rule
|unless_disjunction|. The proof is done by applying
|co_disjunction| and |co_implication|.  *T*)

Theorem unless_disjunction : (E:view)(p,p',q,q':s_prop)
  (unless E p q) -> (unless E p' q') -> 
  (unless E (s_or p p') 
    (s_or3 
      (s_and (s_not p) q') (s_and (s_not p') q) (s_and q q'))).

Intros E p p' q q'.
Intros.
Unfold unless in H.
Unfold unless in H0.
Unfold unless.
Generalize (co_disjunction E ? ? ? ? H H0).
Intros.
Clear H H0.
Apply co_implication
 with p':=(s_or (s_and p (s_not q)) (s_and p' (s_not q')))
      q:=(s_or (s_or p q) (s_or p' q')).
Unfold everywhere s_imp s_and s_not s_or s_or3.
Intros.
Elim H.
Clear H.
Intros.
Clear H1.
Generalize (classic (p s)).
Generalize (classic (p' s)).
Generalize (classic (q s)).
Generalize (classic (q' s)).
Intros.
Elim H.
Intros.
Elim H2.
Intros.
Elim H3.
Intros.
Elim H1.
Intros.
Elim H0.
Right .
Right .
Auto.

Intros.
Right .
Auto.

Intros.
Elim H0.
Right .
Left .
Auto.

Intros.
Left .
Auto.

Intros.
Elim H1.
Intros.
Elim H2.
Intros.
Elim H0.
Right .
Right .
Auto.

Intros.
Elim H4.
Intros.
Left .
Auto.

Intros.
Elim H0.
Left .
Auto.

Intros.
Right .
Auto.

Unfold everywhere s_imp s_and s_not s_or s_or3.
Intros.
Generalize (classic (p s)).
Generalize (classic (p' s)).
Generalize (classic (q s)).
Generalize (classic (q' s)).
Intros.
Clear H1.
Elim H.
Intros.
Elim H1.
Intros.
Left .
Auto.

Intros.
Elim H0.
Intros.
Right .
Right .
Right .
Auto.

Intros.
Elim H3.
Intros.
Left .
Auto.

Intros.
Right .
Right .
Left .
Auto.

Intros.
Elim H1.
Intros.
Left .
Auto.

Intros.
Elim H4.
Auto.

Auto.

Trivial.
Qed.


(*T* It is interesting to note that the proof of
|unless_simple_disjunction| is the only proof in the current version
of the temporal logic library which relies on the use of the classical
axiom |classic|.  Without this axiom it would not be possible to make
use of the left hand side of the |co| assertion in the conclusion
which is of the form 
\begin{verbatim}
        (s_and (s_or p p') 
               (s_not (s_or3 (s_and (s_not p) q') 
                             (s_and (s_not p') q) 
                             (s_and q q'))))
\end{verbatim}
if we expand the
definition of |unless|.  Consider a state satisfying this predicate.
Intuitionistically, we can infer that in this state |q| and |q'|
cannot hold simultaneously, but we do not know which one does not
hold.  In other words, we have |(s_and p (s_not q))| or |(s_and p' (s_not q'))| 
classically, but it does not hold intuitionistically, so that
without the classical axiom it is undecidable which of the two |unless|
premises should be applied. *T*)

(*T* Finally, we use |unless_disjunction| to prove the following cancelation
rule: If we can leave a state satisfying |p| only via a state
satisfying |q| and a state satisfying |q| only via a state statisfying
|r|, it follows that a state satisfying |(s_or p q)| can only be left
via |r|. *T*)

Theorem unless_cancelation : (E:view)(p,q,r:s_prop)
  (unless E p q) -> (unless E q r) -> 
  (unless E (s_or p q) r).

Intros.
Generalize (unless_disjunction E p q q r).
Intros.
Apply (unless_implication_r E (s_or p q)
        (s_or3 (s_and (s_not p) r) (s_and (s_not q) q) (s_and q r)) r).
Unfold everywhere.
Intros.
Unfold s_imp.
Unfold s_or3.
Unfold s_and.
Unfold s_not.
Intros.
Elim H2.
Intros.
Elim H3.
Intros.
Exact H5.
Intros.
Elim H3.
Intros.
Elim H4.
Unfold not.
Intros.
Elim H5.
Exact H6.
Intros.
Elim H4.
Intros.
Exact H6.
Apply H1.
Clear H1.
Exact H.
Clear H1.
Exact H0.
Qed.