Mefresa.Dec.ContingencyDecidability
Let us start by a general manner of expressing
decidability. This shall be used every time we want
to prove a predicate's decidability.
Definition dec (P : Prop) := P \/ ~ P.
Function get_interfaces_vis_role_cont (v:visibility) (r:role) (ct:contingency)
(l:list interface) {struct l} : list interface :=
match l with
| nil => nil
| i :: r' => if ((i->visibility)%int == v)%vis &&
((i->role)%int == r)%role &&
((i->contingency)%int == ct)%cont then
i :: (get_interfaces_vis_role_cont v r ct r')
else
(get_interfaces_vis_role_cont v r ct r')
end.
Lemma get_interfaces_vis_role_cont_spec:
forall v r ct l li,
get_interfaces_vis_role_cont v r ct l = li ->
forall i, In i li ->
((i->visibility)%int = v)%vis /\ ((i->role)%int = r)%role /\ ((i->contingency)%int = ct)%cont.
Proof.
induction l; intros.
Case "Its nil".
simpl in H.
subst; fromfalse.
Case "Its not nil".
unfold get_interfaces_vis_role_cont in H;
fold get_interfaces_vis_role_cont in H.
assert (((((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont) = true) \/ ((((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont) = false)
).
destruct (((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont); auto.
assert (((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont = true ->
((a ->visibility)%int = v)%vis /\ ((a ->role)%int = r)%role /\
((a ->contingency)%int = ct)%cont).
intro.
repeat rewrite andb_true_iff in H2.
destruct H2 as ((Hv, Hr), Hc).
repeat split; auto.
apply role_bool_prop; auto.
apply contingency_eq_reflection; auto.
destruct (((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont); auto.
rewrite <- H in H0.
inversion H0; subst.
apply H2;auto.
clear H0.
apply IHl with (li:=(get_interfaces_vis_role_cont v r ct l)); auto.
apply IHl with (li:=(get_interfaces_vis_role_cont v r ct l)); auto.
rewrite <- H in H0; auto.
Qed.
Lemma get_interfaces_vis_role_cont_fact:
forall i v r ct li, In i (get_interfaces_vis_role_cont v r ct li) ->
In i li.
Proof.
induction li; intros.
simpl in H. inversion H.
simpl in H.
destruct (((a ->visibility)%int == v)%vis && ((a ->role)%int == r)%role &&
((a ->contingency)%int == ct)%cont).
destruct H; subst; intuition.
right. apply IHli; auto.
Qed.
Function check_if_mandatory (li : list interface) : bool :=
match li with
nil => true
| i :: r => if ((i->contingency)%int == Mandatory)%cont then check_if_mandatory r else false
end.
Definition not_nil (l:list interface) : bool :=
match l with
nil => false
| _ => true
end.
Function check_if_recipients_are_mandatory (idC:ident) (li:list interface) (lb:list binding) (lc:list component) (li':list interface): bool :=
match li with
nil => true
| i :: r => let lir := get_normal_binding_recipients idC (i->id%int) lb lc in
let lir' := get_import_binding_recipients idC (i->id%int) lb li' in
if check_if_mandatory (app lir lir') && not_nil (app lir lir') then check_if_recipients_are_mandatory idC r lb lc li' else false
end.
Lemma check_if_recipients_are_mandatory_spec:
forall idC li lb lc li',
check_if_recipients_are_mandatory idC li lb lc li' = true ->
forall i, In i li ->
forall i', In i' ((get_normal_binding_recipients idC (i->id%int) lb lc) ++
(get_import_binding_recipients idC (i->id%int) lb li')) ->
(i' ->contingency)%int = Mandatory.
Proof.
intros.
unfold check_if_recipients_are_mandatory in H.
induction li.
inversion H0.
destruct H0; subst.
Case "1/2".
clear IHli.
assert (check_if_mandatory
(get_normal_binding_recipients idC (i ->id)%int lb lc ++
get_import_binding_recipients idC (i ->id)%int lb li')%list
&&
not_nil
(get_normal_binding_recipients idC (i ->id)%int lb lc ++
get_import_binding_recipients idC (i ->id)%int lb li')%list = true ).
destruct (check_if_mandatory
(get_normal_binding_recipients idC (i ->id)%int lb lc ++
get_import_binding_recipients idC (i ->id)%int lb li')%list
&&
not_nil
(get_normal_binding_recipients idC (i ->id)%int lb lc ++
get_import_binding_recipients idC (i ->id)%int lb li')%list ) ; try congruence; auto.
clear H.
rewrite andb_true_iff in H0.
destruct H0.
clear H0.
induction ((get_normal_binding_recipients idC (i ->id)%int lb lc ++
get_import_binding_recipients idC (i ->id)%int lb li')%list).
inversion H1.
destruct H1; subst.
unfold check_if_mandatory in H.
assert (((i' ->contingency)%int == Mandatory)%cont = true).
destruct (((i' ->contingency)%int == Mandatory)%cont); auto.
apply contingency_eq_reflection; auto.
apply IHl; auto.
unfold check_if_mandatory in H.
destruct (((a ->contingency)%int == Mandatory)%cont);
try congruence; auto.
Case "2/2".
apply IHli; auto.
clear IHli.
destruct (check_if_mandatory
(get_normal_binding_recipients idC (a ->id)%int lb lc ++
get_import_binding_recipients idC (a ->id)%int lb li')%list
&&
not_nil
(get_normal_binding_recipients idC (a ->id)%int lb lc ++
get_import_binding_recipients idC (a ->id)%int lb li')%list );
try congruence.
Qed.
Function subcomponents_client_external_mandatory_interfaces lc : list (component * list interface) :=
match lc with
nil => nil
| c :: r => let liecm := get_interfaces_vis_role_cont External Client Mandatory (c->interfaces%comp) in
(c, liecm) :: (subcomponents_client_external_mandatory_interfaces r)
end.
Lemma subcomponents_client_external_mandatory_interfaces_spec:
forall lc c li, In (c, li) (subcomponents_client_external_mandatory_interfaces lc) ->
(In c lc
/\ (forall i, In i li ->
(In i (c->interfaces%comp) /\ (i ->role)%int = Client /\
(i ->visibility)%int = External /\ (i->contingency%int) = Mandatory))).
Proof.
induction lc; intros.
simpl in H. inversion H.
simpl in H.
destruct H.
Case "1/2".
inversion H; subst.
clear H.
split. left; auto.
intros.
destruct get_interfaces_vis_role_cont_spec with (v:=External) (r:=Client)
(ct:=Mandatory) (l:=(c ->interfaces)%comp)
(li:=get_interfaces_vis_role_cont External Client Mandatory (c ->interfaces)%comp)
(i:=i); auto.
destruct H1.
split; auto.
eapply get_interfaces_vis_role_cont_fact; eauto.
Case "2/2".
destruct IHlc with (c:=c) (li:=li); auto.
split. right; auto.
auto.
Qed.
Lemma subcomponents_client_external_mandatory_interfaces_nil_fact:
forall lc, subcomponents_client_external_mandatory_interfaces lc = nil ->
forall c, In c lc -> forall i, In i (c->interfaces%comp) ->
(i->contingency%int) <> Mandatory.
Proof.
induction lc; intros.
inversion H0.
destruct H0; subst.
simpl in H. inversion H.
simpl in H. inversion H.
Qed.
Definition bool_dec (P: bool) : Prop := (P=true) \/ (P=false).
Theorem bool_dec_fact:
forall P, bool_dec P.
Proof.
destruct P; firstorder.
Qed.
Hint Resolve bool_dec_fact.
Lemma subcomponents_client_external_mandatory_interfaces_fact:
forall lc c li, In (c, li) (subcomponents_client_external_mandatory_interfaces lc) ->
forall i, In i (c->interfaces%comp) ->
((i ->visibility)%int = External)%vis ->
((i ->role)%int = Client)%role ->
(i->contingency%int) = Mandatory ->
In i li.
Proof.
intros.
functional induction subcomponents_client_external_mandatory_interfaces lc.
fromfalse.
destruct H.
Case "1/2". Focus.
inversion H; subst. clear H.
clear IHl.
induction ((c ->interfaces)%comp).
SCase "Interfaces are nil".
fromfalse.
SCase "Interfaces are not nil".
destruct H0; subst.
SSCase "1/2".
Focus.
clear IHl.
simpl.
rewrite <- visibility_eq_reflection in H1.
rewrite <- role_bool_prop in H2.
rewrite <- contingency_eq_reflection in H3.
rewrite H1; rewrite H2; rewrite H3; simpl.
left; auto.
SSCase "2/2".
simpl.
destruct (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont).
right; auto.
auto.
Case "1/2".
auto.
Qed.
Lemma subcomponents_client_external_mandatory_interfaces_spec':
forall lc,
forall e, In e (subcomponents_client_external_mandatory_interfaces lc) ->
In (fst e) lc /\
snd e = get_interfaces_vis_role_cont External Client Mandatory (fst e->interfaces%comp).
Proof.
intros.
functional induction subcomponents_client_external_mandatory_interfaces lc.
inversion H.
inversion H.
Case "Head of the List".
split.
SCase "1/2".
left.
destruct e; simpl in *.
inversion H0; subst; refl.
SCase "2/2".
destruct e; simpl in *.
inversion H0; subst; refl.
Case "In the Tail of List".
split.
SCase "1/2".
right; apply IHl; auto.
SCase "2/2".
apply IHl; auto.
Qed.
Function subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_aux lcli lc li lb : bool :=
match lcli with
nil => true
| (c, cli) :: r => if check_if_recipients_are_mandatory (c->id%comp) cli lb lc li then
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_aux r lc li lb
else
false
end.
Function subcomponents_client_external_mandatory_interfaces_are_bound_bool_one lc li lb : bool :=
match subcomponents_client_external_mandatory_interfaces lc with
nil => true
| lcli => subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_aux lcli lc li lb
end.
Lemma subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec:
forall lc li lb ,
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one lc li lb = true ->
(forall c, In c lc ->
forall i, In i (c->interfaces%comp) ->
(i ->role)%int = Client ->
(i ->visibility)%int = External ->
(i ->contingency)%int = Mandatory ->
forall li', li' = get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc ->
forall li'', li'' = get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li ->
(forall i', In i' (app li' li'') ->
(i'->contingency)%int = Mandatory
)
).
Proof.
intros.
unfold subcomponents_client_external_mandatory_interfaces_are_bound_bool_one in H.
assert (forall c li, In (c, li) (subcomponents_client_external_mandatory_interfaces lc) ->
(In c lc
/\ (forall i, In i li ->
In i (c->interfaces%comp) /\ (i ->role)%int = Client /\ (i ->visibility)%int = External /\
(i->contingency%int) = Mandatory))).
apply subcomponents_client_external_mandatory_interfaces_spec.
assert (forall c li, In (c, li) (subcomponents_client_external_mandatory_interfaces lc) ->
forall i, In i (c->interfaces%comp) ->
((i ->visibility)%int = External)%vis ->
((i ->role)%int = Client)%role ->
(i->contingency%int) = Mandatory ->
In i li) as Hb.
apply subcomponents_client_external_mandatory_interfaces_fact.
assert (exists li, In (c, li) (subcomponents_client_external_mandatory_interfaces lc))
as Ha. Focus.
clear H. clear H2 H3 H4. clear H5 H6 H7. clear H8 Hb.
induction lc; simpl.
fromfalse.
destruct H0; subst.
exists (get_interfaces_vis_role_cont External Client Mandatory (c ->interfaces)%comp).
left; auto.
destruct IHlc; auto.
exists x. right. exact H0.
destruct Ha as (xli, Ha).
assert (subcomponents_client_external_mandatory_interfaces lc = nil ->
In c lc -> In i (c->interfaces%comp) ->
(i->contingency%int) <> Mandatory).
intros.
apply subcomponents_client_external_mandatory_interfaces_nil_fact with (lc:=lc) (c:=c); auto.
clear H0.
clear H9.
clear H8.
induction (subcomponents_client_external_mandatory_interfaces lc).
Case "1/2".
fromfalse.
Case "2/2".
destruct a.
destruct Ha; subst.
SCase "Head". Focus.
clear IHl.
inversion H0; subst.
clear H0.
simpl in H.
assert (
check_if_recipients_are_mandatory (c ->id)%comp xli lb lc li = true ->
forall i, In i xli ->
forall i', In i' ((get_normal_binding_recipients (c ->id)%comp (i->id%int) lb lc) ++
(get_import_binding_recipients (c ->id)%comp (i->id%int) lb li)) ->
(i' ->contingency)%int = Mandatory).
apply check_if_recipients_are_mandatory_spec.
destruct (check_if_recipients_are_mandatory (c ->id)%comp xli lb lc li);
try congruence.
apply H0 with (i:=i); auto.
apply Hb with (c0:=c); auto.
left; auto.
SCase "Tail".
apply IHl; clear IHl; auto.
SSCase "1/2". Focus.
destruct l; auto.
clear -H SSCase SCase Case.
simpl in H.
destruct (check_if_recipients_are_mandatory (c0 ->id)%comp l0 lb lc li);
try congruence. auto.
SSCase "1/2".
intros.
apply Hb with (c:=c1); auto.
right; auto.
Qed.
Inductive ext_client_mand_mapping (l:list component) (l':list (component * list interface)) : Prop :=
| MapNil : l=nil -> l'=nil -> ext_client_mand_mapping l l'
| MapStep: forall e r e' r',
l = e :: r ->
l' = e' :: r' ->
e = (fst e') ->
(snd e') = get_interfaces_vis_role_cont External Client Mandatory (e->interfaces%comp) ->
ext_client_mand_mapping r r' ->
ext_client_mand_mapping l l'.
Lemma get_normal_binding_recipients_aux2_trivial_fact:
forall IdC IdI lc r,
lc[IdC] = None ->
get_normal_binding_recipients_aux2 ((IdC, IdI)::r) lc =
get_normal_binding_recipients_aux2 r lc.
Proof.
intros.
simpl.
rewrite H.
refl.
Qed.
Lemma check_if_mandatory_fact':
forall l,
(forall i : interface,
In i l -> (i ->contingency)%int = Mandatory) ->
check_if_mandatory l = true.
Proof.
induction l. refl.
intros.
simpl.
assert (check_if_mandatory l = true).
apply IHl; intros.
apply H.
right; auto.
rewrite H0.
replace (((a ->contingency)%int == Mandatory)%cont) with true; auto.
assert ((a ->contingency)%int = Mandatory).
apply H. left; auto.
rewrite H1.
refl.
Qed.
Lemma subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec':
forall lc li lb ,
(forall c, In c lc ->
forall i, In i (c->interfaces%comp) ->
(i ->role)%int = Client ->
(i ->visibility)%int = External ->
(i ->contingency)%int = Mandatory ->
(app (get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc )
(get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li)) <> nil /\
forall i', In i' (app (get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc )
(get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li)) ->
(i'->contingency)%int = Mandatory
) ->
forall lcli,
(forall e, In e lcli -> In (fst e) lc /\
snd e = get_interfaces_vis_role_cont External Client Mandatory (fst e->interfaces%comp)) ->
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_aux lcli lc li lb = true.
Proof.
intros.
functional induction subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_aux lcli
lc li lb ; auto.
Case "1/2".
apply IHb; auto.
intros.
apply H0. right;auto.
Case "2/2".
assert (In (fst (c,cli)) lc /\
snd (c, cli) = get_interfaces_vis_role_cont External Client Mandatory (c->interfaces%comp)).
apply H0; left; auto.
simpl in H1. clear H0.
destruct H1.
subst.
assert (forall i : interface,
In i (c ->interfaces)%comp ->
(i ->role)%int = Client ->
(i ->visibility)%int = External ->
(i ->contingency)%int = Mandatory ->
(get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc ++
get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li)%list <>
nil /\
forall i' : interface,
In i'
(get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc ++
get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li) ->
(i' ->contingency)%int = Mandatory) as Ha.
apply H; auto.
clear H.
destruct c; simpl in *. clear H0.
induction l0; simpl in *. congruence.
apply IHl0; clear IHl0.
Focus.
assert ((a ->role)%int = Client ->
(a ->visibility)%int = External ->
(a ->contingency)%int = Mandatory ->
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list <> nil /\
forall i' : interface,
In i'
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li) ->
(i' ->contingency)%int = Mandatory) as Hb.
apply Ha; auto.
clear Ha.
assert (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont = true->
(a ->visibility)%int = External /\
((a ->role)%int = Client)%role /\
((a ->contingency)%int = Mandatory)%cont) as He.
Focus.
intros.
repeat rewrite andb_true_iff in H.
destruct H as ((H' ,H''), H''').
rewrite visibility_eq_reflection in H'.
rewrite role_bool_prop in H''.
rewrite contingency_eq_reflection in H'''.
repeat split; auto.
destruct (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont).
SCase "True".
Focus.
assert ((a ->visibility)%int = External /\
(a ->role)%int = Client /\ (a ->contingency)%int = Mandatory) as Hf.
apply He;auto.
clear He.
destruct Hf as (Hf1, (Hf2, Hf3)).
assert ((get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list <> nil /\
forall i' : interface,
In i'
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li) ->
(i' ->contingency)%int = Mandatory) as Hq.
apply Hb; auto.
clear Hb.
simpl in e0.
assert (check_if_mandatory
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list
&&
not_nil
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list = true ) as Hr.
Focus.
clear e0.
destruct Hq as (Hq1, Hq2).
replace (not_nil
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list) with true.
clear Hq1.
induction ((get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list ). refl.
assert (check_if_mandatory (a0 :: l2) = true).
apply check_if_mandatory_fact'; auto.
rewrite H. refl.
destruct ((get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)%list ); try congruence.
refl.
rewrite Hr in e0.
exact e0.
SCase "False".
exact e0.
intros.
eapply Ha with (i0:=i1); auto.
Qed.
Lemma ext_client_mand_mapping_fact:
forall lc,
ext_client_mand_mapping lc (subcomponents_client_external_mandatory_interfaces lc).
Proof.
induction lc; simpl; auto.
apply MapNil ;auto.
eapply MapStep; eauto.
Qed.
Lemma subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec:
forall lc li lb ,
(forall c, In c lc ->
forall i, In i (c->interfaces%comp) ->
(i ->role)%int = Client ->
(i ->visibility)%int = External ->
(i ->contingency)%int = Mandatory ->
(app (get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc )
(get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li)) <> nil /\
(forall i', In i' (app (get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc )
(get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li)) ->
(i'->contingency)%int = Mandatory
)
) ->
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one lc li lb = true.
Proof.
destruct lc; intros; simpl; auto.
unfold subcomponents_client_external_mandatory_interfaces_are_bound_bool_one.
assert (forall e, In e (subcomponents_client_external_mandatory_interfaces (c::lc)) ->
In (fst e) (c::lc) /\
snd e = get_interfaces_vis_role_cont External Client Mandatory (fst e->interfaces%comp)
).
apply subcomponents_client_external_mandatory_interfaces_spec'.
destruct (subcomponents_client_external_mandatory_interfaces (c :: lc)); auto.
apply subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec'; auto.
Qed.
Definition f_aux := subcomponents_client_external_mandatory_interfaces_are_bound_bool_one.
Fixpoint subcomponents_client_external_mandatory_interfaces_are_bound_bool (c:component) : bool :=
match c with
Component i p ic cl lc li lb => (f_aux lc li lb) &&
((fix f_sub lc {struct lc} :=
match lc with
nil => true
| sc :: r => subcomponents_client_external_mandatory_interfaces_are_bound_bool sc && (f_sub r)
end
)
lc)
end.
Lemma subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact:
forall c,
subcomponents_client_external_mandatory_interfaces_are_bound_bool c = true ->
forall c', In c' (c->subComponents%comp) ->
subcomponents_client_external_mandatory_interfaces_are_bound_bool c' = true.
Proof.
intros.
destruct c.
simpl in *.
rewrite andb_true_iff in H.
destruct H.
clear H.
induction l.
fromfalse.
destruct H0; subst.
Case "1/2".
clear IHl.
rewrite andb_true_iff in H1.
destruct H1; auto.
Case "2/2".
apply IHl; auto.
rewrite andb_true_iff in H1.
destruct H1; auto.
Qed.
Lemma check_if_recipients_are_mandatory_fact:
forall idC li lb lc li',
check_if_recipients_are_mandatory idC li lb lc li' = true ->
forall int,
In int li ->
(get_normal_binding_recipients idC (int ->id)%int lb lc ++
get_import_binding_recipients idC (int ->id)%int lb li')%list <> nil.
Proof.
intros.
functional induction check_if_recipients_are_mandatory idC li lb lc li';
try fromfalse; try congruence.
destruct H0; subst; auto.
clear -e0.
destruct ((get_normal_binding_recipients idC (int ->id)%int lb lc ++
get_import_binding_recipients idC (int ->id)%int lb li')%list);
simpl in * |-; try congruence.
Qed.
Lemma get_normal_import_bindings_fact:
forall lc li lb,
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one
lc li lb = true ->
forall c', In c' lc ->
forall int, In int (c' ->interfaces)%comp ->
(int ->role)%int = Client ->
(int ->visibility)%int = External ->
(int ->contingency)%int = Mandatory ->
(get_normal_binding_recipients (c' ->id)%comp (int ->id)%int lb lc ++
get_import_binding_recipients (c' ->id)%comp (int ->id)%int lb li)%list <> nil.
Proof.
intros.
unfold subcomponents_client_external_mandatory_interfaces_are_bound_bool_one in H.
assert (In (c', (get_interfaces_vis_role_cont External Client Mandatory (c' ->interfaces)%comp)) (subcomponents_client_external_mandatory_interfaces lc))
as Ha. Focus.
clear H. clear H2 H3 H4.
induction lc; simpl.
fromfalse.
destruct H0; subst.
left; refl.
right; apply IHlc; auto.
induction (subcomponents_client_external_mandatory_interfaces lc);
try fromfalse.
destruct Ha; subst.
Case "Head". Focus.
clear IHl.
simpl in H.
apply check_if_recipients_are_mandatory_fact with
(li:=(get_interfaces_vis_role_cont External Client Mandatory
(c' ->interfaces)%comp)).
destruct (check_if_recipients_are_mandatory (c' ->id)%comp
(get_interfaces_vis_role_cont External Client Mandatory
(c' ->interfaces)%comp)); auto.
clear H.
functional induction (get_interfaces_vis_role_cont External Client Mandatory
(c' ->interfaces)%comp); try congruence.
destruct H1; subst. left; auto.
right; apply IHl1; auto.
destruct H1; subst; auto.
rewrite H2 in e0; rewrite H3 in e0;
rewrite H4 in e0. simpl in e0.
congruence.
Case "Tail".
apply IHl; intros; auto; clear IHl.
simpl in H.
destruct a.
destruct (check_if_recipients_are_mandatory (c ->id)%comp l0 lb lc li);
try congruence.
destruct l; auto.
Qed.
Definition eqType c : Prop :=
subcomponents_client_external_mandatory_interfaces_are_bound_bool c = true <->
subcomponents_client_external_mandatory_interfaces_are_bound c.
Lemma nil_eqType: forall c, In c nil -> eqType c.
Proof.
intros.
inversion H.
Qed.
Lemma cons_eqType c (Hc : eqType c) lc (Hlc : forall c', In c' lc -> eqType c'):
forall c', In c' (cons c lc) -> eqType c'.
Proof.
intros.
destruct H; subst; auto.
Qed.
Lemma lc_eqType (Hp: forall c, eqType c) :
forall lc, (forall c', In c' lc -> eqType c').
Proof.
exact (fix lc_eqType lc :=
match lc as lc return (forall c', In c' lc -> eqType c') with
| nil => nil_eqType
| cons c lc => cons_eqType c (Hp c) lc (lc_eqType lc)
end).
Defined.
Theorem eqType_correctness:
forall c,
subcomponents_client_external_mandatory_interfaces_are_bound_bool c = true <->
subcomponents_client_external_mandatory_interfaces_are_bound c.
Proof.
fix 1; intros [i p ic cl lc li lb].
assert (HeqType_correctness := lc_eqType eqType_correctness lc);
clear eqType_correctness.
Guarded.
split; intro.
Case "Function Entails Predicate". Focus.
apply CEMI_Bound; intros.
SCase "Interfaces are of Mandatory nature". Focus.
simpl in *.
rewrite andb_true_iff in H.
destruct H.
clear HeqType_correctness.
unfold f_aux in H.
clear H5.
split.
apply get_normal_import_bindings_fact; auto.
eapply subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec; eauto.
SCase "Recursion on sub-levels".
assert (eqType c'); auto.
clear HeqType_correctness.
unfold eqType in H1.
simpl in H0.
assert (forall c, In c ((Component i p ic cl lc li lb)->subComponents%comp) ->
subcomponents_client_external_mandatory_interfaces_are_bound_bool c = true).
apply subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact; auto.
simpl in H2.
assert (subcomponents_client_external_mandatory_interfaces_are_bound_bool c' = true).
apply H2; auto.
clear H2.
destruct H1.
destruct (subcomponents_client_external_mandatory_interfaces_are_bound_bool c').
SSCase "Its true".
apply H1; auto.
SSCase "Its false".
congruence.
Case "Predicate Entails Function".
unfold eqType in HeqType_correctness.
simpl.
rewrite andb_true_iff.
inversion H; simpl in * |-.
split.
SCase "Current Hierarchical Level".
Focus.
unfold f_aux.
apply subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec.
intros.
eapply H0 with (c':=c) (int:=i0); auto.
SCase "Recursion".
clear -H1 HeqType_correctness Case SCase.
induction lc. auto.
destruct HeqType_correctness with (c':=a). left; auto.
rewrite andb_true_iff.
split.
clear IHlc.
assert (subcomponents_client_external_mandatory_interfaces_are_bound a).
apply H1. left; auto.
apply H0; auto.
apply IHlc; intros; clear IHlc.
split; intro; intuition.
apply HeqType_correctness. right; auto.
auto.
apply H1. right; auto.
Qed.
Lemma subcomponents_client_external_mandatory_interfaces_are_bound_dec:
forall c, dec (subcomponents_client_external_mandatory_interfaces_are_bound c).
Proof.
intros.
unfold dec.
rewrite <- eqType_correctness.
destruct (subcomponents_client_external_mandatory_interfaces_are_bound_bool c);
intuition.
Qed.
Function subcomponents_client_internal_mandatory_interfaces li : list interface :=
match li with
nil => nil
| i :: r => if ((i->visibility%int) == Internal)%vis && ((i->role%int) == Client)%role &&
((i->contingency%int) == Mandatory)%cont then
i :: subcomponents_client_internal_mandatory_interfaces r
else
subcomponents_client_internal_mandatory_interfaces r
end.
Function check_if_recipients_are_mandatory_aux (li:list interface) (lb:list binding) (lc:list component) : bool :=
match li with
nil => true
| i :: r => let lir := get_export_binding_recipients (i->id%int) lb lc in
if check_if_mandatory lir && not_nil lir then
check_if_recipients_are_mandatory_aux r lb lc
else
false
end.
Function client_internal_mandatory_interfaces_are_bound_bool_one
(li:list interface) (lc:list component) (lb:list binding) : bool :=
match subcomponents_client_internal_mandatory_interfaces li with
nil => true
| i :: r => check_if_recipients_are_mandatory_aux (i :: r) lb lc
end.
Fixpoint client_internal_mandatory_interfaces_are_bound_bool (c:component) : bool :=
match c with
Component i p ic cl lc li lb => (client_internal_mandatory_interfaces_are_bound_bool_one li lc lb) &&
(fix f_sub lc {struct lc} :=
match lc with
nil => true
| sc :: r => client_internal_mandatory_interfaces_are_bound_bool sc && f_sub r
end
) lc
end.
Definition client_internal_mandatory_itfs_are_bound_bool :=
client_internal_mandatory_interfaces_are_bound_bool.
Lemma check_if_mandatory_fact:
forall i l, In i l ->
check_if_mandatory l = true ->
(i->contingency%int) = Mandatory.
Proof.
induction l; simpl; intros.
Case "Base".
inversion H.
Case "Step".
destruct H; subst.
SCase "Head".
clear IHl.
apply contingency_eq_reflection.
destruct (((i ->contingency)%int == Mandatory)%cont); auto.
SCase "Tail".
apply IHl; auto.
destruct (check_if_mandatory l); auto.
destruct (((a ->contingency)%int == Mandatory)%cont); auto.
Qed.
Lemma check_if_recipients_are_mandatory'_fact:
forall i i1 l lb lc,
check_if_recipients_are_mandatory_aux (i :: i1 :: l) lb lc = true ->
check_if_recipients_are_mandatory_aux (i1 :: l) lb lc = true.
Proof.
intros.
fold check_if_recipients_are_mandatory_aux in H;
unfold check_if_recipients_are_mandatory_aux in H.
destruct (check_if_mandatory (get_export_binding_recipients (i ->id)%int lb lc) &&
not_nil (get_export_binding_recipients (i ->id)%int lb lc)); try congruence.
exact H.
Qed.
Lemma client_internal_mandatory_interfaces_are_bound_bool_one_spec:
forall li lc lb,
client_internal_mandatory_interfaces_are_bound_bool_one li lc lb = true ->
forall int, In int li ->
(int ->role)%int = Client ->
(int ->visibility)%int = Internal ->
(int ->contingency)%int = Mandatory ->
forall li0,
li0 = get_export_binding_recipients (int ->id)%int lb lc ->
li0 <> nil ->
forall i0,
In i0 li0 ->
(i0 ->contingency)%int = Mandatory.
Proof.
intros.
unfold client_internal_mandatory_interfaces_are_bound_bool_one in H.
functional induction subcomponents_client_internal_mandatory_interfaces li.
inversion H0.
Case "1/2".
Focus.
destruct H0; subst.
SCase "It is the Head".
Focus.
clear IHl.
simpl in H.
destruct ((get_export_binding_recipients (int ->id)%int lb lc));
try congruence.
eapply check_if_mandatory_fact with (l:=i::l); auto.
destruct (check_if_mandatory (i :: l)); auto.
SCase "In the Tail".
apply IHl; clear IHl; auto.
destruct (subcomponents_client_internal_mandatory_interfaces r); auto.
eapply check_if_recipients_are_mandatory'_fact with (i:=i); auto.
intros.
Case "2/2".
destruct H0; subst.
SCase "It is the head".
Focus.
clear IHl.
rewrite H1 in e0.
rewrite H2 in e0.
rewrite H3 in e0.
simpl in e0.
congruence.
SCase "In the tail".
apply IHl; clear IHl; auto.
Qed.
Lemma client_internal_mandatory_interfaces_are_bound_bool_fact:
forall c : component,
client_internal_mandatory_interfaces_are_bound_bool c = true ->
forall c' : component,
In c' (c ->subComponents)%comp ->
client_internal_mandatory_interfaces_are_bound_bool c' = true.
Proof.
intros.
destruct c.
simpl in *.
rewrite andb_true_iff in H.
destruct H.
clear H.
induction l.
fromfalse.
destruct H0; subst.
Case "1/2".
clear IHl.
rewrite andb_true_iff in H1.
destruct H1; auto.
Case "2/2".
apply IHl; auto.
rewrite andb_true_iff in H1.
destruct H1; auto.
Qed.
Lemma client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec_proof_nr_2:
forall lc li lb, (forall int : interface,
In int li ->
(int ->role)%int = Client ->
(int ->visibility)%int = Internal ->
(int ->contingency)%int = Mandatory ->
get_export_binding_recipients (int ->id)%int lb lc <> nil /\
(forall i : interface,
In i (get_export_binding_recipients (int ->id)%int lb lc) ->
(i ->contingency)%int = Mandatory)) ->
client_internal_mandatory_interfaces_are_bound_bool_one li lc lb = true.
Proof.
intros.
induction li; try refl.
assert (client_internal_mandatory_interfaces_are_bound_bool_one li lc lb =
true) as Hi. Focus.
apply IHli; intros.
apply H; auto. right; auto.
clear IHli.
unfold client_internal_mandatory_interfaces_are_bound_bool_one.
simpl.
assert (((a ->visibility)%int == Internal)%vis &&
((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont = true \/
((a ->visibility)%int == Internal)%vis &&
((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont = false).
destruct (((a ->visibility)%int == Internal)%vis && ((a ->role)%int == Client)%role &&
((a ->contingency)%int == Mandatory)%cont); intuition.
destruct H0. Focus.
Case "It is of client, internal and mandatory nature".
rewrite H0.
repeat rewrite andb_true_iff in H0.
destruct H0. destruct H0.
assert (get_export_binding_recipients (a ->id)%int lb lc <> nil /\
(forall i : interface,
In i (get_export_binding_recipients (a ->id)%int lb lc) ->
(i ->contingency)%int = Mandatory)).
apply H; auto. left; auto.
apply role_bool_prop ; auto.
apply contingency_eq_reflection; auto.
clear H H0.
destruct H3.
induction (get_export_binding_recipients (a ->id)%int lb lc); simpl.
congruence.
assert ((a0 ->contingency)%int = Mandatory).
apply H0. left; auto.
rewrite H3.
simpl.
destruct l; simpl.
unfold client_internal_mandatory_interfaces_are_bound_bool_one in Hi.
destruct (subcomponents_client_internal_mandatory_interfaces li); simpl.
auto.
exact Hi.
assert ((if check_if_mandatory (i :: l) && not_nil (i :: l)
then
check_if_recipients_are_mandatory_aux
(subcomponents_client_internal_mandatory_interfaces li) lb lc
else false) = true) as Ha.
apply IHl. discriminate.
intros. apply H0. right. auto.
clear IHl.
simpl in Ha. exact Ha.
Case "It is not of client, internal and mandatory nature".
rewrite H0. clear H0.
exact Hi.
Qed.
Lemma client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec:
forall lc li lb, (forall int : interface,
In int li ->
(int ->role)%int = Client ->
(int ->visibility)%int = Internal ->
(int ->contingency)%int = Mandatory ->
get_export_binding_recipients (int ->id)%int lb lc <> nil /\
(forall i : interface,
In i (get_export_binding_recipients (int ->id)%int lb lc) ->
(i ->contingency)%int = Mandatory)) ->
client_internal_mandatory_interfaces_are_bound_bool_one li lc lb = true.
Proof.
intros.
unfold client_internal_mandatory_interfaces_are_bound_bool_one.
functional induction subcomponents_client_internal_mandatory_interfaces li; auto.
Case "1/2".
Focus.
assert (match subcomponents_client_internal_mandatory_interfaces r with
| nil => true
| i :: r => check_if_recipients_are_mandatory_aux (i :: r) lb lc
end = true) as Ha.
Focus.
apply IHl; clear IHl; intros.
eapply H with (int:=int); subst; auto.
right; auto.
clear IHl.
simpl.
repeat rewrite andb_true_iff in e0.
destruct e0 as ((H', H''), H''').
assert (
get_export_binding_recipients (i ->id)%int lb lc <> nil /\
(forall i' : interface,
In i' (get_export_binding_recipients (i ->id)%int lb lc) ->
(i' ->contingency)%int = Mandatory)) as He.
apply H;auto.
left; auto.
apply role_bool_prop ; auto.
apply contingency_eq_reflection; auto.
clear H H' H'' H'''.
destruct He.
destruct (subcomponents_client_internal_mandatory_interfaces r ).
SCase "1/2".
simpl.
destruct (get_export_binding_recipients (i ->id)%int lb lc);
try congruence.
replace (check_if_mandatory (i0 :: l)) with true.
refl.
symmetry.
eapply check_if_mandatory_fact'; auto.
rewrite Ha. clear Ha.
destruct (get_export_binding_recipients (i ->id)%int lb lc);
try congruence.
replace (check_if_mandatory (i1 :: l0)) with true.
refl.
symmetry.
eapply check_if_mandatory_fact'; auto.
Case "2/2".
apply IHl; intros; clear IHl.
eapply H with (int:=int); subst; auto.
right;auto.
Qed.
Lemma get_export_bindings_not_nil:
forall li lc lb,
client_internal_mandatory_interfaces_are_bound_bool_one li lc lb = true ->
forall int, In int li ->
(int ->role)%int = Client ->
(int ->visibility)%int = Internal ->
(int ->contingency)%int = Mandatory ->
get_export_binding_recipients (int ->id)%int lb lc <> nil.
Proof.
intros.
unfold client_internal_mandatory_interfaces_are_bound_bool_one in H.
functional induction subcomponents_client_internal_mandatory_interfaces li.
inversion H0.
Case "1/2".
Focus.
inversion H0; subst.
SCase "1/2".
clear H0.
clear IHl e0.
simpl in H.
destruct ( (get_export_binding_recipients (int ->id)%int lb lc) );
try discriminate.
SCase "2/2".
apply IHl; auto.
destruct (subcomponents_client_internal_mandatory_interfaces r);auto.
simpl in H.
destruct (check_if_mandatory (get_export_binding_recipients (i ->id)%int lb lc) &&
not_nil (get_export_binding_recipients (i ->id)%int lb lc)); try congruence.
exact H.
Case "2/2".
inversion H0; subst.
SCase "1/2".
Focus.
clear H0 IHl.
rewrite H1 in e0.
rewrite H2 in e0.
rewrite H3 in e0.
compute in e0.
congruence.
SCase "2/2".
apply IHl; auto.
Qed.
Definition eqType' c : Prop :=
client_internal_mandatory_interfaces_are_bound_bool c = true <->
client_internal_mandatory_interfaces_are_bound c.
Lemma nil_eqType': forall c, In c nil -> eqType' c.
Proof.
intros.
inversion H.
Qed.
Lemma cons_eqType' c (Hc : eqType' c) lc (Hlc : forall c', In c' lc -> eqType' c'):
forall c', In c' (cons c lc) -> eqType' c'.
Proof.
intros.
destruct H; subst; auto.
Qed.
Lemma lc_eqType' (Hp: forall c, eqType' c) :
forall lc, (forall c', In c' lc -> eqType' c').
Proof.
exact (fix lc_eqType' lc :=
match lc as lc return (forall c', In c' lc -> eqType' c') with
| nil => nil_eqType'
| cons c lc => cons_eqType' c (Hp c) lc (lc_eqType' lc)
end).
Defined.
Theorem eqType'_correctness:
forall c,
client_internal_mandatory_interfaces_are_bound_bool c = true <->
client_internal_mandatory_interfaces_are_bound c.
Proof.
fix 1; intros [i p ic cl lc li lb].
assert (HeqType'_correctness := lc_eqType' eqType'_correctness lc);
clear eqType'_correctness.
Guarded.
split; intro.
Case "Function Entails Predicate". Focus.
apply CIMI_Bound; intros.
SCase "Interfaces are of Mandatory nature". Focus.
simpl in *.
rewrite andb_true_iff in H.
destruct H.
clear HeqType'_correctness H4.
split; intros.
apply get_export_bindings_not_nil with (li:=li); auto.
eapply client_internal_mandatory_interfaces_are_bound_bool_one_spec; eauto.
destruct (get_export_binding_recipients (int ->id)%int lb lc);
auto; try congruence.
SCase "Recursion on sub-levels".
assert (eqType' c'); auto.
clear HeqType'_correctness.
unfold eqType' in H1.
simpl in H0.
assert (forall c, In c ((Component i p ic cl lc li lb)->subComponents%comp) ->
client_internal_mandatory_interfaces_are_bound_bool c = true).
apply client_internal_mandatory_interfaces_are_bound_bool_fact; auto.
simpl in H2.
assert (client_internal_mandatory_interfaces_are_bound_bool c' = true).
apply H2; auto.
clear H2.
destruct H1.
destruct (client_internal_mandatory_interfaces_are_bound_bool c').
SSCase "Its true".
apply H1; auto.
SSCase "Its false".
congruence.
Case "Predicate Entails Function".
unfold eqType' in HeqType'_correctness.
simpl.
rewrite andb_true_iff.
inversion H; simpl in * |-.
split.
SCase "Current Hierarchical Level".
apply client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec.
intros.
eapply H0 with (int:=int); subst; auto.
SCase "Recursion".
clear -H1 HeqType'_correctness Case SCase.
induction lc. auto.
destruct HeqType'_correctness with (c':=a). left; auto.
rewrite andb_true_iff.
split.
clear IHlc.
assert (client_internal_mandatory_interfaces_are_bound a).
apply H1. left; auto.
apply H0; auto.
apply IHlc; intros; clear IHlc.
split; intro; intuition.
apply HeqType'_correctness. right; auto.
auto.
apply H1. right; auto.
Qed.
Definition cim_itfs_bound_correctness := eqType'_correctness.
Definition mandatory_interfaces_are_bound_bool s : bool :=
client_internal_mandatory_interfaces_are_bound_bool s &&
subcomponents_client_external_mandatory_interfaces_are_bound_bool s.
Theorem mandatory_interfaces_are_bound_reflection:
forall s, (mandatory_interfaces_are_bound s) <->
(mandatory_interfaces_are_bound_bool s = true).
Proof.
intros.
unfold mandatory_interfaces_are_bound;
unfold mandatory_interfaces_are_bound_bool.
rewrite <- eqType'_correctness.
rewrite <- eqType_correctness.
destruct (subcomponents_client_external_mandatory_interfaces_are_bound_bool s);
destruct ( (client_internal_mandatory_interfaces_are_bound_bool s));
intuition.
Qed.
Theorem mandatory_interfaces_are_bound_dec:
forall s, dec (mandatory_interfaces_are_bound s).
Proof.
intros.
unfold dec.
rewrite mandatory_interfaces_are_bound_reflection.
destruct (mandatory_interfaces_are_bound_bool s); auto.
Qed.
Theorem sound_contingency_dec:
forall s, dec (sound_contingency s).
Proof.
apply mandatory_interfaces_are_bound_dec.
Qed.
Definition sound_contingency_bool s := mandatory_interfaces_are_bound_bool s.
Theorem sound_contigency_reflection:
forall s, sound_contingency s <-> sound_contingency_bool s = true.
Proof.
intro s.
unfold sound_contingency.
unfold sound_contingency_bool.
rewrite <- mandatory_interfaces_are_bound_reflection.
intuition.
Qed.
Definition sound_contigency_correctness := sound_contigency_reflection.