(*T* \usection{Liveness Assertions}\label{liveness-section} *T*) (*T* As in New UNITY the liveness assertions |ensures| and |leads_to| are built on top of |unless| and |transient| assertions. This is done in the module |liveness|, which is discussed below and also contains general proof rules for liveness assertions. *T*) (*T* We begin by definining enabledness of an action |e| as a state predicate |(enabled e)| which is satisfied for those states |s| where the action |e| may occur. *T*) Definition enabled := [e:act][s:st] (ExT ([s':st] (trans e s s'))) . (*T* We then lift |(enabled e)| to groups of actions giving rise to another state predicate |(group_enabled E)| which is statisfied iff the group |E| (i.e. at least one action from this group) is enabled. *T*) Definition group_enabled := [E:(set act)][s:st] (ExT [e:act](In act E e) /\ (enabled e s)). (*T* We next introduce |sco|, the strong version of |co|, which takes enabledness into account. The assertion |(sco E p q)| means not only that in |E| the sucessor state of a state satisfying |p| is a state satisfying |q|, but it also states that |E| seen as a group of actions is enabled in every state satisfying |p|. *T*) Definition en := [E:(set act)][p:s_prop] (everywhere (s_imp p (group_enabled E))). Definition sco := [E:(set act)][p,q:s_prop] (en E p) /\ (co E p q) . (*T* These definitions have a number of simple consequences: *T*) Theorem sco_false : (E:(set act))(q:s_prop)(sco E s_false q). Intros. Unfold sco. Intros. Split. Unfold en. Intros. Unfold everywhere s_imp s_false. Intros. Elim H. Apply co_false. Qed. Theorem en_implication : (E:(set act))(p,q:s_prop) (everywhere (s_imp p q)) -> (en E q) -> (en E p). Intro. Unfold en. Unfold everywhere s_imp. Intros. Cut (q s). Intros. Specialize (H0 s H2). Auto. Apply H. Trivial. Qed. Theorem sco_implication : (E:(set act))(p,p',q,q':s_prop) (everywhere (s_imp p p')) -> (everywhere (s_imp q q')) -> (sco E p' q) -> (sco E p q'). Unfold sco. Intros. Elim H1. Intros. Split. Apply en_implication with 1:=H. Trivial. Apply co_implication with 1:=H 2:=H0. Trivial. Qed. Theorem co_sco_conjunction : (E:view) (p,q:s_prop)(co E p q)-> (p',q':s_prop)(sco E p' q')-> (sco E (s_and p p') (s_and q q')). Unfold sco. Intros. Elim H0. Intros. Split. Apply (en_implication E (s_and p p') p'). Unfold everywhere s_imp s_and. Intros. Elim H3. Auto. Trivial. Apply co_conjunction. Trivial. Trivial. Qed. Theorem stable_sco_conjunction : (E:view)(E':view) (Included act E' E)-> (r:s_prop)(stable E r)-> (p,q:s_prop)(sco E' p q)-> (sco E' (s_and r p) (s_and r q)). Unfold stable. Intros. Apply co_sco_conjunction. Unfold co hoare in H0. Unfold co hoare. Intros. Cut (In ? E e). Intros. Apply (H0 e H5 s s' H3). Trivial. Auto with v62. Trivial. Qed. (*T* Now we are prepared to give the formal definition of |transient|, which states that the assertion |(transient E p)| is satisfied iff the given view |E| includes a weakly fair group |E'| of actions such that for every state satisfying |p| each successor state obtained by executing an action from |E'| invalidates |p|. *T*) Definition transient := [E:view][p:s_prop] (ExT [E':(set act)] (In (set act) wf E')/\(Included act E' E)/\ (sco E' p (s_not p))). (*T* Some simple theorems about |transient| are given next. *T*) Theorem transient_implication : (E:view)(p,q:s_prop) (transient E p)->(everywhere (s_imp q p))-> (transient E q). Unfold transient. Intros. Unfold everywhere in H0. Elim H. Intros T. Intros. Split with T. Elim H1. Intros. Elim H3. Intros. Split. Trivial. Split. Trivial. Unfold sco. Unfold sco in H5. Intros. Clear H. Clear H1. Clear H3. Elim H5. Intros. Split. Apply (en_implication T q p). Trivial. Trivial. Clear H H2 H4 H5. Apply (co_implication T q p (s_not p) (s_not q)). Trivial. Unfold everywhere s_imp s_not. Unfold s_imp in H0. Clear H1. Auto. Trivial. Qed. (*BEGIN-H*) (* This can be easily stated in a different form: *) Theorem transient_strengthen : (E:view)(p,q:s_prop) (transient E p)->(transient E (s_and p q)). Intros. Apply transient_implication with 1:=H. Unfold everywhere. Clear H. Intros. Unfold s_imp s_and. Tauto. Qed. (*END-H*) Theorem transient_false : (E:view)(transient E s_false). Intros. Unfold transient. Split with (Empty_set act). Intros. Split. Apply wf_contains_empty_set. Split. Apply Included_Empty. Apply sco_false. Qed. (*T* The previous theorem |transient_false| is reduced to |sco_false| by exploiting our convention that the empty group is weakly fair, as expressed by the axiom |wf_contains_empty_set| in the module |abstract|. In fact, this is the only place where this axiom is used. *T*) (*T* The following rule allows us to combine a |stable| and a |transient| assertion. Being stable and being transient are contradictory requirements for a state predicte, except for the trivial case where it is never satisfied. *T*) Theorem stable_and_transient : (E:view)(p:s_prop) (stable E p) -> (transient E p) -> (everywhere (s_not p)). Unfold stable. Unfold transient. Unfold everywhere s_not. Intros. Elim H0. Intros T. Clear H0. Intros. Elim H0. Intros. Elim H2. Intros. Unfold sco in H4. Unfold not. Intros. Elim H4. Clear H4. Clear H0 H1 H2. Intros. Unfold co in H. Unfold co in H1. Unfold hoare in H. Unfold en in H0. Elim (H0 s H5). Intro t. Intros. Elim H2. Clear H2. Intros. Cut (In ? E t). Intros. Unfold hoare in H1. Unfold enabled in H4. Elim H4. Clear H4. Intros. Specialize (H1 t H2 s x H4 H5). Intros. Specialize (H t H6 s x H4 H5). Intros. Elim H7. Trivial. Apply H3. Trivial. Qed. (*BEGIN-H*) (* The following rule allows substitution of state predicates by equivalent ones under the transient assertion. It extends our list of substitution rules |co_subst_r|, |co_subst_l|, |stable_subst|, |unless_subst_r| and |unless_subst_l|. *) Theorem transient_subst : (E:view)(p,q:s_prop) (everywhere (s_iff p q)) -> (transient E p) -> (transient E q). Unfold everywhere s_iff transient. Intros. Elim H0. Intros T. Intros. Split with T. Clear H0. Elim H1. Intros. Elim H2. Intros. Clear H1 H2. Split. Trivial. Split. Trivial. Apply sco_implication with 3:=H4. Unfold everywhere s_imp. Intros. Generalize (H s). Intros. Elim H2. Intros. Apply H6. Trivial. Unfold everywhere s_imp s_not. Intros. Unfold not. Unfold not in H1. Intros. Apply H1. Generalize (H s). Intros. Elim H5. Intros. Apply H7. Trivial. Qed. (*END-H*) (*T* Again we have proof rules to derive relativized |sco| and |transient| assertions: *T*) Theorem rel_sco : (E:view)(E':view) (Included act E' E)-> (r:s_prop)(stable E r)->(p,q:s_prop) (sco E' (s_and r p) (s_imp r q))-> (sco E' (s_and r p) (s_and r q)). Intros. Generalize (stable_sco_conjunction E E' H r H0 ? ? H1). Intros. Apply sco_implication with 3:=H2. Unfold everywhere s_imp s_and. Tauto. Unfold everywhere s_imp s_and. Tauto. Qed. (*H* Theorem rel_ex_step_dep : (E:view)(E:view) (Included ? E E)-> (r:s_prop)(stable E r)->(p,q:(s:st)(r s)->Prop) (sco E (ds_ex r p) (ds_all r q))-> (sco E (ds_ex r p) (ds_ex r q)). *H*) Theorem rel_transient : (E:view)(p,r:s_prop) (stable E r)-> (ExT [E':view] (In (set act) wf E')/\(Included act E' E)/\ (sco E' (s_and r p) (s_imp r (s_not p))))-> (transient E (s_and r p)). Intros. Elim H0. Clear H0. Intro E. Intros. Elim H0. Clear H0. Intros. Elim H1. Clear H1. Intros. Unfold transient. Split with E0. Split. Trivial. Split. Trivial. Cut (sco E0 (s_and r p) (s_and r (s_not p))). Intros. Apply sco_implication with 3:=H3. Clear H0 H1 H2 H3. log_unfold . Tauto. log_unfold . Clear H0 H1 H2 H3. Tauto. Apply rel_sco with E:=E. Trivial. Trivial. Trivial. Qed. (*T* The |ensures| assertion is essentially |unless| equipped with liveness. Remember the definition of |(unless E p q)| as |(co E (s_and p (s_not q)) (s_or p q))| stating that |(s_and p (s_not q))| implies that |(s_or p q)| holds in the next state in |E|. To ensure liveness we just have to add |(transient E (s_and p (s_|\linebreak|not q)))| expressing that |(s_and p (s_not q))| cannot hold permanently in |E|. This excludes the possibility that |p| holds forever and that |q| never becomes true. *T*) Definition ensures := [E:view][p,q:s_prop] (unless E p q) /\ (transient E (s_and p (s_not q))). (*T* From |unless_true| and |transient_false| we obtain immediately: *T*) Theorem ensures_true : (E:view)(p:s_prop) (ensures E p s_true). Intros. Unfold ensures. Split. Apply unless_true. Apply transient_implication with p:=s_false. Apply transient_false. Trivial. Unfold everywhere s_imp s_and s_not s_false. Tauto. Qed. (*BEGIN-H*) (* As for all other assertions we need substitution rules which are proved again without extensionality. *) Theorem ensures_subst_r : (E:view)(p,q,q':s_prop) (everywhere (s_iff q q'))-> (ensures E p q)->(ensures E p q'). Unfold ensures. Intros. Elim H0. Intros. Split. Apply unless_subst_r with q:=q. Assumption. Assumption. Apply (transient_subst E) with p:=(s_and p (s_not q)). Unfold everywhere s_and s_not s_iff. Unfold everywhere s_iff in H. Intros. Elim (H s). Intros. Split. Intros. Elim H5. Intros. Split. Assumption. Unfold not. Unfold not in H7. Intros. Apply H7. Apply H4. Assumption. Intros. Elim H5. Intros. Split. Assumption. Unfold not. Unfold not in H7. Intros. Apply H7. Apply H3. Assumption. Assumption. Qed. Theorem ensures_subst_l : (E:view)(p,p',q:s_prop) (everywhere (s_iff p p'))-> (ensures E p q)->(ensures E p' q). Unfold ensures. Intros. Elim H0. Intros. Split. Apply unless_subst_l with p:=p. Assumption. Assumption. Apply (transient_subst E) with p:=(s_and p (s_not q)). Unfold everywhere s_and s_not s_iff. Unfold everywhere s_iff in H. Intros. Elim (H s). Intros. Split. Intros. Elim H5. Intros. Split. Apply H3. Assumption. Assumption. Intros. Elim H5. Intros. Split. Apply H4. Assumption. Assumption. Assumption. Qed. (*END-H*) (*BEGIN-H*) (* The following reflexivity rule follows from |unless_refl| and |transient_false|. *) Theorem ensures_refl : (E:view)(p:s_prop)(ensures E p p). Unfold ensures. Intros. Split. Apply unless_refl. Apply transient_subst with p:=s_false. Unfold everywhere s_iff s_false s_and s_not. Intros. Split. Intros. Intros. Elim H. Intros. Elim H. Intros. Apply (H1 H0). Apply transient_false. Qed. (*END-H*) (*T* In analogy to |unless_imp|, any implication gives rise to an |ensures| assertion. *T*) Theorem ensures_imp : (E:view) (p,q:s_prop)(everywhere (s_imp p q)) -> (ensures E p q). Intros. Unfold ensures. Split. Apply unless_imp. Assumption. Apply transient_subst with p:=s_false. Unfold everywhere s_iff s_false s_and s_not. Intros. Split. Intro. Intros. Elim H0. Intros. Elim H0. Intros. Unfold everywhere s_imp in H. Generalize (H s H1). Intros. Apply (H2 H3). Apply transient_false. Qed. (*T* In an assertion |(ensures E p s_false)| the state predicate |p| can never be true, otherwise |s_false| would have to become true eventually which is impossible. *T*) Theorem ensures_false : (E:view) (p:s_prop)(ensures E p s_false)->(everywhere (s_not p)). Intros. Apply stable_and_transient with E:=E. Unfold ensures in H. Elim H. Intros. Apply unless_imp_stable. Trivial. Unfold ensures in H. Elim H. Clear H. Intros. Apply transient_implication with 1:=H0. Unfold everywhere s_imp s_and s_not. Unfold s_false. Tauto. Qed. (*T* In analogy to |unless_implication_r| we have a weakening rule for the right hand side of an |ensures| assertion. *T*) Theorem ensures_implication_r : (E:view)(p,q,r:s_prop) (everywhere (s_imp q r)) -> (ensures E p q) -> (ensures E p r). Unfold ensures. Intros. Elim H0. Intros. Split. Apply unless_implication_r with q:=q. Assumption. Assumption. Clear H0. Apply transient_implication with p:=(s_and p (s_not q)). Assumption. Unfold everywhere s_imp s_and s_not. Intros. Elim H0. Intros. Split. Assumption. Unfold not. Intros. Apply H4. Apply (H s). Assumption. Qed. (*T* The following conjunction rule for |ensures| has a form similar to the |unless| conjunction rule. Notice, however, that only one premise has to be a liveness assertion in order to infer liveness. *T*) Theorem ensures_conjunction : (E:view)(p,p',q,q':s_prop) (unless E p q) -> (ensures E p' q') -> (ensures E (s_and p p') (s_or3 (s_and p q') (s_and p' q) (s_and q q'))). Unfold ensures. Intros. Split. Apply unless_conjunction. Assumption. Elim H0. Intros. Assumption. Elim H0. Intros. Clear H0. Apply transient_implication with p:=(s_and p' (s_not q')). Assumption. Unfold everywhere s_imp s_and s_not. Intros. Unfold s_or3 in H0. Elim H0. Intros. Split. Elim H3. Intros. Assumption. Unfold not. Intros. Apply H4. Left. Split. Elim H3. Intros. Assumption. Assumption. Qed. Theorem ensures_stable_conjunction : (E:view) (p,q,r:s_prop)(stable E r)->(ensures E p q)-> (ensures E (s_and p r) (s_and q r)). Intros. Generalize (stable_imp_unless E r s_false H). Clear H. Intro. Generalize (ensures_conjunction E ? ? ? ? H H0). Clear H0 H. Intros. Cut (ensures E (s_and r p) (s_and q r)). Clear H. Intros. Apply ensures_subst_l with 2:=H. log_unfold . Clear H. Tauto. Apply ensures_implication_r with 2:=H. Clear H. log_unfold . Tauto. Qed. (*BEGIN-H*) Theorem ind_invariant_imp_ensures : (E:view)(p,q,r:s_prop) (ind_invariant E p r)-> (ensures E p q)->(ensures E p (s_and q r)). Intros E p q r I H0. Unfold ind_invariant in I. Elim I. Clear I. Intros. Cut (ensures E (s_and p r) (s_and q r)). Intros. Apply ensures_subst_l with 2:=H2. Clear H0 H1 H2. Generalize H. Clear H. log_unfold . Intros. Generalize (H s). Clear H. Tauto. Apply ensures_stable_conjunction with 1:=H1 2:=H0. Qed. (*END-H*) (*T* Finally, we have the usual rule to derive relativized |ensures| assertions. *T*) Theorem rel_ensures : (E:view)(p,q,r:s_prop) (stable E r)-> (unless E (s_and r p) (s_imp r q))-> (transient E (s_and r (s_and p (s_not q))))-> (ensures E (s_and r p) (s_and r q)). Unfold ensures. Intros. Split. Apply rel_unless. Trivial. Unfold unless in H0. Apply co_implication with 3:=H0. Unfold everywhere s_imp s_and s_and3 s_not. Clear H H0 H1. Tauto. Unfold everywhere s_imp s_and s_or. Clear H H0 H1. Tauto. Apply transient_subst with 2:=H1. Unfold everywhere s_iff s_and s_not. Clear H H0 H1. Tauto. Qed. (*T* The |leads_to| operator is defined inductively on top of |ensures|. In fact, we define |leads_to| as the smallest predicate satisfying the three properties |leads_to_|\linebreak|basis|, |leads_to_transitivity| and |leads_to_disjunction|. Remember that the assertion |(leads_to E p q)| should entail that if |p| holds in an arbitrary state in |E| then |q| will hold eventually in the future. This is obviously a weaker property than |(ensures E p q)|, justifying the implication |leads_to_basis| in the inductive definition below. Furthermore, transitivity is clearly a property of |leads_to|, as required by the implication |leads_to_transitivity|. Finally, the implication |leads_to_disjunction| formalizes a disjunction property: If |(leads_to E|\linebreak|(P i) q)| for a family |P| of state predicates, then we can conclude |(leads_to E|\linebreak|(s_ex T P) q)|. The justification is straightforward: Given a state |s| satisfying the disjunction |(s_ex T P)| there must be some index |i| such that |(P i)| is true at |s|. Now we can use the premise |(leads_to E (P i) q)| to infer that |q| will hold eventually. \begin{verbatim} Inductive leads_to [E:view] : s_prop->s_prop->Prop := leads_to_basis : (p,q:s_prop) (ensures E p q) -> (leads_to E p q) | leads_to_transitivity : (p,q,r:s_prop) (leads_to E p q) -> (leads_to E q r) -> (leads_to E p r) | leads_to_disjunction : (T:Type)(P:T->s_prop)(q:s_prop) ((i:T)(leads_to E (P i) q)) -> (leads_to E (s_ex T P) q). \end{verbatim} *T*) (*T* The induction principle associated with this inductive definition of |leads_to| can be formulated as follows: \begin{verbatim} Theorem leads_to_induction : (IH:view->s_prop->s_prop->Prop)(E:view) ((p,q:s_prop)(ensures E p q)->(IH E p q))-> ((p,q,r:s_prop) ((leads_to E p q)->(leads_to E q r)-> (IH E p q)->(IH E q r)->(IH E p r)))-> ((T:Type)(P:T->s_prop)(p,q:s_prop) ((i:T)(leads_to E (P i) q))->((i:T)(IH E (P i) q))-> (IH E (s_ex T P) q))-> ((p,q:s_prop) (leads_to E p q)->(IH E p q)). \end{verbatim} *T*) (*BEGIN-H*) Inductive leads_to [E:view] : s_prop->s_prop->Prop := leads_to_basis : (p,q:s_prop) (ensures E p q) -> (leads_to E p q) | leads_to_transitivity : (p,q,r:s_prop) (leads_to E p q) -> (leads_to E q r) -> (leads_to E p r) | leads_to_disjunction : (T:Type)(P:T->s_prop)(p,q:s_prop) ((i:T)(leads_to E (P i) q)) -> (everywhere (s_iff p (s_ex T P))) -> (leads_to E p q). (*END-H*) (*T* We now continue with proof rules for |leads_to| assertions, starting with an immediate consequence of |ensures_true|: *T*) Theorem leads_to_true : (E:view) (p:s_prop)(leads_to E p s_true). Intros. Apply leads_to_basis. Apply ensures_true. Qed. (*BEGIN-H*) (* Next we observe that the more standard form of |leads_to_disjunction| is obtained as a special case. *) Theorem leads_to_disjunction_2 : (E:view)(T:Type)(P:T->s_prop)(q:s_prop) ((i:T)(leads_to E (P i) q)) -> (leads_to E (s_ex T P) q). Intros. Apply (leads_to_disjunction E T P (s_ex T P) q). Assumption. Apply s_iff_refl. Qed. (* Due to the careful inductive definition |leads_to| enjoys substitution rules for both sides. *) Theorem leads_to_subst_r : (E:view)(p,q,q':s_prop) (everywhere (s_iff q q'))-> (leads_to E p q)->(leads_to E p q'). Intros E. Cut (p,q,q':s_prop) (leads_to E p q) ->(everywhere (s_iff q q'))->(leads_to E p q'). Intros. Generalize (H p q q' H1 H0). Auto. Induction 1. Intros. Constructor 1. Apply ensures_subst_r with p:=p0 q:=q0 q':=q'. Exact H1. Exact H0. Intros. Generalize (H3 H4). Intros. Constructor 2 with q:=q0. Exact H0. Exact H5. Intros. Constructor 3 with P:=P. Intros. Generalize (H1 i H3). Intros. Exact H4. Exact H2. Qed. Theorem leads_to_subst_l : (E:view)(p,p',q:s_prop) (everywhere (s_iff p p'))-> (leads_to E p q)->(leads_to E p' q). Intros E. Cut (p,q,p':s_prop) (leads_to E p q) ->(everywhere (s_iff p p'))->(leads_to E p' q). Intros. Generalize (H p q p' H1 H0). Intros. Exact H2. Induction 1. Intros. Constructor 1. Apply ensures_subst_l with p:=p0. Exact H1. Exact H0. Intros. Constructor 2 with q:=q0. Generalize (H1 H4). Intros. Exact H5. Exact H2. Intros. Constructor 3 with P:=P. Exact H0. Apply s_iff_trans with q:=p0. Apply s_iff_sym. Exact H3. Exact H2. Qed. (*END-H*) (*T* An immediate consequence of |ensures_imp| is that every implication gives rise to a |leads_to| assertion. We also give two specializations below. *T*) Theorem leads_to_imp : (E:view) (p,q:s_prop)(everywhere (s_imp p q)) -> (leads_to E p q). Intros. Apply leads_to_basis. Apply ensures_imp. Assumption. Qed. Theorem leads_to_refl : (E:view) (p:s_prop)(leads_to E p p). Intros. Apply leads_to_basis. Apply ensures_refl. Qed. Theorem leads_to_false : (E:view) (p:s_prop)(leads_to E s_false p). Intros. Apply leads_to_imp. Apply s_imp_false. Qed. (*T* Using |leads_to_imp| and |leads_to_transitivity| we can prove that an assertion |leads_to| can be strengthened on the left hand side and weakened on the right hand side as stated in the following theorem. *T*) (*BEGIN-H*) Theorem leads_to_implication_l : (E:view) (p,q,r:s_prop)(everywhere (s_imp p q)) -> (leads_to E q r) -> (leads_to E p r). Intros. Apply leads_to_transitivity with q:=q. Apply leads_to_imp. Assumption. Assumption. Qed. Theorem leads_to_implication_r : (E:view) (p,q,r:s_prop)(everywhere (s_imp q r)) -> (leads_to E p q) -> (leads_to E p r). Intros. Apply leads_to_transitivity with q:=q. Assumption. Apply leads_to_imp. Assumption. Qed. (*END-H*) Theorem leads_to_implication : (E:view) (p,p',q,q':s_prop) (everywhere (s_imp p p'))-> (everywhere (s_imp q q'))-> (leads_to E p' q)-> (leads_to E p q'). Intros. Apply leads_to_transitivity with q:=p'. Apply leads_to_imp. Assumption. Apply leads_to_transitivity with q:=q. Assumption. Apply leads_to_imp. Assumption. Qed. (*BEGIN-H*) (* Right hand side weakening can also be written with |s_or| and left hand side strengthening can be written using |s_and|. *) Theorem leads_to_weakening : (E:view) (p,q,r:s_prop)(leads_to E p q)->(leads_to E p (s_or q r)). Intros. Apply leads_to_implication_r with q:=q. Apply s_imp_or_l. Assumption. Qed. Theorem leads_to_strengthening : (E:view) (p,q,r:s_prop)(leads_to E p q)->(leads_to E (s_and p r) q). Intros. Apply leads_to_implication_l with q:=p. Apply s_imp_and_l. Assumption. Qed. (* As a special cases of |leads_to_disjunction| we have: *) Theorem leads_to_binary_disjunction : (E:view) (p,p',q:s_prop)(leads_to E p q)->(leads_to E p' q)-> (leads_to E (s_or p p') q). Intros. Generalize (leads_to_disjunction_2 E bool [b:bool]Cases b of true => p | false => p' end q). Intros. Cut (leads_to E (s_ex bool [b:bool]Case b of p p' end) q). Intros. Apply leads_to_implication_l with q:=(s_ex bool [b:bool]Case b of p p' end). Unfold everywhere s_or s_ex. Intros. Unfold s_imp. Intros. Elim H3. Intros. Split with true. Trivial. Intros. Split with false. Trivial. Trivial. Apply H1. Induction i. Trivial. Trivial. Qed. Theorem leads_to_ternary_disjunction : (E:view)(p,p',p'',q:s_prop) (leads_to E p q)-> (leads_to E p' q)-> (leads_to E p'' q)-> (leads_to E (s_or3 p p' p'') q). Intros. Specialize (leads_to_binary_disjunction E ? ? ? H H0). Intros. Specialize (leads_to_binary_disjunction E ? ? ? H2 H1). Intros. Apply leads_to_implication_l with q:=(s_or (s_or p p') p''). Unfold everywhere s_imp s_or3 s_or. Tauto. Trivial. Qed. (*END-H*) (*T* We also prove a general disjunction rule for arbitrary families of |leads_to| assertions. It is in fact a generalization of the |leads_to_disjunction| rule of the inductive definition. *T*) Theorem leads_to_big_disjunction : (E:view) (T:Type)(P,Q:T->s_prop) ((i:T)(leads_to E (P i) (Q i)))-> (leads_to E (s_ex T P) (s_ex T Q)). Intros. Cut (m:T)(leads_to E (Q m) (s_ex ? Q)). Intros. Cut (i:T)(leads_to E (P i) (s_ex T Q)). Intros. Apply leads_to_disjunction with P:=P. Assumption. Apply s_iff_refl. Intro. Generalize (H i). Intros. Generalize (H0 i). Intros. Apply leads_to_transitivity with 1:=H1 2:=H2. Intros. Apply leads_to_imp. Unfold everywhere s_imp s_ex. Intros. Split with m. Assumption. Qed. (*T* As a special case, we obtain a binary disjunction rule. *T*) Theorem leads_to_small_disjunction : (E:view)(p,q,p',q':s_prop) (leads_to E p p') -> (leads_to E q q')-> (leads_to E (s_or p q) (s_or p' q')). Intros. Generalize (leads_to_big_disjunction E bool [b:bool]Cases b of true => p | false => q end [b:bool]Cases b of true => p' | false => q' end). Intros. Apply leads_to_subst_r with q:=(s_ex bool [b:bool]Case b of p' q' end). Unfold everywhere s_iff s_ex s_or. Intros. Split. Intros. Elim H2. Induction x. Intros. Left . Assumption. Intros. Right . Assumption. Intros. Elim H2. Intros. Split with true. Assumption. Intros. Split with false. Assumption. Apply leads_to_subst_l with p:=(s_ex bool [b:bool]Case b of p q end). Unfold everywhere s_iff s_ex s_or. Intros. Split. Intros. Elim H2. Induction x. Intros. Left . Assumption. Intros. Right . Assumption. Intros. Elim H2. Intros. Split with true. Assumption. Intros. Split with false. Assumption. Apply H1. Induction i. Assumption. Assumption. Qed. (*T* The following cancelation rule is very useful in practice. Assume that: (1) |p| leads to |q| or |b|, and (2) |b| leads to |r|. Then |p| leads either to a state satisfying |q|, or if this is not the case, it must lead to a state satisfying |b|, which in turn leads to |r|. So we can conclude that |p| leads to |q| or |r|. *T*) Theorem leads_to_cancelation : (E:view)(p,q,b,r:s_prop) (leads_to E p (s_or q b))->(leads_to E b r)-> (leads_to E p (s_or q r)). Intros. Cut (leads_to E (s_or q b) (s_or q r)). Intros. Apply leads_to_transitivity with q:=(s_or q b). Assumption. Assumption. Apply leads_to_small_disjunction. Apply (leads_to_refl E). Assumption. Qed. (*T* A very powerful rule is the following progress-safety-progress rule |leads_to_| \linebreak |psp|, which combines a liveness assertion and a safety assertion and allows us to infer a new liveness assertion. The formal metalogical proof is somewhat tedious, but the semantic justification is intuitive: Assume (1) |p| leads to |q| and that (2) |r|, once it is true, cannot become false before |b| becomes true. Now there are two possibilities in a state statisfying |p| and |r|: Either |b| remains false forever, or it becomes true eventually. In the first case |p| and |r| leads to |q| and |r|, since |r| remains true. In the second case |p| and |r| leads to |b| trivially. *T*) (*T* The progress-safety-progress rule for |leads_to| will be proved by induction over the |leads_to| premise. We first prove the progress-safety-progress rule for |ensures|, which is the base case of the inductive definition of |leads_to|. *T*) Theorem ensures_psp : (E:view) (p,q,r,b:s_prop)(ensures E p q)->(unless E r b)-> (ensures E (s_and p r) (s_or (s_and q r) b)). Intros. Generalize (ensures_conjunction E r p b q). Intros. Generalize (H1 H0 H). Intros. Clear H1. Apply ensures_subst_l with p:=(s_and r p). Unfold everywhere s_iff s_and. Intros. Split. Intros. Elim H2. Intros. Split. Elim H1. Auto. Elim H1. Auto. Intros. Elim H1. Intros. Auto. Apply ensures_implication_r with q:=(s_or3 (s_and r q) (s_and p b) (s_and b q)). Unfold everywhere s_imp s_and s_or s_or3. Intros. Elim H1. Intros. Elim H3. Intros. Auto. Intros. Elim H3. Intros. Elim H4. Intros. Auto. Intros. Elim H3. Intros. Elim H5. Auto. Intros. Elim H5. Intros. Auto. Trivial. Qed. Theorem leads_to_psp : (E:view) (p,q,r,b:s_prop)(leads_to E p q)->(unless E r b)-> (leads_to E (s_and p r) (s_or (s_and q r) b)). Intros. Elim H. Intros. Constructor 1. Generalize (ensures_conjunction E r p0 b q0). Intros. Generalize (H2 H0 H1). Intros. Clear H2. Apply ensures_subst_l with p:=(s_and r p0). Unfold everywhere s_iff s_and. Intros. Split. Intros. Elim H2. Intros. Split. Assumption. Assumption. Intros. Elim H2. Intros. Split. Assumption. Assumption. Apply ensures_implication_r with q:=(s_or3 (s_and r q0) (s_and p0 b) (s_and b q0)). Unfold everywhere s_imp s_and s_or s_or3. Intros. Elim H2. Intros. Elim H4. Intros. Left . Split. Assumption. Assumption. Intros. Elim H4. Intros. Right . Elim H5. Intros. Assumption. Intros. Right . Elim H5. Intros. Assumption. Assumption. Intros. Cut (leads_to E (s_and p0 r) (s_or b (s_and q0 r))). Intros. Intros. Generalize (leads_to_cancelation E (s_and p0 r) b (s_and q0 r) (s_or (s_and r0 r) b) H5 H4). Intros. Apply leads_to_subst_r with q:=(s_or b (s_or (s_and r0 r) b)). Unfold everywhere s_iff s_or s_and. Intros. Split. Intros. Elim H7. Intros. Right . Assumption. Intros. Assumption. Intros. Elim H7. Intros. Right . Left . Assumption. Intros. Left . Assumption. Assumption. Apply leads_to_subst_r with q:=(s_or (s_and q0 r) b). Unfold everywhere s_iff s_and s_or. Intros. Split. Intros. Elim H5. Intros. Right . Assumption. Intros. Left . Assumption. Intros. Elim H5. Intros. Right . Assumption. Intros. Left . Assumption. Assumption. Intros. Generalize (leads_to_disjunction_2 E T [i:T](s_and (P i) r) (s_or (s_and q0 r) b) H2). Intros. Apply leads_to_implication_l with q:=(s_ex T [i:T](s_and (P i) r)). Unfold everywhere s_imp s_and s_or. Intros. Generalize (H3 s). Intros. Elim H6. Intros. Elim H5. Clear H5. Intros. Elim (H7 H5). Intros. Split with x. Auto. Assumption. Qed. (*T* Another rule to combine safety and liveness assertions is the following: A |leads_to| assertion can be strengthened on both sides by a state predicate which is known to be stable. *T*) Theorem leads_to_stable_conjunction : (E:view) (p,q,r:s_prop)(stable E r)->(leads_to E p q)-> (leads_to E (s_and p r) (s_and q r)). Intros. Generalize (leads_to_psp E p q r s_false). Intros. Apply leads_to_transitivity with q:=(s_or (s_and q r) s_false). Apply H1. Assumption. Apply stable_imp_unless. Assumption. Apply leads_to_imp. Unfold everywhere s_imp s_or s_and s_false. Intros. Elim H2. Intros. Auto. Intro. Elim H3. Qed. (*T* Using |leads_to_stable_conjunction| we can prove |rel_leads_to|, which completes our list of proof rules for relativized assertions. *T*) Theorem rel_leads_to : (E:view)(p,q,r:s_prop) (stable E r)-> (leads_to E (s_and r p) (s_imp r q))-> (leads_to E (s_and r p) (s_and r q)). Intros. Generalize (leads_to_stable_conjunction E ? ? ? H H0). Clear H H0. Intros. Apply leads_to_implication with 3:=H. Clear H. Unfold everywhere s_imp s_and. Tauto. Clear H. Unfold everywhere s_imp s_and. Tauto. Qed. (*BEGIN-H*) (* Often we have to reason about |leads_to| assertions in the presence of invariants. Remember that |(invariant E p r)| states that |r| is an inductive invariant of |E| with initialization condition |p|. More precisely, it says |p| implies |r| and |r| is stable. By the previous theorem we have |(leads_to E (s_and p r)| \linebreak |(s_and q r))| which is equivalent to |(leads_to p (s_and q r))| in view of the first premise. *) Theorem ind_invariant_imp_leads_to : (E:view)(p,q,r:s_prop) (ind_invariant E p r)-> (leads_to E p q)->(leads_to E p (s_and q r)). Intros E p q r I H0. Unfold ind_invariant in I. Elim I. Clear I. Intros. Generalize (leads_to_stable_conjunction E p q r H1). Intros. Apply (leads_to_implication_l E) with q:=(s_and p r). Unfold everywhere s_imp s_and. Intros. Split. Auto. Unfold everywhere s_imp in H1. Apply (H s H3). Apply H2. Auto. Qed. (*END-H*) (*T* We now present an alternative characterization of |leads_to| by means of the operator |strong_leads_to| introduced by the inductive definition below. The only difference w.r.t. the inductive definition of |leads_to| is that in the context of the other requirements transitivity is expressed by \begin{verbatim} (ensures E p q)->(strong_leads_to E q r) ->(strong_leads_to E p r) \end{verbatim} which in isolation is weaker than \begin{verbatim} (leads_to E p q)->(leads_to E q r)->(leads_to E p r)|. \end{verbatim} The advantage of |strong_leads_to| is that a stronger induction principle is available, due to the stronger premise |(ensures E p q)| instead of |(leads_to E p q)| in this implication. \begin{verbatim} Inductive strong_leads_to [E:view] : s_prop->s_prop->Prop := strong_leads_to_basis : (p,q:s_prop) (ensures E p q) -> (strong_leads_to E p q) | strong_leads_to_transitivity : (p,q,r:s_prop) (ensures E p q) -> (strong_leads_to E q r) -> (strong_leads_to E p r) | strong_leads_to_disjunction : (T:Type)(P:T->s_prop)(q:s_prop) ((i:T)(strong_leads_to E (P i) q)) -> (strong_leads_to E (s_ex T P) q). \end{verbatim} *T*) (*BEGIN-H*) Inductive strong_leads_to [E:view] : s_prop->s_prop->Prop := strong_leads_to_basis : (p,q:s_prop) (ensures E p q) -> (strong_leads_to E p q) | strong_leads_to_transitivity : (p,q,r:s_prop) (ensures E p q) -> (strong_leads_to E q r) -> (strong_leads_to E p r) | strong_leads_to_disjunction : (T:Type)(P:T->s_prop)(p,q:s_prop) ((i:T)(strong_leads_to E (P i) q)) -> (everywhere (s_iff p (s_ex T P))) -> (strong_leads_to E p q). (*END-H*) (*T* The equivalence between |strong_leads_to| and |leads_to| is stated by the following two implications. *T*) Theorem strong_leads_to_imp_leads_to :(E:view) (p,q:s_prop)(strong_leads_to E p q)->(leads_to E p q). Intros. Elim H. Intros. Apply leads_to_basis. Trivial. Intros. Cut (leads_to E p0 q0). Intros. Apply leads_to_transitivity with q:=q0. Trivial. Trivial. Apply leads_to_basis. Trivial. Intros. Apply leads_to_disjunction with P:=P. Intros. Trivial. Trivial. Qed. Theorem leads_to_imp_strong_leads_to :(E:view) (p,q:s_prop)(leads_to E p q)->(strong_leads_to E p q). Intro. Intro. Induction 1. Intros. Apply strong_leads_to_basis. Trivial. Intros. Generalize H3. Clear H3. Elim H0. Intros. Apply strong_leads_to_transitivity with q:=q1. Trivial. Trivial. Clear H H0 H1 H2. Intros. Specialize (H2 H3). Intros. Apply H0. Trivial. Intros. Apply strong_leads_to_disjunction with P:=P. Intros. Apply H4. Trivial. Trivial. Intros. Apply strong_leads_to_disjunction with P:=P. Intros. Apply H1. Trivial. Qed. (*T* As a consequence, the stronger induction principle of |strong_leads_to| is inherited by |leads_to|. It is formulated in the following theorem. \begin{verbatim} Theorem leads_to_strong_induction : (IH:view->s_prop->s_prop->Prop)(E:view) ((p,q:s_prop)(ensures E p q)->(IH E p q))-> ((p,q,r:s_prop) ((ensures E p q)->(leads_to E q r)-> (IH E p q)->(IH E q r)->(IH E p r)))-> ((T:Type)(P:T->s_prop)(p,q:s_prop) ((i:T)(leads_to E (P i) q))->((i:T)(IH E (P i) q))-> (IH E (s_ex T P) q))-> ((p,q:s_prop) (leads_to E p q)->(IH E p q)). \end{verbatim} *T*) (*BEGIN-H*) Theorem leads_to_strong_induction : (IH:view->s_prop->s_prop->Prop)(E:view) ((p,q:s_prop)(ensures E p q)->(IH E p q))-> ((p,q,r:s_prop) ((ensures E p q)->(leads_to E q r)-> (IH E p q)->(IH E q r)->(IH E p r)))-> ((T:Type)(P:T->s_prop)(p,q:s_prop) ((i:T)(leads_to E (P i) q))->((i:T)(IH E (P i) q))-> (everywhere (s_iff p (s_ex T P))) -> (IH E p q))-> ((p,q:s_prop) (leads_to E p q)->(IH E p q)). Intros. Cut (strong_leads_to E p q). Intros. Clear H2. Elim H3. Trivial. Intros. Apply H0 with q:=q0. Trivial. Apply strong_leads_to_imp_leads_to. Trivial. Apply H. Trivial. Trivial. Intros. Apply H1 with P:=P. Intros. Apply strong_leads_to_imp_leads_to. Trivial. Trivial. Trivial. Apply leads_to_imp_strong_leads_to. Trivial. Qed. (*END-H*) (*T* With this induction principle we can prove statements of the form \begin{verbatim} ((p,q:s_prop)(leads_to E p q)->(IH E p q)). \end{verbatim} Later, however, we will encounter a situation where we need to prove a statement with two |leads_to| premises, more precisely a statment of the form \begin{verbatim} ((p,q,p',q':s_prop) (leads_to E p q)->(leads_to E p' q')-> (IH E p q p' q')). \end{verbatim} To deal with goals like this it is in general convenient to introduce the following double induction principle. The proof is done by nested application of |leads_to_strong_induction|. \begin{verbatim} Theorem leads_to_double_induction : (IH:view->s_prop->s_prop->s_prop->s_prop->Prop)(E:view) ((p,q,p',q':s_prop) (ensures E p q)->(leads_to E p' q')-> (IH E p q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(ensures E p' q')-> (IH E p q p' q'))-> ((p,q,r,p',q',r':s_prop) ((ensures E p q)->(leads_to E q r)-> (ensures E p' q')->(leads_to E q' r')-> (IH E p q p' q')-> (IH E p q q' r')->(IH E q r p' q')-> (IH E q r q' r')-> (IH E p r q' r')->(IH E q r p' r')-> (IH E p r p' r')))-> ((T:Type)(P':T->s_prop)(p,q,p',q':s_prop) (leads_to E p q)-> ((i:T)(leads_to E (P' i) q'))-> ((i:T)(IH E p q (P' i) q'))-> (IH E p q (s_ex T P') q'))-> ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop) ((i:T)(leads_to E (P i) q))-> (leads_to E p' q')-> ((i:T)(IH E (P i) q p' q'))-> (IH E (s_ex T P) q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(leads_to E p' q')-> (IH E p q p' q')). \end{verbatim} *T*) (*BEGIN-H*) Theorem leads_to_double_induction : (IH:view->s_prop->s_prop->s_prop->s_prop->Prop)(E:view) ((p,q,p',q':s_prop) (ensures E p q)->(leads_to E p' q')-> (IH E p q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(ensures E p' q')-> (IH E p q p' q'))-> ((p,q,r,p',q',r':s_prop) ((ensures E p q)->(leads_to E q r)-> (ensures E p' q')->(leads_to E q' r')-> (IH E p q p' q')-> (IH E p q q' r')->(IH E q r p' q')-> (IH E q r q' r')-> (IH E p r q' r')->(IH E q r p' r')-> (IH E p r p' r')))-> ((T:Type)(P':T->s_prop)(p,q,p',q':s_prop) (leads_to E p q)-> ((i:T)(leads_to E (P' i) q'))-> ((i:T)(IH E p q (P' i) q'))-> (everywhere (s_iff p' (s_ex T P')))-> (IH E p q p' q'))-> ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop) ((i:T)(leads_to E (P i) q))-> (leads_to E p' q')-> ((i:T)(IH E (P i) q p' q'))-> (everywhere (s_iff p (s_ex T P)))-> (IH E p q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(leads_to E p' q')-> (IH E p q p' q')). Intros IH E H0 H1 H2 H3 H4. Cut (p,q:s_prop) (leads_to E p q) ->(p',q':s_prop)(leads_to E p' q')->(IH E p q p' q'). Clear H0 H1 H2 H3 H4. Intros. Apply H. Trivial. Trivial. Generalize (leads_to_strong_induction [E:view] [p,q:s_prop] (p',q':s_prop)(leads_to E p' q')->(IH E p q p' q') E). Intros. Apply H. Intros. Apply H0. Trivial. Trivial. Intros. Clear H. Apply H2 with 1:=H7 2:=H8 q':=p'0. Apply ensures_refl. Trivial. Generalize (H9 p'0 p'0). Intros. Apply H. Apply leads_to_refl. Apply H9. Trivial. Apply H1. Trivial. Apply ensures_refl. Apply H10. Trivial. Generalize H11. Generalize p'0 q'0. Clear H11. Clear p'0 q'0. Generalize (leads_to_strong_induction [E:view][p'0,q'0:s_prop](IH E p0 r p'0 q'0) E). Intros. Apply H. Intros. Apply H1. Apply leads_to_transitivity with q:=q0. Apply leads_to_basis. Trivial. Trivial. Trivial. Clear H. Intros. Clear H13. Clear H9. Generalize (H10 q1 r0 H12). Intros. Specialize (leads_to_basis E ? ? H). Intros. Specialize (leads_to_transitivity E p1 q1 r0 H13 H12). Intros. Generalize (H10 p1 r0 H15). Intros. Apply (H2 p0 q0 r p1 q1 r0). Trivial. Trivial. Trivial. Trivial. Apply H1. Apply leads_to_basis. Trivial. Trivial. Apply H0. Trivial. Trivial. Apply H10. Apply leads_to_basis. Trivial. Apply H10. Trivial. Trivial. Apply H10. Trivial. Clear H. Intros. Apply H3 with P':=P. Apply leads_to_transitivity with q:=q0. Apply leads_to_basis. Trivial. Trivial. Intros. Apply H. Trivial. Trivial. Trivial. Apply H10. Trivial. Intros. Apply H4 with P:=P. Trivial. Trivial. Intros. Apply H8. Trivial. Trivial. Trivial. Trivial. Qed. (*END-H*) (*T* The double induction principle is more general than necessary if the formula |(IH E p q p' q')| is logically symmetric w.r.t. to replacement of |(p,q)| by |(p',q')|. Actually, this will be the case in our application, which is the proof of the completion theorem. In the presence of such a symmetry |leads_to_double_| \linebreak |induction| can be simplified to |leads_to_symmetric_double_induction|, reducing the number of premises needed to obtain the same goal. \begin{verbatim} Theorem leads_to_symmetric_double_induction : (IH:view->s_prop->s_prop->s_prop->s_prop->Prop) (E:view) ((p,q,p',q':s_prop)(IH E p q p' q')-> (IH E p' q' p q))-> ((p,q,p',q':s_prop) (ensures E p q)->(leads_to E p' q')-> (IH E p q p' q'))-> ((p,q,r,p',q',r':s_prop) ((ensures E p q)->(leads_to E q r)-> (ensures E p' q')->(leads_to E q' r')-> (IH E p q p' q')-> (IH E p q q' r')->(IH E q r p' q')-> (IH E q r q' r')-> (IH E p r q' r')->(IH E q r p' r')-> (IH E p r p' r')))-> ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop) ((i:T)(leads_to E (P i) q))-> (leads_to E p' q')-> ((i:T)(IH E (P i) q p' q'))-> (IH E (s_ex T P) q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(leads_to E p' q')-> (IH E p q p' q')). \end{verbatim} *T*) (*BEGIN-H*) Theorem leads_to_symmetric_double_induction : (IH:view->s_prop->s_prop->s_prop->s_prop->Prop) (E:view) ((p,q,p',q':s_prop)(IH E p q p' q')-> (IH E p' q' p q))-> ((p,q,p',q':s_prop) (ensures E p q)->(leads_to E p' q')-> (IH E p q p' q'))-> ((p,q,r,p',q',r':s_prop) ((ensures E p q)->(leads_to E q r)-> (ensures E p' q')->(leads_to E q' r')-> (IH E p q p' q')-> (IH E p q q' r')->(IH E q r p' q')-> (IH E q r q' r')-> (IH E p r q' r')->(IH E q r p' r')-> (IH E p r p' r')))-> ((T:Type)(P:T->s_prop)(p,q,p',q':s_prop) ((i:T)(leads_to E (P i) q))-> (leads_to E p' q')-> ((i:T)(IH E (P i) q p' q'))-> (everywhere (s_iff p (s_ex T P)))-> (IH E p q p' q'))-> ((p,q,p',q':s_prop) (leads_to E p q)->(leads_to E p' q')-> (IH E p q p' q')). Intros. Apply leads_to_double_induction. Trivial. Intros. Apply H. Apply H0. Trivial. Trivial. Intros. Apply H1 with 1:=H5 2:=H6 3:=H7 4:=H8. Trivial. Trivial. Trivial. Trivial. Trivial. Trivial. Intros. Apply H. Apply H2 with P:=P'. Trivial. Trivial. Intros. Apply H. Auto. Trivial. Trivial. Trivial. Trivial. Qed. (*END-H*) (*T* Our next major goal is to prove the general completion rule given later by the theorem |leads_to_completion|, a rule that is very useful in practice. We will proceed using various intermediate statements, but first we will give an informal explanation. Basically the completion rule combines several |leads_to| assertions into a single one in a conjunctive fashion. Of course, we cannot expect to derive the usual conjunction rule for a family of |leads_to| assertions in the strict sense, since their right hand sides do not necessarily become true simultaneously. However, under some additional restrictions we can approximate this idea: Assume a finite family of assertions |(leads_to E (P i) (Q i))| and assume we know that |(unless E (Q i) r)|, i.e. the states satisfying |(Q i)| can only be left via |r|. Then we can conclude that |(s_all T P)| leads to |(s_all T Q)| or |r|. The disjunction on the right hand side corresponds to the two possible cases: Either all |(Q i)| will simultaneously become true at some time, or if this is not the case, at least one of the state predicates |(Q i)| will become true and then false again. But in this case |r| will become |true|. Actually, the Theorem |leads_to_completion| given later is a little bit more liberal: it has weaker premises |(leads_to E (P i) (s_or (Q i) r))|, because a situation where |r| becomes true immediately satisfies the right hand side of our |leads_to| conclusion. *T*) (*T* The proof in \cite{ChandyMisra88} is rather informal, since it relies on induction over the length of proofs which are themselves not formalized. The length of proofs remains a rather vague notion, in particular in view of the infinitary inductive definition of |leads_to|. Here we adopted a different approach: We will employ the double induction principle for |leads_to|, more precisely its symmetric specialization |leads_to_symmetric_double_induction|, which has been proved before. Using this induction principle we prove |leads_to_simple_conjunction|, and from this we obtain the binary completion theorem |leads_to_simple_completion|. Finally, we prove the general completion theorem |leads_to_completion| by another induction using an intermediate result |leads_to_completion_nat|. *T*) (*T* First we prove the base case of |leads_to_simple_conjunction| where both |leads_to| premises are actually |ensures| assertions. *T*) Lemma leads_to_simple_conjunction_basis : (E:view) (p,q,p',q',r:s_prop) (ensures E p q)-> (leads_to E p' q')-> (unless E q r)-> (unless E q' r)-> (leads_to E (s_and p p') (s_or (s_and q q') r)). Intros. Cut (ensures E p q). Intros ens. Unfold ensures in H. Elim H. Intros. Clear H. Specialize (unless_cancelation E p q r H3 H1). Intros. Specialize (leads_to_psp E ? ? ? ? H0 H). Intros. Cut (leads_to E (s_and p p') (s_or (s_and q' (s_or p q)) r)). Intros. Specialize (ensures_psp E ? ? ? ? ens H2). Intros. Specialize (leads_to_basis E ? ? H7). Intros. Clear H7. Generalize (leads_to_implication E (s_and p p') (s_and p p') (s_or (s_and q' (s_or p q)) r) (s_or (s_or r (s_and q q')) (s_and p q'))). Intros. Cut (leads_to E (s_and p p') (s_or (s_and q' (s_or p q)) r)) ->(leads_to E (s_and p p') (s_or (s_or r (s_and q q')) (s_and p q'))). Intros. Specialize (H9 H6). Intros. Clear H9. Specialize (leads_to_cancelation E ? ? ? ? H10 H8). Intros. Apply (leads_to_implication_r E) with 2:=H9. Unfold everywhere s_imp s_or s_and. Clear H9 H7 H10 H8 H5 H6 H H4 H3 H2 ens H1 H0. Tauto. Intros. Apply H7. Apply s_imp_p_p. Unfold everywhere s_imp s_or s_and. Clear H9 H7 H8 H5 H6 H H4 H3 ens H2 H1 H0. Tauto. Apply (leads_to_implication_l E) with q:=(s_and p' (s_or p q)). Unfold everywhere s_imp s_and s_or. Clear H9 H7 H8 H5 H6 H H4 H3 ens H2 H1 H0. Tauto. Trivial. Apply (leads_to_implication_l E) with q:=(s_and p' (s_or p q)). Unfold everywhere s_imp s_and s_or. Clear H5 H H4 H3 ens H2 H1 H0. Tauto. Trivial. Trivial. Qed. (*T* Next we prove |leads_to_simple_conjunction|. This theorem is obviously symmetric w.r.t. to replacement of |(p,q)| by |(p',q')|, which allows us to prove it using |leads_to_symmetric_double_induction|. *T*) Theorem leads_to_simple_conjunction : (E:view) (p,q,p',q',r:s_prop) (leads_to E p q)-> (leads_to E p' q')-> (unless E q r)-> (unless E q' r)-> (leads_to E (s_and p p') (s_or (s_and q q') r)). Intro. Intro. Generalize (leads_to_symmetric_double_induction [ppr:view] [p,q,p',q':s_prop] (r:s_prop) (unless E q r) ->(unless E q' r) ->(leads_to E (s_and p p') (s_or (s_and q q') r)) E). Intros. Apply H. Intros. Specialize (H4 ? H6 H5). Intros. Apply leads_to_implication with 3:=H7. Unfold everywhere s_imp s_and s_and. Intros. Elim H8. Intros. Auto. Unfold everywhere s_imp s_or s_and. Intros. Elim H8. Intros. Elim H9. Auto. Auto. Intros. Apply leads_to_simple_conjunction_basis. Trivial. Trivial. Trivial. Trivial. Intros. Clear H. Clear H8 H9 H10. Specialize (H11 r1 H14 H15). Specialize (H12 r1 H14 H15). Specialize (H13 r1 H14 H15). Clear H11 H12 H13. Intros. Cut (unless E p0 q0). Intros. Specialize (ensures_conjunction E p0 p'0 q0 q'0 H10 H6). Intros. Specialize (leads_to_basis E ? ? H11). Intros. Clear H11. Cut (leads_to E (s_and p'0 q0) (s_or (s_and r0 r') r1)). Intros. Specialize (leads_to_ternary_disjunction E (s_and p0 q'0) (s_and p'0 q0) (s_and q0 q'0) ? H8 H11 H9). Intros. Apply leads_to_transitivity with 1:=H12 2:=H13. Apply leads_to_implication_l with 2:=H. Unfold everywhere s_imp s_and. Intros. Elim H11. Intros. Auto. Unfold ensures in H4. Elim H4. Auto. Intros. Clear H. Cut (i:T)(leads_to E (s_and (P i) p'0) (s_or (s_and q0 q'0) r0)). Intros. Clear H6. Clear H0 H1 H2 H3. Apply (leads_to_disjunction E T [i:T](s_and (P i) p'0)). Trivial. Unfold everywhere s_iff s_and s_ex. Unfold everywhere s_iff s_ex in H7. Intros. Specialize (H7 s). Intros. Elim H0. Intros. Split. Intros. Elim H3. Intros. Elim (H1 H6). Intros. Split with x. Auto. Intros. Split. Apply H2. Elim H3. Intros. Split with x. Elim H6. Auto. Elim H3. Intros. Elim H6. Auto. Intros. Apply H6. Trivial. Trivial. Trivial. Trivial. Trivial. Trivial. Qed. (*T* By application of |unless_simple_disjunction| and |leads_to_simple_| \linebreak |conjunction| to the previous result we obtain the binary version of the completion theorem which has two |leads_to| premises. *T*) Theorem leads_to_simple_completion : (E:view) (p,q,p',q',r:s_prop) (leads_to E p (s_or q r))-> (leads_to E p' (s_or q' r))-> (unless E q r)-> (unless E q' r)-> (leads_to E (s_and p p') (s_or (s_and q q') r)). Intros. Specialize (unless_refl E r). Intros. Generalize (unless_simple_disjunction E ? ? ? ? H1 H3). Intro. Generalize (unless_simple_disjunction E ? ? ? ? H2 H3). Intros. Generalize (leads_to_simple_conjunction E ? ? ? ? ? H H0 H4 H5). Intros. Apply leads_to_implication_r with 2:=H6. Trivial. Unfold everywhere s_and s_or s_imp. Intros. Clear H H0 H1 H2 H3 H4 H5 H6. Tauto. Qed. (*T* The general completion theorem |leads_to_completion| which has an arbitrary finite family of |leads_to| premises can be reduced to the following special case, where the family is indexed by an initial interval of the natural numbers. The proof is done by induction over the bound |b|, using the previous result for the binary case. *T*) Theorem leads_to_completion_nat : (E:view) (b:nat)(P,Q:nat->s_prop)(r:s_prop) ((i:nat)(lt i b)->(leads_to E (P i) (s_or (Q i) r)))-> ((i:nat)(lt i b)->(unless E (Q i) r))-> (leads_to E (s_all_nat b P) (s_or (s_all_nat b Q) r)). Intros. Generalize H. Generalize H0. Clear H H0. Generalize b. Clear b. Induction b. Intros. Apply (leads_to_implication_r E) with q:=s_true. Unfold everywhere s_imp s_true s_or s_all_nat. Intros. Left . Intros. Elim (lt_n_O i H2). Apply leads_to_true. Intros. Cut (i:nat)(lt i n)->(unless E (Q i) r). Intros. Cut (i:nat)(lt i n)->(leads_to E (P i) (s_or (Q i) r)). Intros. Specialize (H H2 H3). Intros. Clear H. Cut (leads_to E (P n) (s_or (Q n) r)). Intros. Cut (unless E (s_all_nat n Q) r). Intros. Cut (unless E (Q n) r). Intros. Generalize (leads_to_simple_completion E ? ? ? ? ? H4 H H5 H6). Intros. Apply leads_to_implication with 3:=H7. Unfold everywhere s_imp s_all_nat s_and. Intros. Generalize (H8 n). Intros. Split. Intros. Apply H8. Apply lt_S. Trivial. Apply H9. Apply lt_n_Sn. Unfold everywhere s_imp s_or s_and s_all_nat. Intros. Elim H8. Intros. Left . Intros. Elim H9. Intros. Specialize (lt_n_Sm_le i n H10). Intros. Elim (le_lt_or_eq i n H13). Intros. Apply H11. Trivial. Intros. Rewrite H14. Trivial. Intros. Right . Trivial. Apply H0. Apply lt_n_Sn. Apply unless_left_big_conjunction. Trivial. Apply H1. Apply lt_n_Sn. Intros. Apply H1. Apply lt_S. Trivial. Intros. Apply H0. Apply lt_S. Trivial. Qed. (*T* Now the proof of the general completion theorem |leads_to_completion| follows by exploiting the definition of |(finite T)|, which expresses that |T| is of finite cardinality. *T*) Theorem leads_to_completion : (E:view) (T:Type)(finite T)->(P,Q:T->s_prop)(r:s_prop) ((i:T)(leads_to E (P i) (s_or (Q i) r)))-> ((i:T)(unless E (Q i) r))-> (leads_to E (s_all T P) (s_or (s_all T Q) r)). Intros E T F P Q r. Unfold finite in F. Elim F. Intro b. Intro. Clear F. Unfold card_le in H. Elim H. Intro hh. Intro. Clear H. Intros. Cut (leads_to E (s_all_nat b [n:nat](P (hh n))) (s_or (s_all_nat b [n:nat](Q (hh n))) r)). Intros. Apply leads_to_implication with 3:=H2. Unfold everywhere s_imp s_all s_all_nat. Intros. Apply H3. Unfold everywhere s_imp s_or s_all_nat s_all. Intros. Elim H3. Intros. Left . Intros. Elim (H0 t). Intros. Elim H5. Intros. Rewrite <- H7. Apply H4. Trivial. Intros. Right . Trivial. Apply leads_to_completion_nat. Trivial. Intros. Apply H1. Qed. (*T* In addition to our previous characterization of |leads_to| by |strong_leads_to|, we now give another characterization by means of |leads_to_pre|, which is again defined inductively in a way very similar to the definition of |strong_leads_to|. The only difference is that |(strong_leads_to E)| is an inductively defined {\em binary relation} on state predicates, whereas |(leads_to_pre E r)| is an inductively defined {\em set} of state predicates. The intention is that |(leads_to_pre E r)| contains those state predicates which are |strong_leads_to| preconditions of some fixed state predicate |r|. \begin{verbatim} Inductive leads_to_pre [E:view;r:s_prop] : s_prop->Prop := leads_to_pre_basis : (p:s_prop) (ensures E p r) -> (leads_to_pre E r p) | leads_to_pre_transitivity : (p,q:s_prop) (ensures E p q) -> (leads_to_pre E r q) -> (leads_to_pre E r p) | leads_to_pre_disjunction : (T:Type)(P:T->s_prop) ((i:T)(leads_to_pre E r (P i))) -> (leads_to_pre E r (s_ex T P)). \end{verbatim} *T*) (*BEGIN-H*) Inductive leads_to_pre [E:view;r:s_prop] : s_prop->Prop := leads_to_pre_basis : (p:s_prop) (ensures E p r) -> (leads_to_pre E r p) | leads_to_pre_transitivity : (p,q:s_prop) (ensures E p q) -> (leads_to_pre E r q) -> (leads_to_pre E r p) | leads_to_pre_disjunction : (T:Type)(P:T->s_prop) ((i:T)(leads_to_pre E r (P i))) -> (p:s_prop)(everywhere (s_iff p (s_ex T P))) -> (leads_to_pre E r p). (*END-H*) (*T* Indeed, |(leads_to_pre E q p)| is equivalent to |(strong_leads_to E p q)| and hence equivalent to |(leads_to E p q)| as it is proved in the following two theorems. The main reason to set up different characterizations of |leads_to| is that they all give rise to different induction principles. Furthermoere, the definition as an inductive set is structurally simpler than the definitions of |leads_to| and |strong_leads_to| given before. It shows that the definition of |strong_leads_|\linebreak|to| can be cast into a form which is a parameterized inductive definition (|E| and |r| are parameters) of a set of state predicates. *T*) Theorem leads_to_pre_imp_leads_to : (E:view)(p,q:s_prop) (leads_to_pre E q p) -> (leads_to E p q). Intros. Elim H. Intros. Constructor 1. Assumption. Intros. Cut (leads_to E p0 q0). Intros. Apply leads_to_transitivity with q:=q0. Assumption. Assumption. Constructor 1. Assumption. Intros. Constructor 3 with P:=P. Assumption. Assumption. Qed. Theorem leads_to_imp_leads_to_pre : (E:view)(p,q:s_prop) (leads_to E p q) -> (leads_to_pre E q p). Intros. Elim H. Intros. Constructor 1. Assumption. Intros. Elim H1. Intros. Constructor 2 with q:=q0. Assumption. Assumption. Intros. Constructor 2 with q:=q1. Assumption. Assumption. Intros. Constructor 3 with P:=P. Assumption. Assumption. Intros. Constructor 3 with P:=P. Assumption. Assumption. Qed. (*T* Given a state predicate |p| that is satisfied for some state, the assertion |(leads_to|\linebreak|E p s_false)| cannot hold; otherwise a contradiction arises, since |s_false| would have to become true eventually. The proof is done by induction on the |leads_to| premise, using the induction principle provided by |leads_to_pre|. *T*) Theorem leads_to_impossible : (E:view) (p:s_prop)(leads_to E p s_false)->(everywhere (s_not p)). Intros. Generalize (leads_to_imp_leads_to_pre E p s_false H). Intros. Clear H. Elim H0. Intros. Apply ensures_false with E:=E. Assumption. Intros. Apply ensures_false with E:=E. Apply ensures_subst_r with q:=q. Unfold everywhere s_iff s_false. Unfold everywhere s_not in H2. Intros. Generalize (H2 s). Intros. Split. Unfold not in H3. Assumption. Intro. Elim H4. Assumption. Intros. Unfold everywhere s_not s_ex. Unfold everywhere s_not in H1. Intros. Unfold not. Intros. Generalize (H2 s). Intros. Elim H4. Intros. Generalize (H5 H3). Intros. Elim H7. Intros i. Intros. Generalize (H1 i s). Intros. Apply H9. Assumption. Qed. (*T* Finally, we turn to another family of proof rules addressing the fact that induction is the most important proof technique for |leads_to| assertions. In contrast to structural induction over |leads_to| assertions, that we used before as a metalogical tool to derive a number of generic proof rules, we will now discuss object-level induction rules, which are typically employed to prove a particular fixed |leads_to| assertion in a concrete system. We begin with a general proof rule for well-founded induction, and then give a typical specialization for induction over the type |nat| of natural numbers. The general well-founded induction rule |leads_to_induction| assumes that the induction is carried out over a state function |variant| mapping states into some domain, assuming a well-founded ordering |less| on this domain which is not necessarily total. For this purpose we use the predicate |well_founded| from the module |WfT| from the mathematical library. The goal of the subsequent proof rule is that |p| leads to |q|. To guarantee this assertion we use the following condition as a premise: If |p| holds and the value of |variant| equals |m| then there are two possibilities: either (1) we will eventually reach a state satisfying |q|, in this case the conclusion is immediately justified, or (2) we will eventually reach a state satisfying |p| again, but this time with the value of |variant| being decreased w.r.t. |m|. Obviously, we are concerned with a loop where choice (2) can be taken only finitely often, due to the well-foundedness condition. So choice (1) has to be taken eventually, and |q| will then be satisfied. *T*) Theorem leads_to_induction : (E:view) (T:Type)(less:T->T->Prop)(variant:st->T) (WfT_well_founded T less)-> (p,q:s_prop) ((m:T) (leads_to E (s_and p [s:st] (variant s) == m) (s_or (s_and p [s:st] (less (variant s) m)) q)))-> (leads_to E p q). Intros. Cut (m:T)(leads_to E (s_and p [s:st](variant s)==m) q). Intros. Generalize (leads_to_disjunction_2 E T [m:T](s_and p [s:st](variant s)==m) q). Intros. Generalize (H2 H1). Intros. Clear H2. Apply leads_to_implication_l with q:=(s_ex T [m:T](s_and p [s:st](variant s)==m)). Unfold everywhere s_imp s_ex s_and. Intros. Split with (variant s). Split. Assumption. Reflexivity. Assumption. Intros. Apply WfT_well_founded_ind with A:=T R:=less P:=[m:T](leads_to E (s_and p [s:st](variant s)==m) q). Assumption. Intros. Generalize (leads_to_disjunction_2 E (sigT ? [y:T](less y x))). Intros. Generalize (H2 [i:(sigT ? [y:T](less y x))] (s_and p [s:st](variant s)==(projT1 ? ? i))). Intros. Generalize (H3 q). Intros. Clear H2 H3. Cut (leads_to E (s_ex (sigT ? [y:T](less y x)) [i:(sigT ? [y:T](less y x))] (s_and p [s:st](variant s)==(projT1 T [y:T](less y x) i))) q). Intros. Cut (leads_to E q q). Intros. Generalize (leads_to_small_disjunction E (s_ex (sigT ? [y:T](less y x)) [i:(sigT ? [y:T](less y x))] (s_and p [s:st](variant s)==(projT1 T [y:T](less y x) i))) q q q H2 H3). Intros. Apply leads_to_transitivity with q:=(s_or (s_ex (sigT ? [y:T](less y x)) [i:(sigT ? [y:T](less y x))] (s_and p [s:st](variant s)==(projT1 T [y:T](less y x) i))) q). Clear H4 H2 H3 H5. Generalize (H0 x). Clear H0. Intros. Apply leads_to_implication_r with q:=(s_or (s_and p [s:st](less (variant s) x)) q). Unfold everywhere s_imp s_or s_and s_ex. Intros. Elim H2. Intros. Elim H3. Intros. Left . Split with (existT T [y:T](less y x) (variant s) H5). Split. Assumption. Reflexivity. Intros. Right . Assumption. Assumption. Apply leads_to_implication_r with q:=(s_or q q). Unfold everywhere s_imp s_or. Intros. Elim H6. Auto. Auto. Assumption. Apply leads_to_refl. Clear H4. Apply (leads_to_disjunction_2 E (sigT ? [y:T](less y x))). Intros. Elim i. Intros y' H'. Generalize (H1 y' H'). Intros. Auto. Qed. (*BEGIN-H*) (* The following induction rule is a specialization of the preceding one: Instead of a general state function |variant| we use a system variable |M|. *) (* Theorem leads_to_var_induction : (E:view) (M:var)(less:(var_type M)->(var_type M)->Prop) (WfT_well_founded (var_type M) less)-> (p,q:s_prop) ((m:(var_type M)) (leads_to E (s_and p [s:st] (s M) == m) (s_or (s_and p [s:st] (less (s M) m)) q)))-> (leads_to E p q). Intros. Apply (leads_to_induction E (var_type M) less [s:st](s M)). Trivial. Trivial. Qed. *) (*END-H*) (*T* Now we instantiate |less| by |lt|, the usual well-founded strict total order on |nat|, and obtain the following induction rule for natural numbers as a special case. \begin{verbatim} Theorem leads_to_nat_induction : (E:view) (variant:st->nat) (p,q:s_prop) ((m:nat) (leads_to E (s_and p [s:st] (variant s) == m) (s_or (s_and p [s:st] (lt (variant s) m)) q)))-> (leads_to E p q). \end{verbatim} *T*) (*BEGIN-H*) Theorem leads_to_nat_induction : (E:view) (variant:st->nat) (p,q:s_prop) ((m:nat) (leads_to E (s_and p [s:st] (variant s) = m) (s_or (s_and p [s:st] (lt (variant s) m)) q)))-> (leads_to E p q). (*END-H*) Intros E v p q. Intros. Apply (leads_to_induction E nat lt v lt_wf p q). Auto. Intros. Apply leads_to_implication_l with 2:=(H m). Unfold everywhere s_imp s_and. Intros. Elim H0. Intros. Split. Trivial. Rewrite H2. Reflexivity. Qed. (*T* Supplementing the previous induction principle, where the value decreases during the execution, we provide a reverse induction principle, where the variant increases. In this case we have to require some upper bound for the variant, which is specified by |maximum|. In the proof we define a decreasing variant |[s:st](minus maximum (variant s))| and use the previous induction rule for natural numbers. *T*) Theorem leads_to_rev_nat_induction : (E:view) (variant:st->nat)(maximum:nat)(p,q:s_prop) (everywhere (s_imp p [s:st](le (variant s) maximum)))-> ((m:nat)(le m maximum)-> (leads_to E (s_and p [s:st] m = (variant s)) (s_or (s_and p [s:st] (lt m (variant s))) q)))-> (leads_to E p q). Intros. Apply (leads_to_nat_induction E [s:st](minus maximum (variant s)) p q). Intros. Elim (le_or_lt m maximum). Intros L. Cut (le (minus maximum m) maximum). Intros L'. Generalize (H0 (minus maximum m) L'). Intros. Clear H0. Apply leads_to_implication with 3:=H1. Unfold everywhere s_imp s_and. Intros. ECI H0. Split. Assumption. Generalize (H s H0). Intros. Generalize (le_plus_minus ? ? H3). Intros. Rewrite H4. Rewrite H2. Rewrite (plus_sym (variant s) m). Apply minus_plus. Unfold everywhere s_imp s_and s_or. Intros. ECI H0. ECI H0. Left . Split. Trivial. Apply lt_minus_imp_lt_minus. Trivial. Apply (H s H0). Trivial. Auto. Intros. Apply le_minus. Intros. Apply (leads_to_implication_l E (s_and p [s:st](minus maximum (variant s))=m) s_false (s_or (s_and p [s:st](lt (minus maximum (variant s)) m)) q)). Unfold everywhere s_imp s_and s_false. Intros. Generalize (lt_imp_lt_minus_l (variant s) maximum m). Intros. GCI H3 H1. ECI H2. Rewrite H4 in H3. Apply (lt_n_n ? H3). Apply leads_to_false. Qed.