Mefresa.GCM.GCMWellFormedness
Function import_binding (idI idC idI':ident) (lc:list component) (li:list interface) : Prop :=
match lc[idC] with
| None => False
| Some c' =>
match li[idI, Internal]%int, (c'->interfaces%comp)[idI', External]%int with
| Some i, Some i' => (i->role%int) = Server /\ (i'->role%int) = Client
| _, _ => False
end
end.
Function export_binding (idI idC idI':ident) (lc:list component) (li:list interface) : Prop :=
match lc[idC] with
| None => False
| Some c' =>
match li[idI, Internal]%int, (c'->interfaces%comp)[idI', External]%int with
| Some i, Some i' => (i->role%int) = Client /\ (i'->role%int) = Server
| _, _ => False
end
end.
Function normal_binding (idC1 idI1 idC2 idI2:ident)
(lc:list component) (li:list interface) : Prop :=
match lc[idC1], lc[idC2] with
| Some c1, Some c2 =>
match (c1->interfaces%comp)[idI1, External]%int,
(c2->interfaces%comp)[idI2, External]%int with
| Some i, Some i' => (i->role%int) = Client /\ (i'->role%int) = Server
| _, _ => False
end
| _, _ => False
end.
Definition valid_binding (b:binding) (lc:list component) (li:list interface) : Prop :=
match b with
| Normal p idC1 idI1 idC2 idI2 => normal_binding idC1 idI1 idC2 idI2 lc li
| Export p idI idC idI' => export_binding idI idC idI' lc li
| Import p idI idC idI' => import_binding idI idC idI' lc li
end.
Lemma valid_binding_may_entail_false:
forall b li,
valid_binding b nil li -> False.
Proof.
intros.
destruct b; simpl in *.
Case "Normal Binding".
inversion H.
Case "Export Binding".
inversion H.
Case "Import Binding".
inversion H.
Qed.
Hint Resolve valid_binding_may_entail_false.
Definition well_formed_bindings lb lc li : Prop :=
forall b, In b lb -> valid_binding b lc li.
Lemma well_formed_bindings_entailment:
forall lb li, well_formed_bindings lb nil li -> lb = nil.
Proof.
intros.
destruct lb; auto.
unfold well_formed_bindings in H.
assert (valid_binding b nil li).
apply H; left; auto.
compute in H0.
destruct b; fromfalse.
Qed.
Inductive not_in_l_pairs (i : ident) (a : visibility) (l : list interface) : Prop :=
NotInPair_Nil : l = (nil:list interface) -> not_in_l_pairs i a l
| NotInPairStep : forall (int : interface) (r : list interface),
l = int :: r ->
((int ->id)%int == i) && ((int ->visibility)%int == a)%vis = false ->
not_in_l_pairs i a r ->
not_in_l_pairs i a l.
Definition not_in_list_pairs (i:ident) (a: visibility) (l:list interface) : Prop :=
forall e, In e l -> (((e->id)%int == i) &&
(e->visibility%int == a)%vis = false).
Lemma same_nots_pair:
forall i a l, not_in_l_pairs i a l -> not_in_list_pairs i a l.
Proof.
induction 1.
Case "List is Nil".
subst.
unfold not_in_list_pairs.
intros.
inversion H.
Case "List is no Nil".
subst.
unfold not_in_list_pairs.
intros.
destruct H.
SCase "Head of the list".
subst.
exact H0.
SCase "It's in the tail of the list".
unfold not_in_list_pairs in IHnot_in_l_pairs.
apply IHnot_in_l_pairs.
exact H.
Qed.
Inductive unique_pairs (li: list interface) : Prop :=
| UniquePairs_Base: li = nil -> unique_pairs li
| UniquePairs_Step: forall int r,
li = int :: r ->
not_in_l_pairs (int->id)%int (int->visibility)%int r ->
unique_pairs r ->
unique_pairs li.
Inductive well_formed_interfaces (li:list interface) : Prop :=
| WellFormedInterfaces_Base: li=nil ->
well_formed_interfaces li
| WellFormedInterfaces_Step: forall i r,
li = i :: r ->
unique_pairs li ->
well_formed_interfaces r ->
well_formed_interfaces li.
Definition well_formed_interfaces' (li:list interface) : Prop := unique_pairs li.
Lemma same_well_formed_interfaces:
forall li, well_formed_interfaces li <-> well_formed_interfaces' li.
Proof.
induction li; split; intro.
Case "List is nil, Left entails Right".
unfold well_formed_interfaces'.
apply UniquePairs_Base; auto.
Case "List is nil, Right entails Left".
apply WellFormedInterfaces_Base; auto.
Case "List is not nil, Left entails Right".
unfold well_formed_interfaces'.
apply UniquePairs_Step with (int:=a) (r:=li); auto.
inversion H; inversion H0; subst.
inversion H1; inversion H3; subst; auto.
destruct IHli.
assert (well_formed_interfaces li).
inversion H; inversion H2; subst.
destruct r; auto.
inversion H2; subst; auto.
apply UniquePairs_Base; auto.
Case "List is not nil, Right entails Left".
apply WellFormedInterfaces_Step with (i:=a) (r:=li); auto.
destruct IHli.
apply H1.
inversion H; inversion H2; subst. clear H2.
unfold well_formed_interfaces'; auto.
Qed.
Inductive well_formed_component c : Prop :=
| WellFormedComponent:
(forall c',
In c' (c->subComponents%comp) ->
well_formed_component c' ) ->
unique_ids (c->subComponents%comp) ->
well_formed_interfaces (c->interfaces)%comp ->
well_formed_bindings (c->bindings)%comp (c->subComponents)%comp (c->interfaces)%comp ->
well_formed_component c.
Definition well_formed_components cl : Prop :=
unique_ids cl /\
forall c, In c cl -> well_formed_component c.
Lemma well_formed_nil_components:
well_formed_components nil.
Proof.
split; auto.
intros.
thus inversion H.
Qed.
Lemma well_formed_components_have_unique_ids:
forall l,
well_formed_components l ->
unique_ids l.
Proof.
intros.
inversion H; auto.
Qed.
Hint Resolve well_formed_components_have_unique_ids.
Lemma well_formed_nil_interfaces:
well_formed_interfaces nil.
Proof.
apply WellFormedInterfaces_Base; auto.
Qed.
Lemma well_formed_nil_bindings:
forall c, (c->bindings%comp) = nil ->
well_formed_bindings (c->bindings)%comp (c->subComponents)%comp (c->interfaces)%comp.
Proof.
intros.
rewrite H.
unfold well_formed_bindings; intros.
inversion H0.
Qed.
Hint Resolve well_formed_nil_components
well_formed_nil_interfaces
well_formed_nil_bindings.
Lemma well_formed_nil_bindings':
forall lc li, well_formed_bindings nil lc li.
Proof.
intros.
intro. intro.
inversion H.
Qed.
Hint Resolve well_formed_nil_bindings'.
Lemma well_formed_empty_component:
forall id p cl, well_formed_component (Component id p default_class cl nil nil nil).
Proof.
intros.
apply WellFormedComponent; simpl; intros; auto; try fromfalse.
Qed.
Hint Resolve well_formed_empty_component.
Lemma well_formed_component_individuals:
forall lc, well_formed_components lc ->
forall c, In c lc ->
well_formed_component c.
Proof.
intros.
unfold well_formed_components in H.
destruct H.
thus apply H1; auto.
Qed.
Lemma well_formed_tail:
forall c r,
well_formed_components (c :: r) ->
well_formed_components r.
Proof.
intros.
inversion H.
split.
Case "Unique Ids".
inversion H0; inversion H2; subst; auto.
Case "Well Formed Component".
intros.
apply H1; right; auto.
Qed.
Lemma unique_subset':
forall c r acc,
unique_ids ((c :: r) ++ acc) ->
unique_ids (r ++ c :: acc).
Proof.
intros.
assert (unique_ids acc).
apply unique_subset_gen with (l1:=c::r); auto.
destruct r.
Case "R is Nil".
rewrite app_nil_l.
apply Unique_Step with (c:=c) (r:=acc);auto.
inversion H; inversion H1; subst; auto.
Case "R is Not Nil".
apply Unique_Step with (c:=c0) (r:= r ++ c :: acc); auto.
SCase "First is not in tail".
inversion H; inversion H1; subst. clear H1.
apply same_nots in H2.
apply same_nots'.
unfold not_in_list in *; intros.
assert (In e r \/ In e (c1 :: acc)).
apply in_app_or; auto.
assert (((c0 ->id)%comp == (c1 ->id)%comp) = false).
apply H2; left; auto.
destruct H4.
SSCase "In e r".
apply unique_ids_fact with (r:=r++acc); auto.
intuition.
SSCase "In e (c1 :: acc)".
clear H1.
destruct H4; subst.
rewrite beq_ident_symmetry; auto.
apply unique_ids_fact with (r:=r++acc); auto.
intuition.
SCase "Tail has unique Ids".
inversion H; inversion H1; subst. clear H1.
induction r.
SSCase "R is Nil".
rewrite app_nil_l in *.
apply Unique_Step with (c:=c1) (r:=acc); auto.
apply same_nots in H2.
apply same_nots'.
unfold not_in_list in *; intros.
apply H2;auto.
right; auto.
SSCase "Not Nil".
apply Unique_Step with (c:=a) (r:=(r ++ c1 :: acc)); auto.
SSSCase "First is not in tail".
apply same_nots in H2.
apply same_nots'.
unfold not_in_list in *; intros.
assert (In e r \/ In e (c1 :: acc)).
apply in_app_or; auto.
assert (((a ->id)%comp == (c1 ->id)%comp) = false).
apply H2; right; left; auto.
destruct H4.
SSSSCase "In e r".
apply unique_ids_fact with (r:=r++acc).
inversion H3; inversion H6; subst; auto.
intuition.
SSSSCase "In e (c1 :: acc)".
clear H1.
destruct H4; subst.
rewrite beq_ident_symmetry; auto.
apply unique_ids_fact with (r:=r++acc); auto.
inversion H3; inversion H4; subst; auto.
intuition.
SSSCase "Unique Ids".
assert (unique_ids acc).
apply unique_subset_gen with (l1:=c0 :: (a :: r)); auto.
apply IHr; clear IHr.
SSSSCase "First Induction Hyp".
apply same_nots in H2.
apply same_nots'.
unfold not_in_list in *; intros.
assert (((a ->id)%comp == (c1 ->id)%comp) = false).
apply H2; right; left; auto.
destruct H4; subst.
SSSSSCase "aaa".
apply unique_ids_fact with (r:=(e :: a :: r ++ acc)).
inversion H3; inversion H4; subst; auto.
intuition.
SSSSSCase "bbb".
clear H1.
apply unique_ids_fact with (r:=c0 :: a :: r ++ acc); auto.
inversion H3; inversion H1; subst; auto.
intuition.
SSSSCase "Second Induction Hyp".
inversion H3; inversion H4; subst. clear H4.
apply Unique_Step with (c:=c) (r:=r++acc); auto.
inversion H5; inversion H4; subst; auto.
inversion H6; inversion H4; subst; auto.
SSSSCase "Third induction Hyp".
apply Unique_Step with (c:=c1) (r:=c0 :: r ++acc); auto.
apply same_nots in H2.
apply same_nots'.
unfold not_in_list in *; intros.
apply H2;auto.
destruct H4; subst.
left;auto.
right; right; auto.
inversion H3; inversion H4; subst. clear H4.
apply Unique_Step with (c:=c) (r:=r ++acc); auto.
apply same_nots in H5.
apply same_nots'.
unfold not_in_list in *; intros.
apply H5;auto.
right; auto.
inversion H6; inversion H4; subst; auto.
Qed.
Hint Resolve unique_subset unique_subset'.
Lemma well_formed_subset:
forall c r acc,
well_formed_components ((c :: r) ++ acc) ->
well_formed_components (c :: acc).
Proof.
intros.
assert (forall x, In x (c :: acc) -> In x ((c :: r) ++ acc)).
intros.
destruct H0; subst.
left; auto.
right.
intuition.
split.
Case "Unique IDs".
apply unique_subset with (r:=r); auto.
Case "Well formed Components".
inversion H; auto.
Qed.
Lemma well_formed_subset':
forall c r acc,
well_formed_components ((c :: r) ++ acc) ->
well_formed_components (r ++ c :: acc).
Proof.
intros.
assert (forall x, In x (r ++ c :: acc) -> In x ((c :: r) ++ acc)).
intros.
apply in_app_or in H0.
destruct H0; intuition.
destruct H0; subst; intuition.
split.
Case "Unique Ids".
inversion H; auto.
Case "Well Formed Component".
intros.
assert (In c0 ((c :: r) ++ acc)).
intuition.
apply well_formed_component_individuals with (lc:=((c :: r) ++ acc)); auto.
Qed.
Hint Resolve well_formed_subset well_formed_subset' well_formed_tail.
Lemma well_formed_bindings_may_entail_false:
forall b lb li,
well_formed_bindings (b :: lb) nil li -> False.
Proof.
intros.
unfold well_formed_bindings in H.
assert (valid_binding b nil li).
apply H.
left;auto.
eauto.
Qed.
Hint Resolve well_formed_bindings_may_entail_false.
Lemma well_formed_inheritance:
forall c, well_formed_component c ->
well_formed_components (c->subComponents%comp).
Proof.
intros.
inversion H; subst.
unfold well_formed_components.
split.
Case "Unique Ids".
thus auto.
Case "Well Formed Components".
intros. thus apply H0.
Qed.
Hint Resolve well_formed_inheritance.
Lemma stronger_inheritance:
forall c,
well_formed_component c ->
(well_formed_components (c->subComponents%comp) /\
well_formed_bindings (c->bindings)%comp (c->subComponents)%comp (c->interfaces)%comp /\
well_formed_interfaces (c->interfaces%comp)
).
Proof.
intros.
split; auto.
split.
Case "Well formed Bindings".
inversion H.
thus auto.
Case "Well formed Interfaces".
inversion H; auto.
Qed.
Lemma interfaces_are_well_formed:
forall c,
well_formed_component c -> (well_formed_interfaces (c->interfaces%comp)).
Proof.
intros.
inversion H; eauto.
Qed.
Lemma well_formed_entail_unique_ids:
forall c,
well_formed_component c -> (unique_ids (c->subComponents%comp)).
Proof.
intros.
inversion H; auto.
Qed.
Hint Resolve stronger_inheritance interfaces_are_well_formed well_formed_entail_unique_ids.
Lemma well_formed_empty_component':
forall id p cl, well_formed_component (Component id p default_class cl nil nil nil).
Proof.
intros.
split; intros; simpl in *; try fromfalse; auto.
Qed.