(*T* \usection{Extending the Example}\label{sect-comp-example} *T*)

(*T* To illustrate the use of our compositionality results in a
concrete setting we extend the common meeting time example, which
involves two persons represented by functions |f| and |g|, by adding
another person represented by a function |h|. *T*)

(*BEGIN-H*)

Load init.

Variables f,g : nat->nat.
Axiom f_is_ascending : (m:nat)(le m (f m)).
Axiom g_is_ascending : (m:nat)(le m (g m)).
Axiom f_is_monotone : (m,n:nat)(le m n)->(le (f m) (f n)).
Axiom g_is_monotone : (m,n:nat)(le m n)->(le (g m) (g n)).

Definition common := [t:nat] (f t)=t /\ (g t)=t.

Variable cmt : nat.
Axiom cmt_exists : (common cmt).
Axiom cmt_smallest : (m:nat)(common m)->(le cmt m).

(*END-H*)

Variables h : nat->nat.

Axiom h_is_ascending : (m:nat)(le m (h m)).
Axiom h_is_monotone : (m,n:nat)(le m n)->(le (h m) (h n)).
Axiom h_accepts_cmt : (h cmt) = cmt .

Theorem h_rem_below_cmt : (m:nat)(le m cmt)->(le (h m) cmt) .

Intros.
Rewrite <- h_accepts_cmt.
Apply h_is_monotone.
Trivial.
Qed.

(*T* As formulated above, we assume that the new person at least agrees
with the common meeting time |cmt|, i.e. with the common meeting time of
the first two persons. This ensures that adding the new person to the
existing system does not affect the properties, especially Theorem
|CMT_L14|, proved earlier, although the executions of the new system
can be quite different. *T*)

(*BEGIN-H*)

Inductive var : Type := time : var.

Definition vars := (S O).

Definition ith_var := [i:nat] time.

Theorem var_finite : (v:var)
  (ExT [i:nat] (lt i vars) /\ (ith_var i)==v).

Induction v.
Exists  O.
Split.
Unfold vars.
Apply lt_n_Sn.
Unfold ith_var.
Reflexivity.
Qed.

