Mefresa.Dec.CardinalityDecidability
Function client_singleton_are_bound_once_at_most_export_bindings_bool_one lc li lb : bool :=
match li with
nil => true
| i :: r => if ((i ->role)%int == Client)%role &&
((i ->visibility)%int == Internal)%vis &&
((i ->cardinality)%int == Singleton)%card then
match ble_nat (length (get_export_binding_recipients (i->id)%int lb lc)) 1 with
true => client_singleton_are_bound_once_at_most_export_bindings_bool_one lc r lb
| false => false
end
else
client_singleton_are_bound_once_at_most_export_bindings_bool_one lc r lb
end.
Fixpoint client_singleton_are_bound_once_at_most_export_bindings_bool c : bool :=
match c with
Component i p ic cl lc li lb =>
client_singleton_are_bound_once_at_most_export_bindings_bool_one lc li lb &&
(fix f_sub lc {struct lc} :=
match lc with
nil => true
| sc :: r => client_singleton_are_bound_once_at_most_export_bindings_bool sc && f_sub r
end
) lc
end.
Definition eqSingleton_export c : Prop :=
client_singleton_are_bound_once_at_most_export_bindings_bool c = true <->
client_singleton_are_bound_once_at_most_export_bindings c.
Lemma nil_eqSingleton_export: forall c, In c nil -> eqSingleton_export c.
Proof.
intros.
inversion H.
Qed.
Lemma cons_eqSingleton_export c (Hc : eqSingleton_export c) lc (Hlc : forall c', In c' lc -> eqSingleton_export c'):
forall c', In c' (cons c lc) -> eqSingleton_export c'.
Proof.
intros.
destruct H; subst; auto.
Qed.
Lemma lc_eqSingleton_export (Hp: forall c, eqSingleton_export c) :
forall lc, (forall c', In c' lc -> eqSingleton_export c').
Proof.
exact (fix lc_eqSingleton_export lc :=
match lc as lc return (forall c', In c' lc -> eqSingleton_export c') with
| nil => nil_eqSingleton_export
| cons c lc => cons_eqSingleton_export c (Hp c) lc (lc_eqSingleton_export lc)
end).
Defined.
Lemma client_singleton_are_bound_once_at_most_export_bindings_bool_fact:
forall c : component,
client_singleton_are_bound_once_at_most_export_bindings_bool c = true ->
forall c' : component,
In c' (c ->subComponents)%comp ->
client_singleton_are_bound_once_at_most_export_bindings_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_singleton_are_bound_once_at_most_export_bindings_bool_one_fact:
forall lc li lb,
(forall i : interface,
In i li ->
(i ->role)%int = Client ->
(i ->visibility)%int = Internal ->
(i ->cardinality)%int = Singleton ->
length (get_export_binding_recipients (i ->id)%int lb lc) <= 1) ->
client_singleton_are_bound_once_at_most_export_bindings_bool_one lc li lb = true.
Proof.
induction li; intros; auto.
assert (
(a ->role)%int = Client ->
(a ->visibility)%int = Internal ->
(a ->cardinality)%int = Singleton ->
Datatypes.length (get_export_binding_recipients (a ->id)%int lb lc) <= 1) as Ha.
apply H; auto. left; auto.
simpl.
assert ((((a ->role)%int == Client)%role && ((a ->visibility)%int == Internal)%vis &&
((a ->cardinality)%int == Singleton)%card) = true ->
((a ->role)%int = Client /\ (a ->visibility)%int = Internal /\
(a ->cardinality)%int = Singleton)
) as Hb.
intros.
clear -H0.
repeat rewrite andb_true_iff in H0.
destruct H0 as ((H1, H2), H3).
repeat split; auto.
apply role_eq_reflection; auto.
apply cardinality_eq_reflection; auto.
destruct (((a ->role)%int == Client)%role && ((a ->visibility)%int == Internal)%vis &&
((a ->cardinality)%int == Singleton)%card).
Case "Its true".
Focus.
destruct Hb; auto.
destruct H1.
assert (Datatypes.length (get_export_binding_recipients (a ->id)%int lb lc) <= 1)
as Hc.
apply H; auto. left; auto.
replace (ble_nat
(Datatypes.length (get_export_binding_recipients (a ->id)%int lb lc)) 1)
with true.
apply IHli; intros.
apply H; auto. right; auto.
symmetry. apply ble_nat_reflection; auto.
Case "Its False".
apply IHli; intros; auto.
apply H; auto. right; auto.
Qed.
Theorem eqSingleton_export_correctness:
forall c,
client_singleton_are_bound_once_at_most_export_bindings_bool c = true <->
client_singleton_are_bound_once_at_most_export_bindings c.
Proof.
fix 1; intros [i p ic cl lc li lb].
assert (HeqSingleton_export_correctness := lc_eqSingleton_export eqSingleton_export_correctness lc);
clear eqSingleton_export_correctness.
Guarded.
split; intro.
Case "Function Entails Predicate". Focus.
apply SingletonExport; intros.
SCase "Singleton Requirement is Respected".
Focus.
clear HeqSingleton_export_correctness.
simpl in *.
rewrite andb_true_iff in H.
destruct H as (Ha, Hb).
clear Hb.
functional induction
client_singleton_are_bound_once_at_most_export_bindings_bool_one lc li lb;
try congruence.
fromfalse.
destruct H0; subst.
SSCase "Its the Head".
clear -e1 Case SCase SSCase.
apply ble_nat_reflection; auto.
SSCase "It is in the tail".
apply IHb; auto.
destruct H0; subst.
SSSCase "It is the Head".
rewrite H1 in e0;
rewrite H2 in e0;
rewrite H3 in e0.
simpl in e0. congruence.
SSSCase "It is in the Tail".
apply IHb; auto.
SCase "Recursive Call".
assert (eqSingleton_export c') as Ha; auto.
clear HeqSingleton_export_correctness.
unfold eqSingleton_export in Ha.
simpl in H0.
assert (forall c, In c ((Component i p ic cl lc li lb)->subComponents%comp) ->
client_singleton_are_bound_once_at_most_export_bindings_bool c = true) as Hb.
apply client_singleton_are_bound_once_at_most_export_bindings_bool_fact; auto.
simpl in Hb.
assert (client_singleton_are_bound_once_at_most_export_bindings_bool c' = true) as Hc.
apply Hb; auto.
clear Hb.
destruct Ha.
destruct (client_singleton_are_bound_once_at_most_export_bindings_bool c').
SSCase "Its true".
apply H1; auto.
SSCase "Its false".
congruence.
Case "Predicate entails Functions".
unfold eqSingleton_export in *.
simpl.
rewrite andb_true_iff.
inversion H; simpl in * |-.
split.
SCase "Current Hierarchical Level".
Focus.
clear HeqSingleton_export_correctness H1.
eapply client_singleton_are_bound_once_at_most_export_bindings_bool_one_fact; eauto.
SCase "Recursion".
clear -H1 HeqSingleton_export_correctness Case SCase.
induction lc. auto.
destruct HeqSingleton_export_correctness with (c':=a). left; auto.
rewrite andb_true_iff.
split.
clear IHlc.
assert (client_singleton_are_bound_once_at_most_export_bindings a).
apply H1. left; auto.
apply H0; auto.
apply IHlc; intros; clear IHlc.
split; intro; intuition.
apply HeqSingleton_export_correctness. right; auto.
auto.
apply H1. right; auto.
Qed.
Function get_interfaces_vis_role_card v r ct l : list interface :=
match l with
| nil => nil
| i :: r' => if ((i->visibility)%int == v)%vis &&
((i->role)%int == r)%role &&
((i->cardinality)%int == ct)%card then
i :: (get_interfaces_vis_role_card v r ct r')
else
(get_interfaces_vis_role_card v r ct r')
end.
Function subcomponents_client_external_singleton_interfaces lc :=
match lc with
nil => nil
| c :: r => let liecm := get_interfaces_vis_role_card External Client Singleton (c->interfaces%comp) in
(c, liecm) :: (subcomponents_client_external_singleton_interfaces r)
end.
Function check_if_singleton_requirement_is_met (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 ble_nat (length (app lir lir')) 1 then
check_if_singleton_requirement_is_met idC r lb lc li'
else
false
end.
Function client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_aux lcli lc li lb : bool :=
match lcli with
nil => true
| (c, cli) :: r => if check_if_singleton_requirement_is_met (c->id%comp) cli lb lc li then
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_aux r lc li lb
else
false
end.
Function client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one lc li lb : bool :=
match subcomponents_client_external_singleton_interfaces lc with
nil => true
| lcli => client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_aux lcli lc li lb
end.
Fixpoint client_singleton_are_bound_once_at_most_normal_import_bindings_bool (c:component) : bool :=
match c with
Component i p ic cl lc li lb => (client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one lc li lb) &&
((fix f_sub lc {struct lc} :=
match lc with
nil => true
| sc :: r => client_singleton_are_bound_once_at_most_normal_import_bindings_bool sc && (f_sub r)
end
)
lc)
end.
Lemma check_if_singleton_requirement_is_met_fact:
forall c' lb r int li,
check_if_singleton_requirement_is_met (c' ->id)%comp
(get_interfaces_vis_role_card External Client Singleton
(c' ->interfaces)%comp) lb (c' :: r) li = true ->
In int (c' ->interfaces)%comp ->
(int ->role)%int = Client ->
(int ->visibility)%int = External ->
(int ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (int ->id)%int lb (c' :: r) ++
get_import_binding_recipients (c' ->id)%comp (int ->id)%int lb li) <= 1.
Proof.
intros.
assert (In int ((get_interfaces_vis_role_card External Client Singleton
(c' ->interfaces)%comp))) as Ha.
Focus.
functional induction
get_interfaces_vis_role_card External Client Singleton (c' ->interfaces)%comp;
try congruence.
Case "1/2".
Focus.
destruct H0; subst. left; auto.
right. apply IHl0; auto.
clear -Case H.
simpl in H.
destruct (ble_nat
(Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (i ->id)%int lb
(c' :: r) ++
get_import_binding_recipients (c' ->id)%comp (i ->id)%int lb li))
1); congruence.
Case "2/2".
destruct H0; subst; auto.
rewrite H1 in e0;
rewrite H2 in e0;
rewrite H3 in e0.
simpl in e0. congruence.
induction ((get_interfaces_vis_role_card External Client Singleton
(c' ->interfaces)%comp)); try fromfalse.
destruct Ha; subst.
Case "1/2".
Focus.
simpl in H.
rewrite <- ble_nat_reflection.
destruct (ble_nat
(Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (int ->id)%int lb
(c' :: r) ++
get_import_binding_recipients (c' ->id)%comp (int ->id)%int lb li)) 1); auto.
Case "2/2".
apply IHl; auto.
clear -Case H.
simpl in H.
destruct (ble_nat
(Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (a ->id)%int lb
(c' :: r) ++
get_import_binding_recipients (c' ->id)%comp (a ->id)%int lb li))
1); congruence.
Qed.
Lemma check_if_singleton_requirement_is_met_fact':
forall idC li lb lc li',
check_if_singleton_requirement_is_met idC li lb lc li' = true ->
forall int,
In int li ->
Datatypes.length
(get_normal_binding_recipients idC (int ->id)%int lb lc ++
get_import_binding_recipients idC (int ->id)%int lb li') <= 1.
Proof.
intros.
functional induction check_if_singleton_requirement_is_met 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. auto.
apply ble_nat_reflection; auto.
Qed.
Lemma get_normal_binding_recipients_fact:
forall lc li lb,
client_singleton_are_bound_once_at_most_normal_import_bindings_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 ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (int ->id)%int lb lc ++
get_import_binding_recipients (c' ->id)%comp (int ->id)%int lb li) <= 1.
Proof.
intros.
unfold client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one in H.
assert
(In (c', (get_interfaces_vis_role_card External Client Singleton (c' ->interfaces)%comp))
(subcomponents_client_external_singleton_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_singleton_interfaces lc);
try fromfalse.
destruct Ha; subst.
Case "Head". Focus.
clear IHl.
simpl in H.
destruct lc; try fromfalse.
apply check_if_singleton_requirement_is_met_fact' with
(li:=(get_interfaces_vis_role_card External Client Singleton
(c' ->interfaces)%comp)).
destruct (check_if_singleton_requirement_is_met (c' ->id)%comp
(get_interfaces_vis_role_card External Client Singleton
(c' ->interfaces)%comp)); auto.
clear H.
functional induction (get_interfaces_vis_role_card External Client Singleton
(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_singleton_requirement_is_met (c ->id)%comp l0 lb lc li);
try congruence.
destruct l; auto.
Qed.
Lemma client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact:
forall c,
client_singleton_are_bound_once_at_most_normal_import_bindings_bool c = true ->
forall c', In c' (c->subComponents%comp) ->
client_singleton_are_bound_once_at_most_normal_import_bindings_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_singleton_are_bound_once_at_most_normal_import_bindings_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 ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb
lc ++
get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li) <=
1
) ->
forall lcli,
(forall e, In e lcli -> In (fst e) lc /\
snd e = get_interfaces_vis_role_card External Client Singleton (fst e->interfaces%comp)) ->
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_aux lcli lc li lb = true.
Proof.
intros.
functional induction client_singleton_are_bound_once_at_most_normal_import_bindings_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_card External Client Singleton (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 ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients (c ->id)%comp (i ->id)%int lb lc ++
get_import_binding_recipients (c ->id)%comp (i ->id)%int lb li) <= 1) 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 ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li) <= 1) as Hb.
apply Ha; auto.
clear Ha.
assert (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Client)%role &&
((a ->cardinality)%int == Singleton)%card = true->
(a ->visibility)%int = External /\
((a ->role)%int = Client)%role /\
((a ->cardinality)%int = Singleton)%card) 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 cardinality_eq_reflection in H'''.
repeat split; auto.
destruct (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Client)%role &&
((a ->cardinality)%int == Singleton)%card).
SCase "True".
Focus.
assert ((a ->visibility)%int = External /\
(a ->role)%int = Client /\ (a ->cardinality)%int = Singleton) as Hf.
apply He;auto.
clear He.
destruct Hf as (Hf1, (Hf2, Hf3)).
assert (Datatypes.length
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li) <= 1) as Hq.
apply Hb; auto.
clear Hb.
simpl in e0.
assert (ble_nat
(Datatypes.length
(get_normal_binding_recipients i (a ->id)%int lb lc ++
get_import_binding_recipients i (a ->id)%int lb li)) 1 = true ) as Hr.
rewrite ble_nat_reflection; auto.
rewrite Hr in e0.
exact e0.
SCase "False".
exact e0.
intros.
eapply Ha with (i0:=i1); auto.
Qed.
Lemma subcomponents_client_external_singleton_interfaces_spec':
forall lc,
forall e, In e (subcomponents_client_external_singleton_interfaces lc) ->
In (fst e) lc /\
snd e = get_interfaces_vis_role_card External Client Singleton (fst e->interfaces%comp).
Proof.
intros.
functional induction subcomponents_client_external_singleton_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.
Lemma client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec:
forall lc li lb,
(forall c', In c' lc ->
forall int : interface,
In int (c' ->interfaces)%comp ->
(int ->role)%int = Client ->
(int ->visibility)%int = External ->
(int ->cardinality)%int = Singleton ->
Datatypes.length
(get_normal_binding_recipients (c' ->id)%comp (int ->id)%int lb lc ++
get_import_binding_recipients (c' ->id)%comp (int ->id)%int lb li) <= 1) ->
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one lc li lb = true.
Proof.
destruct lc; intros; simpl; auto.
unfold client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one.
assert (forall e, In e (subcomponents_client_external_singleton_interfaces (c::lc)) ->
In (fst e) (c::lc) /\
snd e = get_interfaces_vis_role_card External Client Singleton (fst e->interfaces%comp)
) as Ha.
apply subcomponents_client_external_singleton_interfaces_spec'; auto.
destruct (subcomponents_client_external_singleton_interfaces (c :: lc)); auto.
apply client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec'; auto.
Qed.
Definition eqSingleton_normal_import c : Prop :=
client_singleton_are_bound_once_at_most_normal_import_bindings_bool c = true <->
client_singleton_are_bound_once_at_most_normal_import_bindings c.
Lemma nil_eqSingleton_normal_import: forall c, In c nil -> eqSingleton_normal_import c.
Proof.
intros.
inversion H.
Qed.
Lemma cons_eqSingleton_normal_import c (Hc : eqSingleton_normal_import c) lc (Hlc : forall c', In c' lc -> eqSingleton_normal_import c'):
forall c', In c' (cons c lc) -> eqSingleton_normal_import c'.
Proof.
intros.
destruct H; subst; auto.
Qed.
Lemma lc_eqSingleton_normal_import (Hp: forall c, eqSingleton_normal_import c) :
forall lc, (forall c', In c' lc -> eqSingleton_normal_import c').
Proof.
exact (fix lc_eqSingleton_normal_import lc :=
match lc as lc return (forall c', In c' lc -> eqSingleton_normal_import c') with
| nil => nil_eqSingleton_normal_import
| cons c lc => cons_eqSingleton_normal_import c (Hp c) lc (lc_eqSingleton_normal_import lc)
end).
Defined.
Theorem eqSingleton_normal_import_correctness:
forall c,
client_singleton_are_bound_once_at_most_normal_import_bindings_bool c = true <->
client_singleton_are_bound_once_at_most_normal_import_bindings c.
Proof.
fix 1; intros [i p ic cl lc li lb].
assert (HeqSingleton_normal_import_correctness :=
lc_eqSingleton_normal_import eqSingleton_normal_import_correctness lc);
clear eqSingleton_normal_import_correctness.
Guarded.
split; intro.
Case "Function Entails Predicate". Focus.
apply SingletonNormalImport; intros.
SCase "Singleton Requirement is Met".
Focus.
simpl in *.
clear HeqSingleton_normal_import_correctness.
rewrite andb_true_iff in H.
destruct H as (Ha, Hb).
clear Hb.
apply get_normal_binding_recipients_fact; auto.
SCase "Recursion on sub-levels".
simpl in *.
assert (eqSingleton_normal_import c') as Ha; auto.
clear HeqSingleton_normal_import_correctness.
unfold eqSingleton_normal_import in Ha.
assert (forall c, In c ((Component i p ic cl lc li lb)->subComponents%comp) ->
client_singleton_are_bound_once_at_most_normal_import_bindings_bool c = true) as Hb.
apply client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact; auto.
simpl in Hb.
assert (client_singleton_are_bound_once_at_most_normal_import_bindings_bool c' = true) as Hc.
apply Hb; auto.
clear Hb.
destruct Ha.
destruct (client_singleton_are_bound_once_at_most_normal_import_bindings_bool c').
SSCase "Its true".
apply H1; auto.
SSCase "Its false".
congruence.
Case "Predicate Entails Function".
unfold eqSingleton_normal_import in *.
simpl.
rewrite andb_true_iff.
inversion H; simpl in * |-.
split.
SCase "Current Hierarchical Level".
Focus.
apply client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec.
intros.
eapply H0 with (c':=c') (int:=int); auto.
SCase "Recursion".
clear -H1 HeqSingleton_normal_import_correctness Case SCase.
induction lc. auto.
destruct HeqSingleton_normal_import_correctness with (c':=a). left; auto.
rewrite andb_true_iff.
split.
clear IHlc.
assert (client_singleton_are_bound_once_at_most_normal_import_bindings a).
apply H1. left; auto.
apply H0; auto.
apply IHlc; intros; clear IHlc.
split; intro; intuition.
apply HeqSingleton_normal_import_correctness. right; auto.
auto.
apply H1. right; auto.
Qed.
Function check_server_singleton_requirement_normal_export cid li lb : bool :=
match li with
nil => true
| i :: r => let l := length (get_connected_clients_ids_from_interface_normal_export cid (i->id%int) lb) in
if ble_nat l 1 then
check_server_singleton_requirement_normal_export cid r lb
else
false
end.
Function server_singleton_are_bound_once_at_most_bool_one1 lc lb : bool :=
match lc with
nil => true
| c :: r => let ci := get_interfaces_vis_role_card External Server Singleton (c->interfaces%comp) in
if check_server_singleton_requirement_normal_export (c->id%comp) ci lb then
server_singleton_are_bound_once_at_most_bool_one1 r lb
else
false
end.
Function check_server_singleton_requirement_import li lb : bool :=
match li with
nil => true
| i :: r => let l := length (get_connected_clients_ids_from_interface_import (i->id%int) lb) in
if ble_nat l 1 then
check_server_singleton_requirement_import r lb
else
false
end.
Function server_singleton_are_bound_once_at_most_bool_one2 li lb : bool :=
let li' := get_interfaces_vis_role_card Internal Server Singleton li in
check_server_singleton_requirement_import li' lb.
Definition server_singleton_are_bound_once_at_most_bool_one lc li lb : bool :=
server_singleton_are_bound_once_at_most_bool_one1 lc lb &&
server_singleton_are_bound_once_at_most_bool_one2 li lb.
Fixpoint server_singleton_are_bound_once_at_most_bool c : bool :=
match c with
Component i p ic cl lc li lb => (server_singleton_are_bound_once_at_most_bool_one lc li lb) &&
((fix f_sub lc {struct lc} :=
match lc with
nil => true
| sc :: r => server_singleton_are_bound_once_at_most_bool sc && (f_sub r)
end
)
lc)
end.
Lemma server_singleton_are_bound_once_at_most_bool_one1_spec:
forall lc lb,
server_singleton_are_bound_once_at_most_bool_one1 lc lb = true ->
forall c, In c lc ->
forall i,
In i (c ->interfaces)%comp ->
isServerExternalSingleton i ->
Datatypes.length
(get_connected_clients_ids_from_interface_normal_export (c ->id)%comp
(i ->id)%int lb) <= 1.
Proof.
induction lc; simpl; intros; try fromfalse.
destruct H0; subst.
Case "Head". Focus.
clear IHlc.
assert (In i (get_interfaces_vis_role_card External Server Singleton (c ->interfaces)%comp)) as Ha.
Focus.
destruct c; simpl in *.
clear H.
functional induction get_interfaces_vis_role_card External Server Singleton l0.
inversion H1.
destruct H1; subst. left; auto.
right; apply IHl2; auto.
destruct H1; subst.
unfold isServerExternalSingleton in H2.
destruct H2 as (H', (H'', H''')).
rewrite H' in e0;
rewrite H'' in e0;
rewrite H''' in e0.
simpl in e0. congruence.
apply IHl2; auto.
induction ((get_interfaces_vis_role_card External Server Singleton
(c ->interfaces)%comp)).
inversion Ha.
destruct Ha; subst.
SCase "It is the head".
Focus.
simpl in H.
rewrite <- ble_nat_reflection.
destruct (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_normal_export
(c ->id)%comp (i ->id)%int lb)) 1); try congruence.
SCase "It's in the tail".
apply IHl; auto; clear IHl.
simpl in H.
destruct (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_normal_export
(c ->id)%comp (a ->id)%int lb)) 1); try congruence.
Case "In the Tail".
apply IHlc; auto; clear IHlc.
destruct (check_server_singleton_requirement_normal_export (a ->id)%comp
(get_interfaces_vis_role_card External Server Singleton
(a ->interfaces)%comp) lb); try congruence.
Qed.
Lemma server_singleton_are_bound_once_at_most_bool_one2_spec:
forall li lb,
server_singleton_are_bound_once_at_most_bool_one2 li lb = true ->
forall i, In i li ->
isServerInternalSingleton i ->
Datatypes.length (get_connected_clients_ids_from_interface_import (i ->id)%int lb) <= 1.
Proof.
induction li; intros; try fromfalse.
destruct H0; subst.
Case "Head".
clear IHli.
unfold server_singleton_are_bound_once_at_most_bool_one2 in H.
simpl in H.
replace (((i ->visibility)%int == Internal)%vis &&
((i ->role)%int == Server)%role &&
((i ->cardinality)%int == Singleton)%card) with true in H.
simpl in H.
rewrite <- ble_nat_reflection.
destruct (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_import (i ->id)%int lb)) 1); try congruence.
clear -Case H1.
symmetry.
repeat rewrite andb_true_iff.
destruct H1 as (H1, (H2, H3)).
rewrite <- role_eq_reflection in H1.
rewrite <- visibility_eq_reflection in H2.
rewrite <- cardinality_eq_reflection in H3.
repeat split; auto.
Case "Tail".
apply IHli; auto.
clear IHli.
unfold server_singleton_are_bound_once_at_most_bool_one2 in H.
simpl in H.
destruct (((a ->visibility)%int == Internal)%vis &&
((a ->role)%int == Server)%role &&
((a ->cardinality)%int == Singleton)%card); auto.
unfold server_singleton_are_bound_once_at_most_bool_one2.
simpl in H.
destruct (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_import (a ->id)%int lb))
1); try congruence.
Qed.
Lemma server_singleton_are_bound_once_at_most_bool_fact:
forall c,
server_singleton_are_bound_once_at_most_bool c = true ->
forall c', In c' (c->subComponents%comp) ->
server_singleton_are_bound_once_at_most_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 server_singleton_are_bound_once_at_most_bool_one_rev_spec:
forall lc lb li,
(forall c,
In c lc ->
forall i, In i (c ->interfaces)%comp ->
isServerExternalSingleton i ->
Datatypes.length
(get_connected_clients_ids_from_interface_normal_export (c ->id)%comp
(i ->id)%int lb) <= 1) ->
(forall i : interface,
In i li ->
isServerInternalSingleton i ->
Datatypes.length
(get_connected_clients_ids_from_interface_import (i ->id)%int lb) <= 1) ->
server_singleton_are_bound_once_at_most_bool_one lc li lb = true.
Proof.
intros.
unfold server_singleton_are_bound_once_at_most_bool_one.
rewrite andb_true_iff.
split.
Case "1/2". Focus.
clear H0.
functional induction server_singleton_are_bound_once_at_most_bool_one1 lc lb; auto.
SCase "1/2". Focus.
apply IHb; intros; clear IHb.
apply H; auto.
right; auto.
SCase "2/2".
assert (forall i : interface,
In i (c ->interfaces)%comp ->
isServerExternalSingleton i ->
Datatypes.length
(get_connected_clients_ids_from_interface_normal_export (c ->id)%comp
(i ->id)%int lb) <= 1) as Ha.
apply H; auto. left;auto.
clear H.
rewrite <- e0.
clear e0.
destruct c.
simpl in *.
induction l0.
refl.
simpl.
assert (((a ->visibility)%int == External)%vis &&
((a ->role)%int == Server)%role &&
((a ->cardinality)%int == Singleton)%card = true ->
isServerExternalSingleton a).
Focus.
intros.
repeat rewrite andb_true_iff in H.
destruct H as ((H', H''), H''').
unfold isServerExternalSingleton.
rewrite visibility_eq_reflection in H'.
rewrite role_eq_reflection in H''.
rewrite cardinality_eq_reflection in H'''.
repeat split; auto.
destruct ( ((a ->visibility)%int == External)%vis &&
((a ->role)%int == Server)%role &&
((a ->cardinality)%int == Singleton)%card).
SSCase "True". Focus.
simpl.
replace (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_normal_export i
(a ->id)%int lb)) 1) with true.
apply IHl0; intros.
apply Ha; auto. right; auto.
symmetry. apply ble_nat_reflection.
apply Ha; auto. left; auto.
SSCase "False".
apply IHl0; intros.
apply Ha; auto. right; auto.
Case "2/2".
clear H.
unfold server_singleton_are_bound_once_at_most_bool_one2.
functional induction get_interfaces_vis_role_card Internal Server Singleton li; auto.
SCase "1/2". Focus.
simpl.
replace (ble_nat
(Datatypes.length
(get_connected_clients_ids_from_interface_import (i ->id)%int lb)) 1) with
true.
apply IHl; intros.
apply H0; auto. right; auto.
symmetry.
apply ble_nat_reflection.
apply H0. left; auto.
repeat rewrite andb_true_iff in e0.
destruct e0 as ((H', H''), H''').
unfold isServerInternalSingleton.
rewrite visibility_eq_reflection in H'.
rewrite role_eq_reflection in H''.
rewrite cardinality_eq_reflection in H'''.
repeat split; auto.
SCase "2/2".
apply IHl; intros.
apply H0; auto. right; auto.
Qed.
Definition eqServerSingleton c : Prop :=
server_singleton_are_bound_once_at_most_bool c = true <->
server_singleton_are_bound_once_at_most c.
Lemma nil_eqServerSingleton: forall c, In c nil -> eqServerSingleton c.
Proof.
intros.
inversion H.
Qed.
Lemma cons_eqServerSingleton c (Hc : eqServerSingleton c) lc (Hlc : forall c', In c' lc -> eqServerSingleton c'):
forall c', In c' (cons c lc) -> eqServerSingleton c'.
Proof.
intros.
destruct H; subst; auto.
Qed.
Lemma lc_eqServerSingleton (Hp: forall c, eqServerSingleton c) :
forall lc, (forall c', In c' lc -> eqServerSingleton c').
Proof.
exact (fix lc_eqServerSingleton lc :=
match lc as lc return (forall c', In c' lc -> eqServerSingleton c') with
| nil => nil_eqServerSingleton
| cons c lc => cons_eqServerSingleton c (Hp c) lc (lc_eqServerSingleton lc)
end).
Defined.
Theorem eqServerSingleton_correctness:
forall c,
server_singleton_are_bound_once_at_most_bool c = true <->
server_singleton_are_bound_once_at_most c.
Proof.
fix 1; intros [i p ic cl lc li lb].
assert (HeqServerSingleton_correctness :=
lc_eqServerSingleton eqServerSingleton_correctness lc);
clear eqServerSingleton_correctness.
Guarded.
split; intro.
Case "Function Entails Predicate". Focus.
apply ServerSingleton; intros.
SCase "1/3".
simpl in *.
clear HeqServerSingleton_correctness.
rewrite andb_true_iff in H.
destruct H as (Ha, Hb).
clear Hb.
unfold server_singleton_are_bound_once_at_most_bool_one in Ha.
rewrite andb_true_iff in Ha.
destruct Ha as (Ha, Hb).
clear Hb.
apply server_singleton_are_bound_once_at_most_bool_one1_spec
with (lc:=lc); auto.
SCase "2/3". Focus.
simpl in *.
clear HeqServerSingleton_correctness.
rewrite andb_true_iff in H.
destruct H as (Ha, Hb).
clear Hb.
unfold server_singleton_are_bound_once_at_most_bool_one in Ha.
rewrite andb_true_iff in Ha.
destruct Ha as (Ha, Hb).
clear Ha.
apply server_singleton_are_bound_once_at_most_bool_one2_spec with
(li:=li); auto.
SCase "3/3".
simpl in *.
assert (eqServerSingleton c') as Ha; auto.
clear HeqServerSingleton_correctness.
unfold eqServerSingleton in Ha.
assert (forall c, In c ((Component i p ic cl lc li lb)->subComponents%comp) ->
server_singleton_are_bound_once_at_most_bool c = true) as Hb.
apply server_singleton_are_bound_once_at_most_bool_fact; auto.
simpl in Hb.
assert (server_singleton_are_bound_once_at_most_bool c' = true) as Hc.
apply Hb; auto.
clear Hb.
destruct Ha.
destruct (server_singleton_are_bound_once_at_most_bool c').
SSCase "Its true".
apply H1; auto.
SSCase "Its false".
congruence.
Case "Predicate Entails Function".
unfold eqServerSingleton in *.
simpl.
rewrite andb_true_iff.
inversion H; simpl in * |-.
split.
SCase "Current Hierarchical Level".
Focus.
clear H H2 HeqServerSingleton_correctness.
apply server_singleton_are_bound_once_at_most_bool_one_rev_spec; auto.
SCase "Recursion".
clear -H2 HeqServerSingleton_correctness Case SCase.
induction lc. auto.
destruct HeqServerSingleton_correctness with (c':=a). left; auto.
rewrite andb_true_iff.
split.
clear IHlc.
assert (server_singleton_are_bound_once_at_most a).
apply H2. left; auto.
apply H0; auto.
apply IHlc; intros; clear IHlc.
split; intro; intuition.
apply HeqServerSingleton_correctness. right; auto.
auto.
apply H2. right; auto.
Qed.
Require Import Coq.Logic.Decidable.
Theorem sound_cardinality_dec:
forall s, decidable (sound_cardinality s).
Proof.
intros.
unfold sound_cardinality.
unfold decidable.
unfold client_singleton_are_bound_once_at_most.
rewrite <- eqSingleton_normal_import_correctness.
rewrite <- eqSingleton_export_correctness.
destruct (client_singleton_are_bound_once_at_most_normal_import_bindings_bool s);
destruct (client_singleton_are_bound_once_at_most_export_bindings_bool s);
firstorder.
Qed.
Definition sound_cardinality_bool s :=
client_singleton_are_bound_once_at_most_export_bindings_bool s &&
client_singleton_are_bound_once_at_most_normal_import_bindings_bool s.
Theorem sound_cardinality_reflection:
forall s,
sound_cardinality s <->
sound_cardinality_bool s = true.
Proof.
intros.
unfold sound_cardinality;
unfold sound_cardinality_bool.
unfold client_singleton_are_bound_once_at_most.
rewrite <- eqSingleton_normal_import_correctness.
rewrite <- eqSingleton_export_correctness.
destruct (client_singleton_are_bound_once_at_most_normal_import_bindings_bool s);
destruct (client_singleton_are_bound_once_at_most_export_bindings_bool s);
firstorder.
Qed.
Definition sound_cardinality_correctness := sound_cardinality_reflection.