Theorem var_eq_dec : (v,v':var){(v==v')}+{~(v==v')}.

Induction v.
Induction v'.
Left.
Reflexivity.
Qed.

Inductive type_name : Type := unat : type_name.

Definition type := [n:type_name]
  Cases n of unat => nat end.

Definition var_type_name := [v:var]
  Cases v of time => unat end.

Definition var_type := [v:var] (type (var_type_name v)).

Definition st := (v:var)(var_type v).

Load var_state_ops.

(*END-H*)

(*T* While preserving the original component |CMT|, we represent the
additional person by an action |update_h| in the new component
|CMT'|. The definitions of |act| and |effect| are extended
correspondingly. It is interesting to note that there is no need to
assume weak fairness for |update_h|. *T*)

Inductive act : Type :=
  update_f : act | update_g : act | update_h : act.

Definition effect := [e:act] 
  Cases e of 
          update_f => [s:st] (assign s time (f (s time)))
        | update_g => [s:st] (assign s time (g (s time)))
        | update_h => [s:st] (assign s time (h (s time)))
  end.

(*BEGIN-H*)

Definition trans := [e:act][s,s':st]
  (s' == (effect e s)) .

Definition view := act->Prop.

(*END-H*)

Definition CMT := 
  (Add act (Add act (Empty_set act) update_g) update_f) .

Definition CMT' := 
  (Add act (Empty_set act) update_h) .

(*BEGIN-H*)

Definition CMT'' := 
  (Add act (Add act (Add act (Empty_set act) 
  update_h) update_g) update_f) .

Definition wf := 
  (Add (set act) (Add (set act) (Add (set act) 
  (Empty_set (set act))
  (Empty_set act))
  (Singleton act update_f))
  (Singleton act update_g)).

Theorem wf_contains_empty_set : 
  (In (set act) wf (Empty_set act)).

Unfold wf.
Auto with v62.
Qed.

Load state_pred.
Load safety.
Load liveness.
Load var_state_pred.
Load var_elim.

Theorem enabled_vacuous : (e:act)(s:st)(enabled e s) .

Intros.
Unfold enabled.
Split with (effect e s).
Unfold trans.
Trivial.
Qed.

Lemma hoare_sc : (e:act)(p,q:s_prop)
  ((s:st)(enabled e s)->(p s)->(q ((effect e) s))) ->
  (hoare e p q).

Unfold hoare.
Unfold trans.
Intros.
Rewrite H0.
Apply H.
Apply enabled_vacuous.
Trivial.
Qed.

Theorem sys_contains_update_g :
  (Included act (Singleton act update_g) CMT).

Unfold Included CMT.
Intro t.
Intros.
Generalize (Singleton_inv ? ? ? H).
Intros.
Rewrite <- H0.
Auto with v62.
Qed.

Theorem sys_contains_update_f :
  (Included act (Singleton act update_f) CMT).

Unfold Included CMT.
Intro t.
Intros.
Generalize (Singleton_inv ? ? ? H).
Intros.
Rewrite <- H0.
Auto with v62.
Qed.

Theorem CMT'_contains_update_h :
  (Included act (Singleton act update_h) CMT').

Unfold Included CMT'.
Intro t.
Intros.
Generalize (Singleton_inv ? ? ? H).
Intros.
Rewrite <- H0.
Auto with v62.
Qed.

Lemma CMT_S1 : (m:nat)
  (co CMT ([s:st] (eq nat (s time) m))
             ([s:st] (le (s time) (f m)) \/ 
                       (le (s time) (g m)))).

Intros.
Unfold CMT.
Unfold co.
Intros.
Apply hoare_sc.
Intros.
Elim H.
Intros.
Elim H2.
Intros.
Elim H3.

Intros.
Specialize (Singleton_inv ? ? ? H3).
Clear H3.
Intro.
Rewrite <- H3.
Right.
Simpl.
Rewrite assign_changed.
Rewrite H1.
Apply le_n.

Intros.
Left.
Specialize (Singleton_inv ? ? ? H2).
Clear H2.
Intro.
Rewrite <- H2.
Simpl.
Rewrite assign_changed.
Rewrite H1.
Apply le_n.
Qed.


Lemma CMT_S2 : (n:nat)(co CMT
  [s:st]((common n)->(le (s time) n))
  (s_ex ? [m:nat] 
    [s:st]((common n)->(le m n))/\
            ((le (s time) (f m))\/(le (s time) (g m))))).

Intros.
Generalize (elimination CMT time
             [s:st](common n)->(le (s time) n)
             [m:nat]
              [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intro.
Cut (v:var)
     ~v==time
      ->(independent [s:st](common n)->(le (s time) n) v).
Intro.
Cut (m:(var_type time))
     (co CMT [s:st](eq nat (s time) m)
       [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intro.
Cut (m:(var_type time))
     (co CMT [s:st](s time)==m
       [s:st](le (s time) (f m))\/(le (s time) (g m))).
Intros.
Generalize (H H0 H2).
Clear H2.
Clear H.
Intro.
Apply co_implication_r
 with q:=(s_ex (var_type time)
           [m:(var_type time)]
            (s_and
              (subst [s:st](common n)->(le (s time) n) time m)
              [s:st](le (s time) (f m))\/(le (s time) (g m)))).
Unfold everywhere s_imp s_and subst var_type.
Unfold type var_type_name.
Unfold s_ex.
Intros.
Elim H2.
Intros t H3.
Split with t.
Elim H3.
Intros.
Split.
Intro.
Generalize (H4 H6).
Rewrite assign_changed.
Intro.
Assumption.
Assumption.
Assumption.
Intros.
Apply co_implication_l with 2:=(H1 m).
Unfold everywhere s_imp.
Intros.
Rewrite H2.
Reflexivity.
Unfold var_type.
Unfold var_type_name type.
Exact CMT_S1.
Induction v.
Intro.
Apply False_ind.
Unfold not in H0.
Apply H0.
Reflexivity.
Qed.


Lemma CMT_S3 : (n:nat)(stable CMT
             ([s:st] (common n) -> (le (s time) n))).

Intro.
Unfold stable.
Apply co_implication_r with q:=(s_ex ?
                                   [m:nat]
                                    [s:st]
                                     ((common n)->(le m n))
                                     /\((le (s time) (f m))
                                        \/(le (s time) (g m)))).
Unfold everywhere s_imp s_ex.
Intros.
Elim H.
Intros t H1.
Clear  H.
Elim H1.
Intros.
Clear  H1.
Generalize (H H0).
Intro.
Generalize (f_is_monotone t n H1).
Intro.
Generalize (g_is_monotone t n H1).
Intro.
Unfold common in H0.
Elim H0.
Intros.
Rewrite H5 in H3.
Rewrite H6 in H4.
Elim H2.
Intro.
Apply le_trans with (f t).
Assumption.
Assumption.
Intro.
Apply le_trans with (g t).
Assumption.
Assumption.
Apply CMT_S2.
Qed.


Lemma CMT_S4 : (n:nat)
  (ind_invariant CMT [s:st](eq nat (s time) O)
     ([s:st] (common n) -> (le (s time) n))).

Intro.
Unfold ind_invariant.
Split.
Unfold everywhere s_imp.
Intros.
Rewrite -> H.
Apply le_O_n.
Apply CMT_S3.
Qed.


Theorem CMT_S5 : (ind_invariant CMT 
  [s:st](s time)=O [s:st](le (s time) cmt)).

Generalize (CMT_S4 cmt).
Intros.
Apply ind_invariant_subst with 3:=H.
Unfold everywhere s_imp.
Auto with v62.
Unfold everywhere s_iff.
Intros.
Split.
Intros.
Apply H0.
Apply cmt_exists.
Intros.
Trivial.
Qed.


Theorem CMT_S6 : (m:nat)
  (co CMT [s:st](eq nat m (s time)) 
             [s:st](le m (s time))).

Unfold CMT.
Unfold co.
Intros.
Apply hoare_sc.
Intros.
Elim H.
Intros.
Elim H2.
Intros.
Elim H3.

Intros.
Specialize (Singleton_inv ? ? ? H3).
Clear H3.
Intro.
Rewrite <- H3.
Simpl.
Rewrite (assign_changed s time (g (s time))).
Rewrite <- H1.
Apply g_is_ascending.

Intros.
Specialize (Singleton_inv ? ? ? H2).
Clear H2.
Intro.
Rewrite <- H2.
Simpl.
Rewrite (assign_changed s time (f (s time))).
Rewrite <- H1.
Apply f_is_ascending.
Qed.


Definition cmt_variant := [s:st](s time).


Lemma CMT_S7 : (stable CMT [s:st](le (cmt_variant s) cmt)).

Unfold cmt_variant.
Generalize (CMT_S3 cmt).
Intros.
Apply (stable_subst CMT) with p:=[s:st]
                                     (common cmt)->(le (s time) cmt).
Unfold everywhere s_iff.
Intros.
Split.
Intros.
Apply (H0 cmt_exists).
Intros.
Auto with v62.
Auto with v62.
Qed.


Lemma CMT_S8 : (m:nat)
  (unless CMT
     (s_and [s:st](le (s time) cmt) 
            [s:st](eq nat m (s time)))
     (s_or
       (s_and [s:st](le (s time) cmt) 
              [s:st](lt m (s time)))
       [s:st](eq nat (s time) cmt))).

Intros.
Generalize (co_stable_conjunction CMT [s:st](eq nat m (s time))
             [s:st](le m (s time)) [s:st](le (cmt_variant s) cmt)
             CMT_S7 (CMT_S6 m)).
Intros.
Unfold unless.
Apply co_implication with p':=(s_and [s:st](eq nat m (s time))
                                  [s:st](le (cmt_variant s) cmt)) q:=(
s_and [s:st](le m (s time)) [s:st](le (cmt_variant s) cmt)).
Unfold everywhere s_imp s_or s_and.
Intros.
Unfold cmt_variant.
Elim H0.
Intros.
Elim H1.
Intros.
Split.
Auto with v62.
Auto with v62.
Unfold everywhere s_imp s_and s_or.
Intros.
Elim H0.
Intros.
Clear  H H0.
Unfold cmt_variant in H2.
Elim (eq_nat_dec m (s time)).
Intros.
Left.
Split.
Auto with v62.
Auto with v62.
Intros.
Right.
Left.
Split.
Auto with v62.
Elim (le_lt_or_eq m (s time)).
Intros.
Auto with v62.
Intros.
Elim y.
Auto with v62.
Auto with v62.
Auto with v62.
Qed.


Theorem CMT_L9 : (m:nat) (transient CMT 
  [s:st](not (common (s time))) /\ (eq nat m (s time))).

Intros.
Unfold transient.
Unfold transient.
Elim (eq_nat_dec m (f m)).
Intros.
Split with (Singleton ? update_g).
Split.
Unfold wf.
Auto with v62.

Split.
Exact sys_contains_update_g.

Unfold sco.
Intros.
Unfold en.
Split.
Intros.
Split with update_g.
Split.
Auto with v62.

Apply enabled_vacuous.

Unfold co.
Intro.
Intro.
Apply hoare_sc.
Intros.
Unfold s_not.
Unfold not.
Specialize (Singleton_inv ? update_g e H).
Intros.
Rewrite <- H2 in H3.
Unfold effect in H3.
Unfold common in H3.
Elim H1.
Intros.
Unfold common in H4.
Elim H3.
Clear H0.
Intros.
Clear H3.
Apply H0.
Clear H0.
Rewrite <- H6.
Split.
Auto.

Rewrite <- H5 in H6.
Rewrite (assign_changed s time (g m)) in H6.
Auto.

Intros.
Split with (Singleton ? update_f).
Split.
Unfold wf.
Auto with v62.

Split.
Exact sys_contains_update_f.

Unfold sco.
Split.
Unfold en.
Intros.
Split with update_f.
Split.
Auto with v62.

Apply enabled_vacuous.

Unfold co.
Intros.
Apply hoare_sc.
Intros.
Specialize (Singleton_inv ? update_f e H).
Clear H.
Intros.
Unfold s_not.
Unfold not.
Intros.
Elim H2.
Clear H2.
Intros.
Rewrite <- H in H2.
Rewrite <- H in H3.
Clear H.
Unfold effect in H2.
Unfold effect in H3.
Rewrite assign_changed in H2.
Rewrite assign_changed in H3.
Elim H1.
Clear H1.
Intros.
Rewrite <- H1 in H3.
Apply (y H3).
Qed.


Lemma CMT_L10 : (m:nat) (transient CMT 
  [s:st]((lt (s time) cmt) /\ (eq nat m (s time)))).

Intros.
Apply transient_implication with p:=[s:st]
                                       ~(common (s time))
                                       /\(eq nat m (s time)).
Apply CMT_L9.
Unfold everywhere s_imp.
Intros.
Elim H.
Clear  H.
Intros.
Split.
Unfold not.
Intros.
Generalize (cmt_smallest (s time) H1).
Intros.
Generalize (le_lt_trans cmt (s time) cmt H2 H).
Intros.
Apply (lt_n_n cmt H3).
Auto with v62.
Qed.


Lemma CMT_L11 : (m:nat)(transient CMT
   (s_and (s_and [s:st](le (s time) cmt) 
                 [s:st](eq nat m (s time)))
     (s_not
       (s_or
         (s_and [s:st](le (s time) cmt) 
                [s:st](lt m (s time)))
         [s:st](eq nat (s time) cmt))))).

Intros.
Apply transient_implication with p:=[s:st]
                                       (lt (s time) cmt)
                                       /\(eq nat m (s time)).
Apply CMT_L10.
Unfold everywhere s_imp s_and s_or s_not.
Intros.
Elim H.
Clear  H.
Intros.
Elim H.
Clear  H.
Intros.
Split.
Elim (eq_nat_dec (s time) cmt).
Intros.
Elim H0.
Right.
Auto with v62.
Intros.
Elim (le_lt_or_eq (s time) cmt H).
Intros.
Auto with v62.
Intros.
Elim y.
Auto with v62.
Auto with v62.
Qed.

Load composition.
Load inf_liveness.

Lemma CMT_L12 : (m:nat)
  (inf_leads_to CMT
    (s_and [s:st](le (s time) cmt) 
           [s:st](eq nat m (cmt_variant s)))
    (s_or
      (s_and [s:st](le (s time) cmt) 
             [s:st](lt m (cmt_variant s)))
      [s:st](eq nat (s time) cmt))).

Intros.
Unfold cmt_variant.
Apply inf_leads_to_basis.
Unfold ensures.
Split.
Apply CMT_S8.
Apply CMT_L11.
Qed.

Lemma CMT_L13 : (inf_leads_to CMT 
  ([s:st](le (s time) cmt)) ([s:st](eq nat (s time) cmt))).

Apply (inf_leads_to_rev_nat_induction CMT cmt_variant cmt).
Unfold cmt_variant.
Apply s_imp_p_p.
Intros.
Apply CMT_L12.
Qed.

Theorem CMT_L14 : (inf_leads_to CMT 
  ([s:st](eq nat (s time) O)) ([s:st](eq nat (s time) cmt))).

Apply (inf_leads_to_implication_l CMT [s:st](eq nat (s time) O)
        [s:st](le (s time) cmt) [s:st](eq nat (s time) cmt)).
Unfold everywhere s_imp.
Intros.
Rewrite -> H.
Apply le_O_n.
Apply CMT_L13.
Qed.

Lemma CMT''_is_union : (Union act CMT CMT')==CMT''.

Unfold CMT CMT' CMT''.
Apply Extensionality_Ensembles.
Unfold Same_set.
Unfold Included.
Split.
Intros.
ECI H.
ECI H.
ECI H.
Elim H.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.

ECI H.
Elim H.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.

Intros.
ECI H.
ECI H.
ECI H.
Elim H.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.

Specialize (Singleton_inv ? ? ? H).
Clear H.
Intro.
Rewrite <- H.
Auto with v62.
Qed.

(*END-H*)

(*T* Again, we have verified that after this extension all theorems
remain valid. More importantly, we have reproved these theorems in
their informative versions, that we need to apply our compositionality
rule in the proof of Theorem |CMT_L16| below.  *T*)

(*T* The only nontrivial proof obligation produced by Theorem
|CMT_L16| below is given by the following lemma: For the new component
|CMT'| we just have to prove an |unless| assertion, which states
noninterference with the informative version of |CMT_L12| (a
|inf_leads_to| assertion that is actually an |ensures| assertion). 

\begin{verbatim}
Lemma CMT_L15 : (m:nat)(unless CMT'
     (s_and [s:st](le (s time) cmt)  
            [s:st]m==(s time))
     (s_or (s_and [s:st](le (s time) cmt) 
                  [s:st](lt m (s time)))
           [s:st](s time)==cmt)).
\end{verbatim}

*T*)

Lemma CMT_L15 : (m:nat)(unless CMT'
     (s_and [s:st](le (s time) cmt)  
            [s:st]m=(s time))
     (s_or (s_and [s:st](le (s time) cmt) 
                  [s:st](lt m (s time)))
           [s:st](s time)=cmt)).

Unfold unless.
Unfold co.
Intros.
Cut e==update_h.
Intros.
Rewrite H0.
Clear H0 H.
Clear e.
Apply hoare_sc.
log_unfold .
Intros.
Clear H.
ECI H0.
ECI H.
Simpl.
Rewrite assign_changed.
Cut (le m (h (s time))).
Intros.
Elim (le_lt_or_eq ? ? H2).
Intros.
Right.
Left.
Split.
Apply h_rem_below_cmt.
Trivial.

Trivial.

Intros.
Left.
Rewrite <- H3.
Split.
Rewrite H1.
Trivial.

Trivial.

Rewrite H1.
Apply h_is_ascending.

Unfold CMT' in H.
Elim H.
Intros.
Elim H0.

Auto with v62.
Intros.
Symmetry.
Apply Singleton_inv.
Trivial.
Qed.


Transparent CMT_L13.
Transparent CMT_L12.

(*T* Now we can prove the expected liveness property of the composed
system as formulated in the following theorem. 

\begin{verbatim}
Theorem CMT_L16 : (inf_leads_to (Union act CMT CMT')
  ([s:st](le (s time) cmt)) ([s:st]((s time)==cmt))).
\end{verbatim}
*T*)

Theorem CMT_L16 : (inf_leads_to (Union act CMT CMT')
  ([s:st](le (s time) cmt)) ([s:st](eq nat (s time) cmt))).

Apply (inf_leads_to_union CMT CMT' [s:st](le (s time) cmt)
        [s:st](s time)=cmt CMT_L13).
Unfold CMT_L13.
Apply inf_leads_to_rev_nat_induction_comp.
Unfold CMT_L12.
Intros.
Apply inf_leads_to_basis_comp.
Apply CMT_L15.
Qed.

Opaque CMT_L13.
Opaque CMT_L12.

(*T* The proof is done by applying the compositionality theorem
|inf_leads_to_| \linebreak |union|. The verification of the compositionality
property is reduced to |CMT_L15| by applying
|inf_leads_to_induction_comp| and
|inf_leads_to_basis_comp|. *T*)

(*BEGIN-H*)

Theorem CMT_L17 : (leads_to CMT''
  ([s:st](le (s time) cmt)) ([s:st](eq nat (s time) cmt))).

Rewrite <- CMT''_is_union.
Apply inf_leads_to_imp_leads_to.
Apply CMT_L16.
Qed.

(*END-H*)