Mefresa.Operation.HeavyLifting
In this section we prove all the auxiliary lemmas necessary for
our development. All the gory details are depicted, if you're
looking for all the subtleties, you're in the right place!
Most proofs are closely tied with the chosen structures for our
development, making sometimes the most relevant aspects lost
into all the intricacies demanded by Coq. It should be noted
that the remaining files are still
readable if the reader
decides to skip this section.
For the brave ones, here you go!
Making Well Formed Components!
Lemma well_formed_append:
forall c comp_list lb,
well_formed_component c ->
well_formed (Component (Ident "Root") root "null" Configuration comp_list nil lb) ->
not_in_l (c->id)%comp comp_list ->
well_formed_components (c:: comp_list).
Proof.
intros.
unfold well_formed_components.
split.
Case "No ID clash between components".
apply Unique_Step with (c:=c) (r:=comp_list); auto.
inversion H0.
destruct H3 as (Hr, (Hic, (Hc, (Hp, Hw)))).
thus inversion Hw; simpl in *; subst; auto.
Case "Well Formed Individuals".
intros.
destruct H2; subst; auto.
inversion H0.
destruct H4 as (Hr, (Hic, (Hc, (Hp, Hw)))).
thus destruct well_formed_inheritance with
(c:=Component (Ident "Root") root "null" Configuration comp_list nil lb); auto.
Qed.
Lemma well_formed_append':
forall c comp_list,
well_formed_component c ->
well_formed_components comp_list ->
not_in_l (c->id)%comp comp_list ->
well_formed_components (c:: comp_list).
Proof.
intros.
unfold well_formed_components.
split.
Case "No ID clash between components".
apply Unique_Step with (c:=c) (r:=comp_list); auto.
Case "Well Formed Individuals".
intros.
destruct H2; subst; auto.
inversion H0; simpl in *; subst; eauto.
Qed.
Hint Resolve well_formed_component_individuals
well_formed_append well_formed_append'.
Lemma get_component_with_path_dec:
forall p s,
well_formed_component s ->
(exists c, Some c = get_component_with_path p s /\
well_formed_component c) \/
None = get_component_with_path p s.
Proof.
intros.
unfold get_component_with_path.
destruct p; auto.
destruct s.
inversion H; simpl in * |-; subst.
clear H H2 H3.
functional induction get_component_with_path_aux (i :: p) l; auto.
SCase "1/2".
functional induction get_component id li; auto.
left.
exists e; split; auto.
apply H0;auto. left; auto.
apply IHo;auto.
intros.
apply H0; right; auto.
inversion H1; inversion H; subst; auto.
SCase "2/2".
apply IHo; auto; clear IHo.
intros.
assert (In c0 li).
eauto.
assert (well_formed_component c0).
apply H0; auto.
assert (well_formed_components (c0 ->subComponents)%comp).
auto.
eauto.
assert (In c0 li).
eauto.
assert (well_formed_component c0).
apply H0; auto.
assert (well_formed_components (c0 ->subComponents)%comp).
auto.
eauto.
Qed.
Lemma bindings_unaffected:
forall c c' lc ,
c' = update_sub_components c lc ->
(c'->bindings)%comp = (c->bindings)%comp.
Proof.
intros.
functional induction update_sub_components c lc.
thus subst; refl.
Qed.
Hint Resolve bindings_unaffected.
Lemma well_formed_subcomponents_update:
forall c lc, well_formed_component c ->
well_formed_components lc ->
forall c',
c' = update_sub_components c lc ->
well_formed_bindings (c'->bindings)%comp (c'->subComponents)%comp (c'->interfaces)%comp ->
well_formed_component c'.
Proof.
intros.
functional induction update_sub_components c lc.
apply WellFormedComponent; intros; subst; eauto; simpl.
inversion H; auto.
Qed.
Lemma well_formed_component_has_subcomponents_w_unique_ids:
forall id p ic cl lc li lb,
well_formed_component (Component id p ic cl lc li lb) ->
unique_ids lc.
Proof.
intros.
inversion H; simpl in *; subst; auto.
Qed.
Hint Resolve well_formed_component_has_subcomponents_w_unique_ids.
Lemma well_formed_component_has_well_formed_interfaces:
forall id p ic cl lc li lb,
well_formed_component (Component id p ic cl lc li lb) ->
well_formed_interfaces li.
Proof.
intros.
inversion H; auto.
Qed.
Hint Resolve well_formed_component_has_well_formed_interfaces.
Lemma well_formed_component_has_well_formed_sub_components:
forall i p ic c lc li lb,
well_formed_component (Component i p ic c lc li lb) ->
well_formed_components lc.
Proof.
intros.
inversion H; simpl in *; subst; auto.
split; auto.
Qed.
Hint Resolve well_formed_component_has_well_formed_sub_components.
Lemma same_by_ids:
forall id c c' l r,
unique_ids l ->
l [id] = Some c ->
forall X,
lookup_aux l id X = Some (c', r) ->
c = c'.
Proof.
intros.
unfold lookup in H1.
functional induction lookup_aux l id X.
Case "Branch 1/3".
thus inversion H1.
Case "Branch 2/3".
inversion H1; subst. clear H1.
unfold get_component in H0.
rewrite e0 in H0.
thus inversion H0; subst; auto.
Case "Branch 3/3".
apply IHo; eauto.
unfold get_component in H0.
rewrite e0 in H0.
thus fold get_component in H0; auto.
Qed.
Hint Resolve same_by_ids.
Lemma valid_path_step:
forall li id c1 r rp,
well_formed_components li ->
lookup li id = Some (c1, r) ->
valid_path (id :: rp) li ->
valid_path rp (c1 ->subComponents)%comp.
Proof.
intros.
inversion H1.
Case "Path is nil".
thus inversion H2.
Case "Path is not nil".
inversion H2; subst. clear H2.
assert (In s' li).
eauto.
assert (c1->id%comp = i).
eauto.
assert (s'->id%comp = i).
eauto.
assert (In c1 li).
eauto.
assert (c1 = s').
inversion H.
symmetry.
thus apply same_by_ids with (id:=i) (l:=li) (r:=r) (X:=nil); eauto.
thus subst; auto.
Qed.
Lemma transitive_inheritance':
forall lc c,
well_formed_components lc ->
forall p, valid_path p lc ->
get_component_with_path_aux p lc = Some c->
well_formed_component c.
Proof.
intros.
functional induction get_component_with_path_aux p lc.
Case "1/4".
inversion H1.
Case "2/4".
assert (In c li).
apply membership_fact with (id:=id); auto.
inversion H.
apply H4; auto.
Case "3/4".
thus inversion H1.
Case "4/4".
simpl in *.
apply IHo; auto.
SCase "1/3".
assert (forall c, In c li -> well_formed_components (c->subComponents)%comp).
intros. apply well_formed_inheritance.
apply well_formed_component_individuals with (lc:=li); auto.
apply H2; auto.
apply lookup_solution_fact with (id:=id) (r:=r); auto.
SCase "2/3".
clear IHo y.
unfold valid_component_path in *.
simpl in *.
apply valid_path_step with (li:=li) (id:=id) (r:=r); auto.
Qed.
Lemma transitive_inheritance:
forall s c,
well_formed_components (s->components)%st ->
forall p, valid_component_path p s ->
get_component_with_path p s = Some c->
well_formed_component c.
Proof.
intros.
destruct s; simpl in *.
unfold valid_component_path in H0.
simpl in H0.
unfold get_component_with_path in H1.
destruct p. inversion H1.
apply transitive_inheritance' with (lc:=l) (c:=c) (p:= (i1 :: p));auto.
Qed.
Hint Resolve valid_path_step transitive_inheritance' transitive_inheritance.
Lemma update_sub_comp_maitains_id:
forall c lc,
((update_sub_components c lc)->id)%comp = (c->id)%comp.
Proof.
intros.
functional induction update_sub_components c lc; auto.
Qed.
Hint Resolve update_sub_comp_maitains_id.
Lemma update_sub_comp_red:
forall c lc,
(update_sub_components c lc ->subComponents)%comp = lc.
Proof.
intros.
functional induction update_sub_components c lc; auto.
Qed.
Lemma update_sub_comp_red':
forall c lc,
(update_sub_components c lc ->interfaces)%comp = (c->interfaces)%comp.
Proof.
intros.
functional induction update_sub_components c lc; auto.
Qed.
Lemma update_sub_comp_red'':
forall c lc,
(update_sub_components c lc ->bindings)%comp = (c->bindings)%comp.
Proof.
intros.
functional induction update_sub_components c lc; auto.
Qed.
Hint Resolve update_sub_comp_red update_sub_comp_red' update_sub_comp_red''.
Lemma get_comp_fact:
forall lc id c c',
lc [id] = Some c ->
well_formed_components ((c' :: lc)) ->
(c' :: lc) [id] = Some c.
Proof.
intros.
inversion H0.
assert ( ( id == (c'->id%comp)) = false).
clear H2.
inversion H1;
inversion H2; subst. clear H2.
assert (In c r).
eauto.
assert (c->id%comp = id).
eauto.
subst.
apply same_nots in H3.
unfold not_in_list in H3.
apply H3;auto.
unfold get_component.
apply beq_ident_symmetry' in H3.
rewrite H3; auto.
Qed.
Hint Resolve get_comp_fact.
Lemma adding_comp_maintains_valid_bindings:
forall b lc li c,
well_formed_components (c :: lc) ->
valid_binding b lc li ->
valid_binding b (c :: lc) li.
Proof.
intros.
destruct b; simpl in *.
Case "Normal Binding".
functional induction normal_binding i i0 i1 i2 lc li.
SCase "Exit Branch 1/3".
unfold normal_binding.
assert ((c :: lc) [i] = Some c1).
auto.
rewrite H1. clear H1 e.
assert ((c :: lc) [i1] = Some c2).
auto.
rewrite H1. clear H1 e0.
rewrite e1.
rewrite e2; auto.
SSCase "Exit Branch 2/3".
inversion H0.
SSCase "Exit Branch 3/3".
inversion H0.
SCase "Export Binding".
functional induction export_binding i i0 i1 lc li.
SSCase "Exit Branch 1/3".
inversion H0.
SSCase "Exit Branch 2/3".
unfold export_binding.
assert ((c :: lc) [i0] = Some c').
auto.
rewrite H1; clear H1 e.
rewrite e0.
rewrite e1; auto.
SSCase "Exit Branch 3/3".
inversion H0.
SCase "Import Binding".
functional induction import_binding i i0 i1 lc li.
SSCase "Exit Branch 1/3".
inversion H0.
SSCase "Exit Branch 2/3".
unfold import_binding.
assert ((c:: lc) [i0] = Some c').
auto.
rewrite H1. clear H1.
rewrite e0.
rewrite e1; auto.
SSCase "Exit Branch 3/3".
inversion H0.
Qed.
Hint Resolve adding_comp_maintains_valid_bindings.
Lemma adding_comp_keeps_bindings_well_formed:
forall lb lc li c,
well_formed_bindings lb lc li ->
well_formed_components (c :: lc) ->
well_formed_bindings lb (c :: lc) li.
Proof.
intros.
unfold well_formed_bindings in H.
intro. intro.
assert (valid_binding b lc li).
apply H; auto.
auto.
Qed.
Hint Resolve adding_comp_keeps_bindings_well_formed.
Lemma well_formed_bindings_in_nil:
forall lb lc li,
well_formed_bindings lb nil li ->
well_formed_bindings lb lc li.
Proof.
intros.
unfold well_formed_bindings in H.
intro. intro.
assert (valid_binding b nil li).
apply H; auto.
compute in H1.
destruct b; fromfalse.
Qed.
Hint Resolve well_formed_bindings_in_nil.
Lemma add_comp_may_entail_false:
forall lc p c,
well_formed_components lc ->
valid_path p lc ->
add_component_aux lc p c = nil ->
False.
Proof.
intros.
functional induction add_component_aux lc p c;
inversion H1; clear H1.
Case "Exit Branch 1/2".
Focus.
inversion H0;
inversion H1; clear H1; subst.
assert (False).
eauto.
inversion H1.
Case "Exit Branch 2/2".
apply IHl; eauto.
Qed.
Hint Resolve add_comp_may_entail_false.
Lemma get_component_fact:
forall id p ic cl lc lc' li lb r i,
forall x,
(Component id p ic cl lc li lb :: r) [i] = Some x ->
(Component id p ic cl lc' li lb :: r) [i] = Some x \/
(Component id p ic cl lc' li lb :: r) [i] = (Some (Component id p ic cl lc' li lb)).
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=i).
Case "Ids are Equal".
assert ((id == i) = true).
eauto.
right.
simpl; rewrite H0; auto.
Case "Ids are not Equal".
left.
assert ((id == i) = false).
eauto.
simpl in *; rewrite H0 in *; auto.
Qed.
Lemma get_component_fact':
forall id p ic cl lc li' li lb r i,
forall x,
(Component id p ic cl lc li lb :: r) [i] = Some x ->
(Component id p ic cl lc li' lb :: r) [i] = Some x \/
(Component id p ic cl lc li' lb :: r) [i] = (Some (Component id p ic cl lc li' lb)).
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=i).
Case "Ids are Equal".
assert ((id == i) = true).
eauto.
right.
simpl; rewrite H0; auto.
Case "Ids are not Equal".
left.
assert ((id == i) = false).
eauto.
simpl in *; rewrite H0 in *; auto.
Qed.
Hint Resolve get_component_fact get_component_fact'.
Lemma get_component_fact_same_interfaces:
forall id p ic cl lc lc' li lb r i,
forall x y,
(Component id p ic cl lc li lb :: r) [i] = Some x ->
(Component id p ic cl lc' li lb :: r) [i] = Some y ->
(x->interfaces)%comp = (y->interfaces)%comp.
Proof.
intros.
destruct get_component_fact with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc)
(lc':=lc') (li:=li) (lb:=lb) (r:=r) (i:=i) (x:=x); auto.
Case "Head of the list".
assert (x = y).
rewrite H1 in H0.
inversion H0;auto.
destruct x; destruct y; simpl.
inversion H2;auto.
Case "Not the Head of the List".
rewrite H1 in H0.
destruct ident_dec with (id1:=id) (id2:=i).
SCase "Ids are equal".
assert ((id == i) = true).
eauto.
unfold get_component in H.
simpl in H.
rewrite H2 in H.
destruct x.
inversion H; subst.
simpl.
destruct y; simpl; subst.
inversion H0; auto.
SCase "Ids are not equal".
assert ((id == i) = false).
eauto.
unfold get_component in H; simpl in H.
rewrite H2 in H.
fold get_component in H.
unfold get_component in H1; simpl in H1.
rewrite H2 in H1.
fold get_component in H1.
clear n H2.
assert (x = Component id p ic cl lc' li lb).
rewrite H in H1.
inversion H1; auto.
destruct x; inversion H2; subst.
destruct y; simpl.
inversion H0; auto.
Qed.
Hint Resolve get_component_fact_same_interfaces.
Lemma valid_binding_fact:
forall id p ic cl lc li li' lb r b lc',
valid_binding b (Component id p ic cl lc' li lb :: r) li' ->
valid_binding b (Component id p ic cl lc li lb :: r) li'.
Proof.
intros.
destruct b; simpl in *.
Case "Normal Binding".
functional induction normal_binding i i0 i1 i2 (Component id p ic cl lc' li lb :: r) li';
try inversion H.
unfold normal_binding.
destruct get_component_fact with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc')
(lc':=lc) (li:=li) (lb:=lb) (r:=r) (i:=i) (x:=c1);
destruct get_component_fact with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc')
(lc':=lc) (li:=li) (lb:=lb) (r:=r) (i:=i1) (x:=c2); auto.
SCase "Both Not Head of the List".
rewrite H3; rewrite H2; rewrite e1; rewrite e2; auto.
SCase "Not Head od the list, Head of the List".
rewrite H2; rewrite e1.
rewrite H3.
assert ((c2 ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
simpl. simpl in H4.
rewrite H4 in e2.
rewrite e2; auto.
SCase "Head of the list, not head of the list".
rewrite H2; rewrite H3.
rewrite e2.
assert ((c1 ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
simpl. simpl in H4.
rewrite H4 in e1.
rewrite e1; auto.
SCase "Both Head of the list".
rewrite H2; rewrite H3.
assert ((c1 ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
assert ((c2 ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
simpl; simpl in H5; simpl in H4.
rewrite H4 in e1.
rewrite H5 in e2.
rewrite e1; rewrite e2; auto.
Case "Export Binding".
functional induction export_binding i i0 i1 (Component id p ic cl lc' li lb :: r) li';
try inversion H.
unfold export_binding.
destruct get_component_fact with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc')
(lc':=lc) (li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'); auto.
SCase "Not the Head of the List".
rewrite H2; rewrite e1; auto.
rewrite e0; auto.
SCase "The Head of the list".
rewrite H2; rewrite e0.
assert ((c' ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
simpl; simpl in H3.
rewrite H3 in e1.
rewrite e1; auto.
Case "Import Binding".
functional induction import_binding i i0 i1 (Component id p ic cl lc' li lb :: r) li';
try inversion H.
unfold import_binding.
destruct get_component_fact with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc')
(lc':=lc) (li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'); auto.
SCase "Not the Head of the List".
rewrite H2; rewrite e1; auto.
rewrite e0; auto.
SCase "The Head of the list".
rewrite H2; rewrite e0.
assert ((c' ->interfaces)%comp = (Component id p ic cl lc li lb->interfaces%comp)).
eapply get_component_fact_same_interfaces; eauto.
simpl; simpl in H3.
rewrite H3 in e1.
rewrite e1; auto.
Qed.
Hint Resolve valid_binding_fact.
Lemma update_w_bindings_reduction_fact:
forall lb c' lc backup li,
well_formed_bindings lb (c' :: backup) li ->
well_formed_bindings
lb
(update_sub_components c' lc :: backup)
li.
Proof.
intros.
functional induction update_sub_components c' lc.
unfold well_formed_bindings in H.
intro. intro.
assert (valid_binding b (Component id p iclass cl lc' li0 lb0 :: backup) li).
apply H; auto.
eauto.
Qed.
Hint Resolve update_w_bindings_reduction_fact.
Lemma update_w_valid_bindings_reduction_fact:
forall b c backup li lc,
valid_binding b (c :: backup) li ->
valid_binding b (update_sub_components c lc :: backup) li.
Proof.
intros.
functional induction update_sub_components c lc;
eauto.
Qed.
Hint Resolve update_w_valid_bindings_reduction_fact.
Lemma valid_binding_lookup_fact:
forall lc id c r b li,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
valid_binding b lc li ->
valid_binding b (c :: r) li.
Proof.
intros.
inversion H.
destruct b; simpl in *.
Case "Normal Binding".
functional induction normal_binding i i0 i1 i2 lc li.
SCase "Exit Branch 1/3".
assert ((c::r)[i] = Some c1).
apply lookup_get_fact' with (id:=id) (lc:=lc); auto.
assert ((c::r)[i1] = Some c2).
apply lookup_get_fact' with (id:=id) (lc:=lc); auto.
unfold normal_binding;
rewrite H5; rewrite H4.
rewrite e1; rewrite e2; auto.
SCase "Exit Branch 2/3".
inversion H1.
SCase "Exit Branch 3/3".
inversion H1.
Case "Export Binding".
functional induction export_binding i i0 i1 lc li.
SCase "Exit Branch 1/3".
inversion H1.
SCase "Exit Branch 2/3".
assert((c::r)[i0]=Some c').
apply lookup_get_fact' with (id:=id) (lc:=lc); auto.
unfold export_binding;
rewrite H4;
rewrite e1; rewrite e0; auto.
SSCase "Exit Branch 3/3".
inversion H1.
SCase "Import Binding".
functional induction import_binding i i0 i1 lc li.
SSCase "Exit Branch 1/3".
inversion H1.
SSCase "Exit Branch 2/3".
assert ((c::r)[i0] = Some c').
apply lookup_get_fact' with (id:=id) (lc:=lc); auto.
unfold import_binding;
rewrite H4; rewrite e1; rewrite e0;auto.
SSCase "Exit Branch 3/3".
inversion H1.
Qed.
Hint Resolve valid_binding_lookup_fact.
Lemma bindings_lookup_fact:
forall lc id c r lb li,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
well_formed_bindings lb lc li ->
well_formed_bindings lb (c :: r) li.
Proof.
intros.
unfold well_formed_bindings in H1.
intro. intro.
assert (valid_binding b lc li).
apply H1; auto.
eauto.
Qed.
Hint Resolve bindings_lookup_fact.
Lemma updating_comps_bindings:
forall c' p c,
well_formed_component c' ->
well_formed_components (add_component_aux (c' ->subComponents)%comp p c) ->
valid_path p (c'->subComponents%comp) ->
well_formed_bindings (c' ->bindings)%comp
(update_sub_components c' (add_component_aux (c' ->subComponents) p c) ->subComponents)%comp
(c'->interfaces)%comp.
Proof.
intros.
assert (well_formed_components (c' ->subComponents)%comp ).
apply well_formed_inheritance; auto.
inversion H; subst.
Case "Sub Components are Not Nil".
assert ( ((update_sub_components c' (add_component_aux (c' ->subComponents) p c) ->subComponents)%comp)
= (add_component_aux (c' ->subComponents)%comp p c) ).
auto.
rewrite H7; clear H7.
functional induction add_component_aux (c' ->subComponents)%comp p c; auto.
SCase "Exit Branch 1/3".
inversion H1;
inversion H7; subst.
clear H7.
assert (False).
eauto.
inversion H7.
SCase "Exit Branch 2/3".
assert (False).
inversion H1; inversion H7; subst. clear H7.
assert (c'0 = s').
symmetry; eauto.
subst; eauto.
inversion H7.
SCase "Exit Branch 3/3".
clear y.
apply update_w_bindings_reduction_fact.
eauto.
Qed.
Hint Resolve updating_comps_bindings.
Lemma updating_comps_unaffect_bindings:
forall c' c p,
valid_path p (c' ->subComponents)%comp ->
well_formed_component c' ->
well_formed_component c ->
well_formed_components (add_component_aux (c' ->subComponents)%comp p c) ->
well_formed_component
((update_sub_components c' (add_component_aux (c' ->subComponents)%comp p c))).
Proof.
intros c' c p Hvp.
intros.
inversion H1.
apply WellFormedComponent; intros.
Case "1/4".
assert ((update_sub_components c' (add_component_aux (c' ->subComponents) p c)
->subComponents)%comp = (add_component_aux (c' ->subComponents)%comp p c)).
apply update_sub_comp_red.
rewrite H5 in H4. clear H5.
apply well_formed_component_individuals with
(lc:=(add_component_aux (c' ->subComponents)%comp p c)); auto.
Case "2/4".
assert ((update_sub_components c' (add_component_aux (c' ->subComponents) p c)
->subComponents)%comp = (add_component_aux (c' ->subComponents)%comp p c)).
apply update_sub_comp_red.
rewrite H4; auto.
Case "3/4". Focus.
assert ((update_sub_components c' (add_component_aux (c' ->subComponents) p c)
->interfaces)%comp = (c'->interfaces)%comp).
apply update_sub_comp_red'.
rewrite H4; eauto.
Case "4/4".
assert ((update_sub_components c' (add_component_aux (c' ->subComponents) p c)
->interfaces)%comp = (c'->interfaces)%comp).
apply update_sub_comp_red'.
rewrite H4. clear H4.
assert ((update_sub_components c' (add_component_aux (c' ->subComponents) p c)
->bindings)%comp = (c'->bindings)%comp).
apply update_sub_comp_red''.
rewrite H4. clear H4.
apply updating_comps_bindings; auto.
Qed.
Hint Resolve updating_comps_unaffect_bindings.
Lemma well_formed_adding_component:
forall lc p c ,
valid_path p lc ->
well_formed_components lc ->
well_formed_component c ->
no_id_clash' (c->id%comp) p lc ->
well_formed_components (add_component_aux lc p c ).
Proof.
intros lc p c Hvp.
intros.
functional induction add_component_aux lc p c; eauto.
assert (well_formed_components (add_component_aux (c' ->subComponents)%comp r c)).
SCase "Assertion".
inversion H.
apply IHl; simpl in *; eauto.
split; intros.
SCase "Unique Ids".
apply Unique_Step with
(c:=(update_sub_components c' (add_component_aux (c' ->subComponents)%comp r c)))
(r:=backup); eauto.
assert((update_sub_components c' (add_component_aux (c' ->subComponents) r c) ->id)%comp
= (c'->id)%comp).
apply update_sub_comp_maitains_id.
rewrite H3.
inversion H.
apply lookup_unique_ids_gen' with (lc:=comp_list) (c:=c');eauto.
assert (c'->id%comp = id).
eauto.
subst;auto.
SCase "Well Formed Component".
destruct H3; subst.
SSCase "It is the head of the list".
apply updating_comps_unaffect_bindings with (p:=r); eauto.
SSCase "It is in the tail of the list".
assert (In c0 comp_list).
eauto.
eauto.
Qed.
Hint Resolve well_formed_adding_component.
Lemma root_config_is_unaffected_by_add_comp:
forall s id p ic cl lc li lb s',
well_formed s ->
Mk_component id p ic cl lc li lb / s ~~~> Done / s' ->
(s->id%comp) = (s'->id%comp) /\
(s->path%comp) = (s'->path%comp) /\
(s->iclass%comp) = (s'->iclass%comp) /\
(s->controlLevel%comp) = (s'->controlLevel%comp) /\
(s->bindings%comp) = (s'->bindings%comp) /\
(s->interfaces%comp) = (s'->interfaces%comp).
Proof.
intros.
destruct s; simpl.
inversion H. destruct H2 as (Hp, (Hic, (Hc, (Hl, Hw)))); subst.
inversion H0; subst. clear H0.
unfold add_component in H13.
functional induction add_component_aux l p (Component id p ic cl lc li lb).
Case "Exit Branch 1/4".
inversion H13; subst; simpl. clear H13.
repeat split ;auto.
Case "Exit Branch 2/4".
congruence.
Case "Exit Branch 3/4".
congruence.
Case "Exit Branch 4/4".
inversion H13; subst; simpl.
repeat split; auto.
Qed.
Hint Resolve root_config_is_unaffected_by_add_comp.
Lemma adding_comp_unaffect_bindings:
forall p lc li lb,
well_formed_component (Component (Ident "Root") root "null" Configuration lc li lb) ->
forall lc' c,
valid_path p lc ->
lc' = add_component_aux lc p c ->
well_formed_components lc' ->
well_formed_bindings lb lc' li.
Proof.
intros; subst.
assert (add_component_aux lc p c = nil -> False) as Hfalse.
eauto.
inversion H2.
inversion H; simpl in *; subst; eauto.
unfold well_formed_bindings in H7.
intro. intro.
assert (valid_binding b lc li).
auto.
functional induction add_component_aux lc p c; eauto.
Case "Exit Branch 1/2".
assert (False).
eauto.
congruence.
Case "Exit Branch 2/2".
clear IHl.
assert (False).
eauto.
congruence.
Qed.
Hint Resolve adding_comp_unaffect_bindings.
Removing Well Formed Components
Lemma ids_unicity_kept_removing_component:
forall lc id,
unique_ids lc ->
unique_ids (remove_component_from_list id lc).
Proof.
intros.
functional induction remove_component_from_list id lc; eauto.
apply Unique_Step with (c:=e) (r:=remove_component_from_list id r); eauto.
clear IHl.
inversion H; inversion H0; subst. clear H0.
functional induction remove_component_from_list id r0; auto.
Case "1/2".
apply IHl; eauto.
inversion H1; inversion H0; auto.
inversion H. inversion H0.
inversion H0; subst. clear H0.
apply Unique_Step with (c:=c0) (r:=r); eauto.
inversion H1. inversion H0.
inversion H0; subst; auto.
Case "2/2".
apply NotInStep with
(a:=e) (r:=remove_component_from_list id r); auto.
inversion H1; inversion H0; subst; auto.
apply IHl; eauto.
inversion H1; inversion H0; auto.
inversion H. inversion H0.
inversion H0; subst. clear H0.
apply Unique_Step with (c:=c0) (r:=r); eauto.
inversion H1. inversion H0.
inversion H0; subst; auto.
Qed.
Hint Resolve ids_unicity_kept_removing_component.
Lemma not_in_preserved_by_removing_component:
forall id id' l,
not_in_l id l ->
not_in_l id (remove_component_from_list id' l).
Proof.
intros.
functional induction remove_component_from_list id' l; auto.
Case "1/2".
apply IHl0.
inversion H; inversion H0; auto.
Case "2/2".
apply NotInStep
with (a:=e) (r:=remove_component_from_list id' r); auto.
inversion H; inversion H0; subst; auto.
apply IHl0.
inversion H; inversion H0; auto.
Qed.
Hint Resolve not_in_preserved_by_removing_component.
Lemma well_formed_removing_component_from_list:
forall lc id, well_formed_components lc ->
well_formed_components (remove_component_from_list id lc).
Proof.
intros.
functional induction remove_component_from_list id lc; eauto.
assert (well_formed_components (remove_component_from_list id r)).
eauto.
split.
Case "Unique Ids".
apply Unique_Step
with (c:=e) (r:=remove_component_from_list id r); auto.
inversion H.
inversion H1; inversion H3; subst; auto.
Case "Well Formed Components".
intros.
destruct H1; subst; eauto.
inversion H.
intuition.
Qed.
Hint Resolve well_formed_removing_component_from_list.
Lemma remove_component_fact:
forall lc p id,
lc = nil ->
remove_component_aux lc p id = nil.
Proof.
intros.
functional induction remove_component_aux lc p id; auto.
inversion e0.
Qed.
Lemma unique_ids_fact':
forall c r,
unique_ids (c :: r) ->
forall c', (c'->id%comp) = (c->id%comp) ->
(~ In c' r).
Proof.
intros.
inversion H; inversion H1; subst. clear H1.
intro.
assert (((c'->id%comp) == (c0->id%comp)) = false).
apply unique_ids_fact with (r:=r0); auto.
assert (((c'->id%comp) == (c0->id%comp)) = true).
auto.
congruence.
Qed.
Lemma get_parent_step:
forall c c' id r comp_list backup,
Some c = get_parent r (c' ->subComponents)%comp ->
lookup comp_list id = Some (c', backup) ->
Some c = get_parent (id :: r) comp_list.
Proof.
intros.
simpl.
destruct r.
Case "r is nil".
simpl in H.
inversion H.
Case "r is not nil".
rewrite H0. clear H0.
auto.
Qed.
Lemma empty_components_entail_no_bindings:
forall lb lc li,
well_formed_bindings lb lc li ->
lc = nil ->
lb = nil.
Proof.
intros.
subst.
unfold well_formed_bindings in H.
induction lb; auto.
clear IHlb.
assert (valid_binding a nil li).
apply H; left; auto.
compute in H0.
destruct a; fromfalse.
Qed.
Lemma removing_from_empty_list_yields_empty_list:
forall lc p id,
lc = nil ->
remove_component_aux lc p id = nil.
Proof.
induction p; intros.
Case "Path is empty".
subst; simpl; auto.
Case "Path is not empty".
simpl.
replace (lookup lc a) with (None:option (component*list component)).
auto.
unfold lookup; subst.
simpl.
auto.
Qed.
Lemma bindings_still_valid_removing_unbinded_component:
forall b c r li,
valid_binding b (c::r) li ->
(b ~~ (c->id)%comp)%bind ->
valid_binding b r li.
Proof.
intros.
destruct c.
destruct b; simpl in *.
Case "Normal ". destruct ident_dec with (id1:=i1) (id2:=i);
destruct ident_dec with (id1:=i3) (id2:=i).
SCase "Both Ids are equal".
assert ((i1 == i) = true /\ (i3 == i) = true).
split; auto.
destruct H1; subst.
unfold no_interference in H0.
simpl in H0.
rewrite H1 in H0.
inversion H0.
SCase "Ids are Equal, Ids are not Equal".
assert ((i1 == i) = true /\ (i3 == i) = false).
split; auto.
destruct H1; subst.
unfold no_interference in H0.
simpl in H0.
rewrite H1 in H0.
inversion H0.
SCase "Ids are not Equal, Ids are Equal".
assert ((i1 == i) = false /\ (i3 == i) = true).
split; auto.
destruct H1; subst.
unfold no_interference in H0.
simpl in H0.
rewrite H2 in H0.
replace ((i1 == i) || true) with (true || (i1 == i)) in H0; intuition.
simpl in H0.
inversion H0.
SCase "Both Ids are not Equal".
assert ((i1 == i) = false /\ (i3 == i) = false).
split; auto.
destruct H1.
unfold normal_binding in *.
simpl in *.
replace ((if i == i1 then Some (Component i p i0 c l l0 l1) else r [i1]))
with (r[i1]) in H.
replace ((if i == i3 then Some (Component i p i0 c l l0 l1) else r [i3]))
with (r[i3]) in H.
exact H.
replace (i3 == i) with (i == i3) in H2; eauto.
rewrite H2; auto.
replace (i1 == i) with (i == i1) in H1; eauto.
rewrite H1; auto.
Case "Export Binding".
destruct ident_dec with (id1:=i2) (id2:=i).
SCase "Ids are Equal".
assert ((i2 == i) = true).
auto.
subst.
unfold no_interference in H0.
simpl in * |-.
rewrite H1 in H0.
inversion H0.
SCase "Ids are not Equal".
assert ((i2 == i) = false).
auto.
unfold export_binding in H.
simpl in H.
replace (i2 == i) with (i == i2) in H1; eauto.
rewrite H1 in H; auto.
Case "Import Binding".
destruct ident_dec with (id1:=i2) (id2:=i).
SCase "Ids are Equal".
assert ((i2 == i) = true).
auto.
subst.
unfold no_interference in H0.
simpl in * |-.
rewrite H1 in H0.
inversion H0.
SCase "Ids are not Equal".
assert ((i2 == i) = false).
auto.
unfold import_binding in H.
simpl in H.
replace (i2 == i) with (i == i2) in H1; eauto.
rewrite H1 in H; auto.
Qed.
Lemma remove_id_and_search_for_it_yields_none:
forall lc id,
remove_component_from_list id lc [id] = None.
Proof.
intros.
functional induction remove_component_from_list id lc; auto.
unfold get_component.
rewrite e1.
exact IHl.
Qed.
Lemma removing_components_fact:
forall lc id,
well_formed_components lc ->
forall lc', lc' = remove_component_from_list id lc ->
well_formed_components lc' ->
(forall i, i <> id ->
lc[i] = lc'[i]).
Proof.
intros. subst.
functional induction remove_component_from_list id lc; subst; auto.
Case "1/2".
unfold get_component.
replace ((e ->id)%comp == i) with false.
fold get_component.
apply IHl; eauto.
assert ((e ->id)%comp = id).
auto.
subst; symmetry; auto.
Case "2/2".
unfold get_component.
destruct ident_dec with (id1:=(e->id)%comp) (id2:=i).
SCase "Ids are Equal".
replace ((e ->id)%comp == i) with true; try symmetry; auto.
SCase "Ids are Not Equal".
replace ((e ->id)%comp == i) with false; try symmetry; auto.
fold get_component.
symmetry; apply IHl; eauto.
Qed.
Lemma removing_component_keeps_bindings_well_formed:
forall idComponent I P IC CL lc li lb,
well_formed_components lc ->
component_is_not_connected nil idComponent (Component I P IC CL lc li lb) ->
well_formed_bindings lb lc li ->
well_formed_bindings lb (remove_component_from_list idComponent lc) li.
Proof.
intros.
unfold component_is_not_connected in H0.
unfold not_binded in H0; simpl in *.
intro. intro.
assert (valid_binding b lc li); auto.
induction lc. simpl; auto.
destruct b.
Case "Normal".
destruct ident_dec with (id1:=i) (id2:=(a->id)%comp);
destruct ident_dec with (id1:=i1) (id2:=(a->id)%comp).
SCase "Both ids are equal". Focus.
subst.
simpl in *.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SSCase "Ids are Equal".
subst.
unfold no_interference in H0.
assert (match ((Normal p (a ->id)%comp i0 (a ->id)%comp i2) ->idcc)%bind with
| Some idC =>
match (Normal p (a ->id)%comp i0 (a ->id)%comp i2 ->idcs)%bind with
| Some idS =>
if (idC == (a ->id)%comp) || (idS == (a ->id)%comp) then
False
else
True
| None => if idC == (a ->id)%comp then False else True
end
| None =>
match (Normal p (a ->id)%comp i0 (a ->id)%comp i2 ->idcs)%bind with
| Some idS => if idS == (a ->id)%comp then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace ((a ->id)%comp == (a ->id)%comp) with true in H4; try symmetry; auto.
inversion H4.
SSCase "Ids are Not Equal".
replace ((a ->id)%comp == idComponent) with false; try symmetry;auto.
clear IHlc.
unfold normal_binding in *.
simpl in *.
replace ((a ->id)%comp == (a ->id)%comp) with true in *; try symmetry; auto.
SCase "Ids are equal, Ids are not Equal". Focus.
simpl in *.
unfold no_interference in H0.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SSCase "Ids are Equal".
assert (match ((Normal p i i0 i1 i2) ->idcc)%bind with
| Some idC =>
match (Normal p i i0 i1 i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p i i0 i1 i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
subst.
replace ((a ->id)%comp == (a ->id)%comp) with true in H4; try symmetry; auto.
simpl in H4.
inversion H4.
SSCase "Ids are NOT Equal".
subst.
replace ((a ->id)%comp == idComponent) with false; try symmetry; auto.
clear IHlc.
unfold normal_binding in *.
simpl in *.
replace ((a ->id)%comp == (a ->id)%comp) with true in *; try symmetry; auto.
replace ((a ->id)%comp == i1) with false in *; try symmetry; auto.
replace (remove_component_from_list idComponent lc [i1]) with (lc[i1]).
exact H3.
apply removing_components_fact with (id:=idComponent); eauto.
destruct ident_dec with (id1:=i1) (id2:=idComponent).
SSSCase "Ids are Equal".
Focus.
subst.
assert (match ((Normal p (a ->id)%comp i0 idComponent i2) ->idcc)%bind with
| Some idC =>
match (Normal p (a ->id)%comp i0 idComponent i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p (a ->id)%comp i0 idComponent i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace (idComponent == idComponent) with true in H4; try symmetry; auto.
replace (((a ->id)%comp == idComponent) || true) with (true || ((a ->id)%comp == idComponent)) in H4; intuition.
SSSCase "Ids are Not Equal".
exact n1.
SCase "Ids are not Equal, Ids are equal". Focus.
simpl in *.
unfold no_interference in H0.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SSCase "Ids are Equal".
assert (match ((Normal p i i0 i1 i2) ->idcc)%bind with
| Some idC =>
match (Normal p i i0 i1 i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p i i0 i1 i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4. subst.
replace ((a ->id)%comp == (a ->id)%comp) with true in H4; try symmetry; auto.
replace ((i == (a ->id)%comp) || true) with (true || (i == (a ->id)%comp)) in H4; intuition.
simpl in H4.
inversion H4.
SSCase "Ids are Not Equal".
subst.
replace ((a ->id)%comp == idComponent) with false; try symmetry; auto.
clear IHlc.
unfold normal_binding in *.
simpl in *.
replace ((a ->id)%comp == i) with false in *; try symmetry; auto.
replace (remove_component_from_list idComponent lc [i]) with (lc[i]).
replace (remove_component_from_list idComponent lc [(a ->id)%comp]) with (lc[(a ->id)%comp]).
exact H3.
apply removing_components_fact with (id:=idComponent); eauto.
apply removing_components_fact with (id:=idComponent); eauto.
destruct ident_dec with (id1:=i) (id2:=idComponent).
SSSCase "Ids are Equal".
subst. clear H1.
assert (match ((Normal p idComponent i0 (a ->id)%comp i2) ->idcc)%bind with
| Some idC =>
match (Normal p idComponent i0 (a ->id)%comp i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p idComponent i0 (a ->id)%comp i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H1.
replace (idComponent == idComponent ) with true in H1; try symmetry; auto.
SSSCase "Ids are Not Equal".
exact n1.
SCase "Both ids are Not equal".
Focus.
simpl in *.
unfold no_interference in H0.
unfold normal_binding in H3.
simpl in H3.
replace ((a ->id)%comp == i) with (false) in H3; try symmetry; auto.
replace ((a ->id)%comp == i1) with (false) in H3; try symmetry; auto.
clear IHlc.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SSCase "Ids are Equal".
subst.
replace ((a ->id)%comp == (a ->id)%comp) with true in *; try symmetry; auto.
unfold normal_binding.
replace (remove_component_from_list (a ->id)%comp lc [i]) with (lc[i]).
replace (remove_component_from_list (a ->id)%comp lc [i1]) with (lc[i1]).
exact H3.
apply removing_components_fact with (id:=(a->id)%comp); eauto.
apply removing_components_fact with (id:=(a->id)%comp); eauto.
SSCase "Ids are Not Equal".
replace ((a ->id)%comp == idComponent) with false; try symmetry; auto.
unfold normal_binding.
simpl.
replace ((a ->id)%comp == i) with false; try symmetry; auto.
replace (remove_component_from_list idComponent lc [i]) with (lc[i]).
replace (remove_component_from_list idComponent lc [i1]) with (lc[i1]).
replace ((a ->id)%comp == i1 ) with false; try symmetry; auto.
apply removing_components_fact with (id:=idComponent); eauto.
destruct ident_dec with (id1:=i1) (id2:=idComponent); auto.
subst.
assert (match ((Normal p i i0 idComponent i2) ->idcc)%bind with
| Some idC =>
match (Normal p i i0 idComponent i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p i i0 idComponent i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace (idComponent == idComponent) with true in H4; try symmetry; auto.
replace ((i == idComponent) || true) with true in H4; intuition.
apply removing_components_fact with (id:=idComponent); eauto.
destruct ident_dec with (id1:=i) (id2:=idComponent); auto.
subst.
assert (match ((Normal p idComponent i0 i1 i2) ->idcc)%bind with
| Some idC =>
match (Normal p idComponent i0 i1 i2 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Normal p idComponent i0 i1 i2 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace ((idComponent == idComponent)) with true in H4; try symmetry; intuition.
Case "Export Binding".
Focus.
simpl in *.
unfold no_interference in H0.
clear IHlc.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SCase "Ids are Equal".
Focus.
replace ((a ->id)%comp == idComponent) with true; try symmetry; auto.
assert (match ((Export p i i0 i1) ->idcc)%bind with
| Some idC =>
match (Export p i i0 i1 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Export p i i0 i1 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
destruct ident_dec with (id1:=i0) (id2:=idComponent).
SSCase "Ids are Equal".
replace (i0 == idComponent) with true in H4; try symmetry; auto.
fromfalse.
SSCase "Ids are not Equal".
clear H4.
unfold export_binding.
replace (remove_component_from_list idComponent lc [i0] ) with (lc[i0]);
try apply removing_components_fact with (id:=idComponent); eauto.
unfold export_binding in H3.
subst.
clear -H3 n.
unfold get_component in H3.
replace ((a ->id)%comp == i0) with false in H3; try symmetry;auto.
SCase "Ids are Not Equal".
replace ((a ->id)%comp == idComponent) with false; try symmetry; auto.
unfold export_binding in *.
destruct ident_dec with (id1:=(a ->id)%comp) (id2:=i0).
SSCase "Ids are Equal".
simpl in *.
replace ((a ->id)%comp == i0) with true in *; try symmetry;auto.
SSCase "Ids are not Equal".
simpl in *.
replace ((a ->id)%comp == i0) with false in *; try symmetry;auto.
destruct ident_dec with (id1:=idComponent) (id2:=i0).
SSSCase "IDs are Equal".
subst.
assert (match ((Export p i i0 i1) ->idcc)%bind with
| Some idC =>
match (Export p i i0 i1 ->idcs)%bind with
| Some idS =>
if (idC == i0) || (idS == i0) then
False
else
True
| None => if idC == i0 then False else True
end
| None =>
match (Export p i i0 i1 ->idcs)%bind with
| Some idS => if idS == i0 then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace (i0 == i0) with true in H4; try symmetry;auto.
inversion H4.
SSSCase "Ids are Not Equal".
replace (remove_component_from_list idComponent lc [i0]) with (lc[i0]);auto.
apply removing_components_fact with (id:=idComponent); eauto.
Case "Import Binding".
simpl in *.
unfold no_interference in H0.
clear IHlc.
destruct ident_dec with (id1:=(a->id)%comp) (id2:=idComponent).
SCase "Ids are Equal".
replace ((a ->id)%comp == idComponent) with true; try symmetry; auto.
assert (match ((Import p i i0 i1) ->idcc)%bind with
| Some idC =>
match (Import p i i0 i1 ->idcs)%bind with
| Some idS =>
if (idC == idComponent) || (idS == idComponent) then
False
else
True
| None => if idC == idComponent then False else True
end
| None =>
match (Import p i i0 i1 ->idcs)%bind with
| Some idS => if idS == idComponent then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
destruct ident_dec with (id1:=i0) (id2:=idComponent).
SSCase "Ids are Equal".
Focus.
replace (i0 == idComponent) with true in H4; try symmetry; auto.
inversion H4.
SSCase "Ids are not Equal".
clear H4.
unfold import_binding.
replace (remove_component_from_list idComponent lc [i0] ) with (lc[i0]);
try apply removing_components_fact with (id:=idComponent); eauto.
unfold import_binding in H3.
subst.
clear -H3 n.
unfold get_component in H3.
replace ((a ->id)%comp == i0) with false in H3; try symmetry;auto.
SCase "Ids are Not Equal".
replace ((a ->id)%comp == idComponent) with false; try symmetry; auto.
unfold import_binding in *.
destruct ident_dec with (id1:=(a ->id)%comp) (id2:=i0).
SSCase "Ids are Equal".
simpl in *.
replace ((a ->id)%comp == i0) with true in *; try symmetry;auto.
SSCase "Ids are not Equal".
simpl in *.
replace ((a ->id)%comp == i0) with false in *; try symmetry;auto.
destruct ident_dec with (id1:=idComponent) (id2:=i0).
SSSCase "IDs are Equal".
subst.
assert (match ((Import p i i0 i1) ->idcc)%bind with
| Some idC =>
match (Import p i i0 i1 ->idcs)%bind with
| Some idS =>
if (idC == i0) || (idS == i0) then
False
else
True
| None => if idC == i0 then False else True
end
| None =>
match (Import p i i0 i1 ->idcs)%bind with
| Some idS => if idS == i0 then False else True
| None => True
end
end).
apply H0; auto.
simpl in H4.
replace (i0 == i0) with true in H4; try symmetry;auto.
inversion H4.
SSSCase "Ids are Not Equal".
replace (remove_component_from_list idComponent lc [i0]) with (lc[i0]);auto.
apply removing_components_fact with (id:=idComponent); eauto.
Qed.
Lemma valid_path_on_non_empty_path_entails_non_empty_components:
forall e r lc,
valid_path (e :: r) lc ->
lc <> nil.
Proof.
intros.
inversion H; inversion H0; subst.
clear H0.
intuition.
subst.
inversion H2.
Qed.
Lemma removing_component_from_non_empty_path_cannot_yield_empty_components:
forall p lc id,
valid_path p lc ->
forall lc', lc' = remove_component_aux lc p id ->
lc' = nil ->
forall a r, p = a :: r ->
False.
Proof.
intros. subst.
unfold remove_component_aux in H0.
unfold lookup in H0.
assert (lookup_aux lc a nil <> None).
Focus.
clear H0.
intuition.
inversion H; inversion H1; subst.
apply lookup_congruence_fact with (lc:=lc) (id:=i) (c:=s'); auto.
destruct (lookup_aux lc a ).
Case "1/2".
destruct p.
inversion H0.
Case "2/2".
congruence.
Qed.
Lemma remove_component_nil_specification:
forall p lc id,
valid_path p lc ->
remove_component_aux lc p id = nil ->
lc = nil \/
(forall c, In c lc -> (c->id)%comp = id).
Proof.
intros.
induction p.
Case "path is nil".
simpl in H0.
functional induction remove_component_from_list id lc; auto.
SCase "1/2".
right; intros.
destruct H1; subst; auto.
destruct IHl; auto.
subst; inversion H1.
SCase "2/2".
inversion H0.
Case "Path is not nil".
assert (False).
apply removing_component_from_non_empty_path_cannot_yield_empty_components
with (p:=a::p) (lc:=lc) (id:=id) (lc':=nil)
(a:=a) (r:=p);auto.
inversion H1.
Qed.
Lemma get_component_dec:
forall id lc,
(exists c, lc[id] = Some c) \/ lc[id] = None.
Proof.
intros.
destruct (lc[id]).
left; exists c; auto.
right; auto.
Qed.
Lemma lists_with_same_elements_yield_same_component:
forall lc id c backup,
well_formed_components lc ->
forall X, lookup_aux lc id X = Some (c, backup) ->
X = nil ->
forall i, lc[i] = (c::backup)[i].
Proof.
intros.
assert (forall x, In x lc <-> In x (c::backup)).
intros.
apply lookup_mem_fact with (id:=id) (X:=X); auto.
assert (well_formed_components (c::backup)).
subst; eauto.
destruct get_component_dec with (id:=i) (lc:=lc).
Case "Exists".
destruct H4.
rewrite H4.
symmetry.
apply get_component_commutes_on_l with (l:=lc); eauto.
Case "Does Not Exist".
destruct get_component_dec with (id:=i) (lc:=c::backup).
SCase "Exists".
destruct H5.
rewrite H5.
apply get_component_commutes_on_l with (l:=c::backup); auto.
intros.
split; firstorder.
SCase "Does Not Exist".
rewrite H5.
rewrite H4; auto.
Qed.
Lemma valid_binding_on_same_element_lists:
forall b lc li c backup id,
valid_binding b lc li ->
well_formed_components lc ->
lookup lc id = Some (c, backup) ->
valid_binding b (c :: backup) li.
Proof.
intros.
assert (forall i, lc[i] = (c::backup)[i]).
intros.
apply lists_with_same_elements_yield_same_component
with (id:=id) (X:=nil); auto.
destruct b; simpl in H |- *.
Case "Normal Binding".
unfold normal_binding.
replace ((c :: backup) [i]) with (lc[i]); auto.
replace ((c :: backup) [i1]) with (lc[i1]); auto.
Case "Export Binding".
unfold export_binding.
replace ((c :: backup) [i0]) with (lc[i0]); auto.
Case "Import Binding".
unfold import_binding.
replace ((c :: backup) [i0]) with (lc[i0]); auto.
Qed.
Lemma removing_comp_unaffect_bindings:
forall p lc li lb I IC P CL,
well_formed_component (Component I P IC CL lc li lb) ->
valid_path p lc ->
forall id,
component_is_not_connected p id (Component I P IC CL lc li lb) ->
forall lc', lc' = remove_component_aux lc p id ->
well_formed_components lc' ->
well_formed_bindings lb lc' li.
Proof.
intros; subst.
inversion H; simpl in *; subst; auto.
unfold well_formed_bindings in H6.
intro. intro.
assert (valid_binding b lc li); auto.
clear H6.
functional induction remove_component_aux lc p id; eauto.
Case "1/2".
eapply removing_component_keeps_bindings_well_formed; eauto.
inversion H; auto.
Case "1/2".
inversion H0; inversion H6 ; subst.
assert (False); eauto.
fromfalse.
Qed.
Hint Resolve removing_comp_unaffect_bindings.
Lemma well_formed_update_remove_sub_comps:
forall c' r0 id backup,
well_formed_components (c' :: backup) ->
well_formed_components ((remove_component_aux (c' ->subComponents)%comp r0 id)) ->
well_formed_bindings (c'->bindings%comp) ((remove_component_aux (c' ->subComponents)%comp r0 id)) (c'->interfaces%comp) ->
well_formed_components
(update_sub_components c'
(remove_component_aux (c' ->subComponents)%comp r0 id) :: backup).
Proof.
intros.
functional induction update_sub_components c'
(remove_component_aux (c' ->subComponents)%comp r0 id).
split;auto; intros.
Case "Unique Ids".
inversion H; auto.
clear -H2.
inversion H2; inversion H; simpl in *; subst.
apply Unique_Step with (c:=Component id0 p iclass cl lc li lb) (r:=r);auto.
Case "Well Formed Component".
destruct H2; subst; eauto.
inversion H.
assert (well_formed_component (Component id0 p iclass cl lc' li lb)).
apply H3; left; auto.
apply WellFormedComponent; intros; simpl in *; eauto.
Qed.
Lemma well_formed_removing_component:
forall p id s ,
valid_path p (s->components%st) ->
component_is_not_connected p id s ->
well_formed s ->
forall lc', lc' = remove_component_aux (s->components%st) p id ->
well_formed_components lc'.
Proof.
intros.
destruct s; simpl in *.
destruct H1 as (Hi, (Hp, (Hic, (Hc, (Hl, Hw))))). subst.
inversion H.
Case "Path is nil".
subst; simpl; eauto.
Case "Path is not nil".
subst; simpl in * |-.
inversion Hw; simpl in * |-; subst; eauto.
inversion H0.
clear H0 H8 Hw H3 H2 H7.
functional induction remove_component_aux l (i::r) id; eauto.
apply well_formed_removing_component_from_list.
split; auto.
assert (well_formed_components
(remove_component_aux (c' ->subComponents)%comp r0 idComponent)).
SCase "Assertion".
apply IHl2; eauto; clear IHl2.
apply valid_path_step with (li:=comp_list) (id:=idp) (r:=backup); auto.
split; auto.
intros.
apply H9. clear H9.
eapply get_parent_step; eauto.
clear IHl2.
assert (well_formed_components (c'::backup)).
unfold lookup in e0.
assert (well_formed_components comp_list).
split; auto.
eauto.
apply well_formed_update_remove_sub_comps; auto.
destruct c'; simpl in *.
apply removing_comp_unaffect_bindings with
(p:=r0) (IC:=i1) (lc:=l)
(I:=i0) (P:=p) (CL:=c) (id:=idComponent); eauto.
SCase "Valid Path".
assert (valid_path r0 (Component i0 p i1 c l l0 l2 ->subComponents%comp)).
apply valid_path_step with (li:=comp_list) (id:=idp) (r:=backup); auto.
split; auto.
simpl in H3; auto.
SCase "".
unfold component_is_not_connected.
destruct r0; simpl.
SSCase "r0 is nil".
assert (not_binded idComponent ((Component i0 p i1 c l l0 l2)->bindings%comp)).
apply H9.
clear -e0 H2.
symmetry.
apply lookup_get_comp with (r:=backup);auto.
simpl in H3; auto.
SSCase "r0 is not nil".
rewrite e0 in H9.
apply NotConnected_Step; intuition.
inversion H3.
Qed.
Lemma root_config_is_unaffected_by_remove_comp:
forall (s : state) (id : ident) (p : path)
(s' : state),
well_formed s ->
Rm_component p id / s ~~~> Done / s' ->
(s ->id)%comp = (s' ->id)%comp /\
(s ->path)%comp = (s' ->path)%comp /\
(s ->iclass)%comp = (s' ->iclass)%comp /\
(s ->controlLevel)%comp = (s' ->controlLevel)%comp /\
(s ->bindings)%comp = (s' ->bindings)%comp /\
(s ->interfaces)%comp = (s' ->interfaces)%comp.
Proof.
intros.
destruct s; simpl.
inversion H. destruct H2 as (Hp, (Hic, (Hc, (Hl, Hw)))); subst.
inversion H0; subst. clear H0.
unfold remove_component in H6.
destruct s'; inversion H7; simpl in *; subst.
split; auto.
Qed.
Making Well Formed Interfaces!
Lemma valid_interface_path_step:
forall lc id c r backup,
unique_ids lc ->
lookup lc id = Some (c, backup) ->
valid_interface_path' (id :: r) lc ->
r <> nil ->
valid_interface_path' r (c ->subComponents)%comp.
Proof.
intros.
inversion H1.
Case "Path has just one element".
inversion H3; subst.
congruence.
Case "Path has more than one element".
inversion H3; subst. clear H3.
destruct H4.
destruct H3.
assert (x = c).
apply same_by_ids with (id:=id0) (l:=lc) (r:=backup) (X:=nil); auto.
subst; auto.
Qed.
Hint Resolve valid_interface_path_step.
Lemma valid_no_id_acc_step:
forall lc id c backup iid acc r,
lookup lc id = Some (c, backup) ->
no_id_acc_clash' iid acc (id :: r) lc ->
no_id_acc_clash' iid acc r (c ->subComponents)%comp.
Proof.
intros.
unfold no_id_acc_clash' in *; intros.
apply H0. clear H0.
unfold get_component_with_path_aux in *.
assert (lc[id] = Some c).
eauto.
unfold get_component_with_path_aux.
rewrite H0.
fold get_component_with_path_aux.
destruct r; auto. inversion H1.
rewrite H; auto.
Qed.
Hint Resolve valid_no_id_acc_step.
Lemma add_interface_may_entail_false:
forall lc p c,
well_formed_components lc ->
valid_interface_path' p lc ->
add_interface_aux lc p c = nil ->
False.
Proof.
intros.
functional induction add_interface_aux lc p c;
inversion H0; inversion H2; clear H2; subst; eauto.
destruct H3.
eauto.
destruct H3. destruct H2. eauto.
destruct H3. destruct H2. eauto.
destruct H3. destruct H2.
apply IHl; eauto.
assert (x = c').
eauto.
subst; auto.
Qed.
Hint Resolve add_interface_may_entail_false.
Lemma adding_interface_keeps_components_ids_unique:
forall c r int,
unique_ids (c :: r) ->
unique_ids (add_interface_in_component c int :: r).
Proof.
intros.
functional induction add_interface_in_component c int.
inversion H; inversion H0; subst; clear H0.
simpl in *.
apply Unique_Step with (c:=Component id p ic cl lc (int :: li) lb) (r:=r0); auto.
Qed.
Hint Resolve adding_interface_keeps_components_ids_unique.
Lemma update_sub_comps_keep_ids:
forall c r lc,
unique_ids (c :: r) ->
unique_ids (update_sub_components c lc :: r).
Proof.
intros.
functional induction update_sub_components c lc.
inversion H; inversion H0; subst; clear H0.
eapply Unique_Step; eauto.
Qed.
Hint Resolve update_sub_comps_keep_ids.
Lemma get_interface_post:
forall li i a int,
(li [i, a])%int = Some int ->
(int->id)%int = i /\ (int->visibility)%int = a.
Proof.
intros.
functional induction get_interface i a li.
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
inversion H; subst. clear H.
split; eauto.
Case "Exit Branch 3/3".
apply IHo; auto.
Qed.
Lemma get_interface_membership_fact:
forall li i a int,
(li [i, a])%int = Some int ->
In int li.
Proof.
intros.
functional induction get_interface i a li; inversion H; subst.
Case "1/2".
left; auto.
Case "2/2".
right; apply IHo; auto.
Qed.
Hint Resolve get_interface_post get_interface_membership_fact.
Lemma query_interface_entail_false:
forall li i a int int',
li[i, a]%int = Some int ->
unique_pairs (int' :: li) ->
( ((int'->id%int) == i) && ((int'->visibility%int) == a)%vis ) = true->
False.
Proof.
intros.
assert (forall i, In i li -> ((int'->id%int) == (i->id%int)) &&
((int'->visibility%int) == (i->visibility%int))%vis = false).
intros.
inversion H0. inversion H3.
apply same_nots_pair in H4.
unfold not_in_list_pairs in H4.
inversion H3; subst. clear H3.
assert (((i0->id%int) == (int0->id%int)) &&
((i0->visibility%int) == (int0->visibility%int))%vis = false).
apply H4; auto.
assert ( ((int0 ->id)%int == (i0 ->id)%int) &&
((int0 ->visibility)%int == (i0 ->visibility)%int)%vis =
((i0 ->id)%int == (int0 ->id)%int) &&
((i0 ->visibility)%int == (int0 ->visibility)%int)%vis
).
apply inner_symmetry.
rewrite H6; auto.
assert ( ((int' ->id)%int == (int ->id)%int) &&
((int' ->visibility)%int == (int ->visibility)%int)%vis = false).
apply H2. auto.
eauto.
assert (((int ->id)%int = i) /\ ((int ->visibility)%int = a)).
eauto.
destruct H4.
rewrite H4 in *; rewrite H5 in *.
congruence.
Qed.
Lemma component_query_fact:
forall lc i id ic p cl sc li lb,
lc [i] = Some (Component id p ic cl sc li lb) ->
id = i.
Proof.
intros.
functional induction get_component i lc.
Case "Exit Branch 1/3".
inversion H.
Case "Exit Branch 2/3".
destruct e; inversion H; subst.
simpl in *.
auto.
Case "Exit Branch 3/3".
apply IHo;auto.
Qed.
Hint Resolve component_query_fact.
Lemma bool_fact:
forall b, b <> true -> b = false.
Proof.
intros.
destruct b.
Case "b is true".
congruence.
Case "b is false".
refl.
Qed.
Require Import Coq.Bool.Bool.
Lemma valid_binding_interface_fact:
forall id p ic cl lc li li' lb r b int,
valid_binding b (Component id p ic cl lc li lb :: r) li' ->
unique_pairs (int :: li) ->
valid_binding b (Component id p ic cl lc (int :: li) lb :: r) li'.
Proof.
intros.
destruct b; simpl in *.
Case "Normal Binding".
functional induction normal_binding i i0 i1 i2 (Component id p ic cl lc li lb :: r) li'.
SCase "Exit Branch 1/3".
unfold normal_binding.
destruct get_component_fact' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc) (li':=int::li)
(li:=li) (lb:=lb) (r:=r) (i:=i) (x:=c1);
destruct get_component_fact' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc) (li':=(int::li))
(li:=li) (lb:=lb) (r:=r) (i:=i1) (x:=c2); auto.
SSCase "Both Not the Head of the List".
rewrite H1; rewrite H2.
rewrite e1; rewrite e2; auto.
SSCase "Not Head of the list, Head of the list".
rewrite H1; rewrite H2; rewrite e1.
assert (id = i1).
eauto.
assert ((id == i1) = true).
eauto.
unfold get_component in e0; simpl in e0.
rewrite H4 in e0.
destruct c2; inversion e0; subst. inversion e0; subst.
assert ((Component i4 p1 i5 c l (int :: l0) l1 ->interfaces)%comp = int :: l0).
eauto.
rewrite H3.
simpl in e2.
unfold get_interface.
destruct bool_dec with (b1:=((int ->id)%int == i2) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSCase "It is true".
destruct query_interface_entail_false with (li:=l0) (i:=i2) (a:=External) (int:=i') (int':=int); auto.
SSSCase "It is false".
assert ( ((int ->id)%int == i2) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H6.
fold get_interface.
rewrite e2; auto.
SSCase "Head of the list, Not Head of the list".
rewrite H1; rewrite H2.
rewrite e2.
assert (id = i).
eauto.
assert ((id == i) = true).
eauto.
unfold get_component in e; simpl in e.
rewrite H4 in e.
destruct c1; inversion e; subst.
rewrite <- e0 in H2.
assert ((Component i4 p1 i5 c l (int :: l0) l1 ->interfaces)%comp = int :: l0).
eauto.
rewrite H3.
simpl in e1.
unfold get_interface.
destruct bool_dec with (b1:=((int ->id)%int == i0) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSCase "It is true".
destruct query_interface_entail_false with (li:=l0) (i:=i0) (a:=External) (int:=i3) (int':=int); auto.
SSSCase "It is false".
assert ( ((int ->id)%int == i0) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H5.
fold get_interface.
rewrite e1; auto.
SSCase "Both Head of the list".
rewrite H2; rewrite H1.
assert (id = i).
eauto.
assert ((id == i) = true).
eauto.
assert (id = i1).
eauto.
assert ((id == i1) = true).
eauto.
unfold get_component in e; simpl in e;
rewrite H4 in e.
unfold get_component in e0; simpl in e0;
rewrite H6 in e0.
destruct c1; inversion e; subst.
clear H1.
destruct c2; inversion e0; subst.
clear H2.
assert ((Component i4 p i7 c0 l2 (int :: l3) l4 ->interfaces)%comp = int :: l3).
eauto.
rewrite H1.
subst.
subst. clear e e0.
simpl in *.
destruct bool_dec with (b1:=((int ->id)%int == i0) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSCase "It is true".
destruct query_interface_entail_false with (li:=l3) (i:=i0) (a:=External) (int:=i3) (int':=int); auto.
SSSCase "It is false".
assert ( ((int ->id)%int == i0) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H2.
rewrite e1; auto.
destruct bool_dec with (b1:=((int ->id)%int == i2) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSSCase "It is true".
destruct query_interface_entail_false with (li:=l3) (i:=i2) (a:=External) (int:=i') (int':=int); auto.
SSSSCase "It is false".
assert ( ((int ->id)%int == i2) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H3.
rewrite e2; auto.
SCase "Exit Branch 2/3".
inversion H.
SCase "Exit Branch 3/3".
inversion H.
Case "Export Binding".
functional induction export_binding i i0 i1 (Component id p ic cl lc li lb :: r) li'.
SCase "Exit Branch 1/3".
inversion H.
SCase "Exit Branch 2/3".
unfold export_binding.
destruct get_component_fact' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc) (li':=int::li)
(li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'); auto.
SSCase "Not the Head of the List".
rewrite H1; rewrite e1; rewrite e0; auto.
SSCase "Head of the list".
rewrite H1; rewrite e0.
assert (id = i0).
eauto.
assert ((id == i0) = true).
eauto.
unfold get_component in e; simpl in e;
rewrite H3 in e.
destruct c'; inversion e; subst.
clear H1.
inversion e; subst. clear e H2.
assert ((Component i3 p1 i4 c l (int :: l0) l1 ->interfaces)%comp = int :: l0).
eauto.
rewrite H1.
simpl in e1.
unfold get_interface.
destruct bool_dec with (b1:=((int ->id)%int == i1) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSCase "It is true".
destruct query_interface_entail_false with (li:=l0) (i:=i1) (a:=External) (int:=i') (int':=int); auto.
SSSCase "It is false".
assert ( ((int ->id)%int == i1) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H2.
fold get_interface.
rewrite e1; auto.
SCase "Exit Branch 3/3".
inversion H.
Case "Import Binding".
functional induction import_binding i i0 i1 (Component id p ic cl lc li lb :: r) li'.
SCase "Exit Branch 1/3".
inversion H.
SCase "Exit Branch 2/3".
unfold import_binding.
destruct get_component_fact' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc) (li':=int::li)
(li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'); auto.
SSCase "Not the Head of the List".
rewrite H1; rewrite e1; rewrite e0; auto.
SSCase "Head of the list".
rewrite H1; rewrite e0.
assert (id = i0).
eauto.
assert ((id == i0) = true).
eauto.
unfold get_component in e; simpl in e;
rewrite H3 in e.
destruct c'; inversion e; subst.
clear H1.
inversion e; subst. clear e H2.
assert ((Component i3 p1 i4 c l (int :: l0) l1 ->interfaces)%comp = int :: l0).
eauto.
rewrite H1.
simpl in e1.
unfold get_interface.
destruct bool_dec with (b1:=((int ->id)%int == i1) && ((int ->visibility)%int == External)%vis)
(b2:=true).
SSSCase "It is true".
destruct query_interface_entail_false with (li:=l0) (i:=i1) (a:=External) (int:=i') (int':=int); auto.
SSSCase "It is false".
assert ( ((int ->id)%int == i1) && ((int ->visibility)%int == External)%vis = false).
apply bool_fact; auto.
rewrite H2.
fold get_interface.
rewrite e1; auto.
SCase "Exit Branch 3/3".
inversion H.
Qed.
Hint Resolve valid_binding_interface_fact.
Lemma update_w_bindings_reduction_fact'':
forall lb c backup li int,
well_formed_bindings lb (c :: backup) li ->
well_formed_component (add_interface_in_component c int) ->
well_formed_bindings
lb
(add_interface_in_component c int :: backup)
li.
Proof.
intros.
functional induction add_interface_in_component c int.
intro. intro.
unfold well_formed_bindings in H.
assert (valid_binding b (Component id p ic cl lc li0 lb0 :: backup) li).
apply H;auto.
apply valid_binding_interface_fact; auto.
inversion H0; simpl in *; subst; auto.
inversion H5; auto; inversion H7.
Qed.
Hint Resolve update_w_bindings_reduction_fact''.
Lemma adding_interface_keeps_bindings_well_formed:
forall lb c r li int,
well_formed_bindings lb (c :: r) li ->
well_formed_component (add_interface_in_component c int) ->
well_formed_bindings lb (add_interface_in_component c int :: r) li.
Proof.
intros; apply update_w_bindings_reduction_fact'';auto.
Qed.
Hint Resolve adding_interface_keeps_bindings_well_formed.
Lemma well_formed_bindings_w_lookup:
forall lc id c r li lb,
lookup lc id = Some (c, r) ->
well_formed_interfaces li ->
well_formed_bindings lb lc li ->
well_formed_components lc ->
well_formed_bindings lb (c :: r) li.
Proof.
intros lc id c r li lb H H0 H1 Hw.
assert (forall e, In e lc <-> In e (c :: r)).
eauto.
intro; intro.
unfold well_formed_bindings in H1.
Case "Bindings are not Nil".
assert (valid_binding b lc li).
apply H1;auto.
destruct b; simpl in *.
SCase "Normal Binding".
functional induction normal_binding i i0 i1 i2 lc li.
SSCase "Exit Branch 1/3".
unfold normal_binding.
assert ((c::r)[i] = Some c1).
apply lookup_get_fact' with (id:=id) (lc := lc);auto.
assert ((c::r)[i1] = Some c2).
apply lookup_get_fact' with (id:=id) (lc := lc);auto.
rewrite H6; rewrite H5.
rewrite e1; rewrite e2; auto.
SSCase "Exit Branch 2/3".
fromfalse.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Export Binding".
functional induction export_binding i i0 i1 lc li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
unfold export_binding.
assert ((c::r)[i0] = Some c').
apply lookup_get_fact' with (id:=id) (lc := lc);auto.
inversion Hw;auto.
rewrite H5;
rewrite e1; rewrite e0; auto.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Import Binding".
functional induction import_binding i i0 i1 lc li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
unfold import_binding.
assert ((c::r)[i0] = Some c').
apply lookup_get_fact' with (id:=id) (lc := lc);auto.
inversion Hw; auto.
rewrite H5;
rewrite e1; rewrite e0; auto.
SSCase "Exit Branch 3/3".
fromfalse.
Qed.
Hint Resolve well_formed_bindings_w_lookup.
Lemma adding_interface_unaffect_bindings:
forall p lc li lb I IC P CL,
well_formed_component (Component I P IC CL lc li lb) ->
forall lc' c,
valid_interface_path' p lc ->
lc' = add_interface_aux lc p c ->
well_formed_components lc' ->
well_formed_bindings lb lc' li.
Proof.
intros.
assert (add_interface_aux lc p c = nil -> False) as Hfalse.
eauto.
functional induction add_interface_aux lc p c; subst; auto.
Case "1/6".
inversion H0; inversion H1.
Case "2/6".
inversion H0; inversion H1; subst; clear H1.
assert (False).
eauto.
inversion H1.
assert (False).
eauto.
inversion H1.
Case "3/6".
inversion H; simpl in *; subst; auto.
apply adding_interface_keeps_bindings_well_formed.
apply well_formed_bindings_w_lookup with (lc:=comp_list) (id:=c_id); auto.
assert (well_formed_components ((Component I P IC CL comp_list li lb)->subComponents%comp)).
apply well_formed_inheritance; auto.
simpl in H6; auto.
apply well_formed_component_individuals with (lc:=(add_interface_in_component c int :: r)); auto.
left;auto.
Case "4/6".
inversion H0; inversion H1; subst; clear H1.
inversion y.
assert (False).
eauto.
inversion H1.
Case "5/6".
assert (False).
apply Hfalse; auto.
inversion H1.
Case "6/6".
clear IHl y y0 Hfalse.
inversion H; simpl in *; subst.
inversion e0.
eauto.
Qed.
Hint Resolve adding_interface_unaffect_bindings.
Lemma well_formed_interface_append:
forall lc c p int,
valid_path p lc ->
well_formed_components lc ->
Some c = get_component_with_path_aux p lc ->
forall li, (c->interfaces)%comp = li ->
no_id_acc_clash' (int->id%int) (int->visibility%int) p lc ->
well_formed_interfaces (int :: li).
Proof.
intros.
inversion H0.
apply WellFormedInterfaces_Step with (i:=int) (r:=li); auto.
Case "Unique Pairs".
apply UniquePairs_Step with (int:=int) (r:=li); auto.
SCase "Head is not in the tail".
destruct c; simpl in *; subst.
unfold no_id_acc_clash' in H3.
destruct H3 with (c:=(Component i p0 i0 c l li l1) ); auto.
simpl in *; subst.
apply NotInPair_Nil; auto.
simpl in *; subst.
apply NotInPairStep with (int:=int0) (r:=r); auto.
SCase "Tail have unique ids".
assert (well_formed_component c).
apply transitive_inheritance' with (lc:=lc) (p:=p); auto.
destruct c; simpl in *; subst; auto.
inversion H6; simpl in *; subst; auto.
inversion H8; subst; eauto.
apply UniquePairs_Base; auto.
Case "Well Formed Interfaces".
assert (well_formed_component c).
apply transitive_inheritance' with (lc:=lc) (p:=p); auto.
destruct c.
simpl in H2; subst.
inversion H6;auto.
Qed.
Hint Resolve well_formed_interface_append.
Lemma get_interface_fact:
forall li id a int,
(li [id, a])%int = Some int ->
In int li.
Proof.
intros.
functional induction get_interface id a li.
Case "1/3".
inversion H.
Case "2/3".
inversion H; subst; clear H.
left;auto.
Case "3/3".
right.
apply IHo;auto.
Qed.
Hint Resolve get_interface_fact.
Lemma get_interface_fact_id:
forall li id a int,
(li [id, a])%int = Some int ->
(int ->id)%int = id.
Proof.
intros.
functional induction get_interface id a li; inversion H;
subst; clear H; eauto.
Qed.
Hint Resolve get_interface_fact_id.
Lemma bool_conjunction_acc:
forall a a' X,
X && (a == a')%vis = true ->
(a == a')%vis = true.
Proof.
intros.
assert (X && (a == a')%vis = (a == a')%vis && X).
intuition.
rewrite H0 in H.
functional induction beq_visibility a a'; auto.
Qed.
Hint Resolve bool_conjunction_acc.
Lemma beq_acc_fact:
forall a a',
(a == a')%vis = true ->
a = a'.
Proof.
intros.
functional induction beq_visibility a a'; auto.
inversion H.
Qed.
Hint Resolve beq_acc_fact.
Lemma get_interface_fact_acc:
forall li id a int,
(li [id, a])%int = Some int ->
(int ->visibility)%int = a.
Proof.
intros.
functional induction get_interface id a li; inversion H;
subst; clear H; auto.
assert (((int ->visibility)%int == a)%vis = true).
eauto.
eauto.
Qed.
Hint Resolve get_interface_fact_acc.
Lemma bool_symmetry_fact:
forall id id' a a',
((id == id') &&
(a == a')%vis
=
( id' == id) &&
(a' == a)%vis).
Proof.
intros.
assert ((id == id') = (id' == id)).
unfold beq_ident.
assert (forall str1 str2, (if string_dec str1 str2 then true else false) =
(if string_dec str2 str1 then true else false)).
intros.
apply str_symmetry.
destruct id.
destruct id'.
apply H.
rewrite H.
assert ((a == a')%vis = (a' == a)%vis).
functional induction beq_visibility a a'; try refl.
destruct v1.
destruct v2.
inversion y.
refl.
destruct v2.
refl.
inversion y.
rewrite H0; refl.
Qed.
Hint Resolve bool_symmetry_fact.
Lemma query_is_equal_for_well_formed_interfaces:
forall int li i X i2,
well_formed_interfaces (int :: li) ->
li[i, X]%int = Some i2 ->
((int :: li) [i, X])%int = Some i2.
Proof.
intros.
inversion H;
inversion H1; subst; clear H1.
assert (((i0 ->id)%int == i) && ((i0 ->visibility)%int == X)%vis= false).
inversion H2;
inversion H1; subst. clear H1.
assert (In i2 r0).
eauto.
assert (i2->id%int = i).
eauto.
assert (i2->visibility%int = X).
eauto.
subst.
apply same_nots_pair in H4.
unfold not_in_list_pairs in H4.
assert (((i2 ->id)%int == (int ->id)%int) &&
((i2 ->visibility)%int == (int ->visibility)%int)%vis
=
( (int ->id)%int == (i2 ->id)%int) &&
((int ->visibility)%int == (i2 ->visibility)%int)%vis).
auto.
rewrite <- H6.
apply H4;auto.
unfold get_interface.
rewrite H1; auto.
Qed.
Hint Resolve query_is_equal_for_well_formed_interfaces.
Lemma appending_interface_keeps_bindings_well_formed:
forall lb lc li int,
well_formed_interfaces (int :: li) ->
well_formed_bindings lb lc li ->
well_formed_bindings lb lc (int :: li).
Proof.
intros lb lc li int Hw.
intros.
unfold well_formed_bindings in H.
intro; intro.
assert (valid_binding b lc li).
auto.
destruct b; simpl in *.
SCase "Normal Binding".
eauto.
SCase "Export Binding". Focus.
functional induction export_binding i i0 i1 lc li.
SSCase "1/3".
fromfalse.
SSCase "2/3".
unfold export_binding.
rewrite e; rewrite e1; clear e e1.
assert ( ((int :: li) [i, Internal])%int = Some i2).
apply query_is_equal_for_well_formed_interfaces;auto.
rewrite H2;auto.
SSCase "3/3".
fromfalse.
SCase "Import Binding".
functional induction import_binding i i0 i1 lc li; try fromfalse.
unfold import_binding.
rewrite e; rewrite e1; clear e e1.
assert (((int :: li) [i, Internal])%int = Some i2).
apply query_is_equal_for_well_formed_interfaces;auto.
rewrite H2;auto.
Qed.
Hint Resolve appending_interface_keeps_bindings_well_formed.
Lemma well_formed_adding_component_interface:
forall lc id c r int,
well_formed_components lc ->
lookup lc id = Some (c, r) ->
no_id_acc_clash' (int->id)%int (int->visibility)%int (id::nil) lc ->
well_formed_components (add_interface_in_component c int :: r).
Proof.
intros.
assert (forall x, In x lc <-> In x (c :: r)).
intros; eauto.
assert (well_formed_components (c::r)).
eauto.
functional induction add_interface_in_component c int.
split.
Case "Unique Ids".
inversion H3.
inversion H4; inversion H6; subst; clear H6.
apply Unique_Step with (c:=Component id0 p ic cl lc0 (int :: li) lb ) (r:=r0);auto.
Case "Well formed Components".
intros.
destruct H4;subst;eauto.
assert (In (Component id0 p ic cl lc0 li lb) lc).
eauto.
assert (well_formed_component (Component id0 p ic cl lc0 li lb)).
eauto.
assert (well_formed_components lc0).
inversion H5; simpl in *; subst; eauto.
apply WellFormedComponent; intros; simpl in *.
SCase "1/4".
eauto.
SCase "2/4".
inversion H6;auto.
SCase "3/4". Focus.
apply well_formed_interface_append with
(lc:=lc) (c:=(Component id0 p ic cl lc0 li lb)) (p:=(id :: nil)); auto.
apply ValidN with (i:=id) (r:=nil) (s':=Component id0 p ic cl lc0 li lb); eauto.
unfold get_component_with_path_aux.
symmetry.
apply lookup_get_comp with (r:=r); auto.
inversion H; auto.
SCase "1/4".
apply appending_interface_keeps_bindings_well_formed.
SSCase "Well formed Interfaces Append".
destruct stronger_inheritance with (c:=Component id0 p ic cl lc0 li lb); auto.
destruct H10; simpl in *.
apply well_formed_interface_append with
(lc:=lc) (c:=Component id0 p ic cl lc0 li lb) (p:=((id :: nil))); auto.
apply ValidN with (i:=id) (r:=nil) (s':=Component id0 p ic cl lc0 li lb); eauto.
unfold get_component_with_path_aux.
symmetry.
apply lookup_get_comp with (r:=r);auto.
inversion H;auto.
SSCase "Well formed Bindings".
inversion H3.
inversion H5; simpl in *; subst; auto.
Qed.
Hint Resolve well_formed_adding_component_interface.
Lemma well_formed_update_w_add_interface:
forall c' p int,
valid_interface_path p c' ->
well_formed_component c' ->
well_formed_components ((add_interface_aux (c'->subComponents)%comp p int)) ->
well_formed_component (update_sub_components c' ((add_interface_aux (c'->subComponents)%comp p int))).
Proof.
intros.
destruct c'; simpl in *.
assert (well_formed_bindings l1 ((add_interface_aux l p int)) l0).
apply adding_interface_unaffect_bindings with
(p:=p) (IC:=i0) (lc:=l) (li:=l0) (lb:=l1) (I:=i) (P:=p0)
(CL:=c) (lc':=(add_interface_aux l p int)) (c:=int);auto.
apply WellFormedComponent; intros; simpl in *.
Case "1/4".
eauto.
Case "2/4".
inversion H1;auto.
Case "3/4".
inversion H0;auto.
Case "4/4".
auto.
Qed.
Hint Resolve well_formed_update_w_add_interface.
Lemma well_formed_adding_interface:
forall lc p int ,
valid_interface_path' p lc ->
well_formed_components lc ->
no_id_acc_clash' (int->id)%int (int->visibility)%int p lc ->
well_formed_components (add_interface_aux lc p int ).
Proof.
intros.
inversion H; subst.
Case "Interface Path has just one element".
clear H3. functional induction add_interface_aux lc (id :: nil) int; eauto.
assert ( well_formed_components
(add_interface_aux (c' ->subComponents)%comp r int)).
Focus.
apply IHl0; eauto.
apply valid_interface_path_step with (lc:=comp_list) (id:=id0) (backup:=backup).
inversion H0; auto.
exact e0.
exact H.
destruct r; auto.
intuition.
inversion H2.
assert (well_formed_components (c' :: backup)).
eauto.
assert (well_formed_component (update_sub_components c' (add_interface_aux (c' ->subComponents)%comp r int))).
apply well_formed_update_w_add_interface; auto.
apply valid_interface_path_step with (lc:=comp_list) (id:=id0) (backup:=backup); auto.
inversion H0; auto.
destruct r; auto.
intuition. inversion H6.
eauto. split; eauto.
intros.
destruct H5; subst; eauto.
Case "Interface has more than one element".
clear H3. functional induction add_interface_aux lc (id :: r) int; auto.
SCase "1/2".
eauto.
SCase "2/2".
assert ( well_formed_components
(add_interface_aux (c' ->subComponents)%comp r0 int)).
Focus.
apply IHl0; eauto.
apply valid_interface_path_step with (lc:=comp_list) (id:=id0) (backup:=backup).
inversion H0; auto.
exact e0.
exact H.
destruct r0; auto.
intuition.
inversion H2.
assert (well_formed_components (c' :: backup)).
eauto.
assert (well_formed_component (update_sub_components c' (add_interface_aux (c' ->subComponents)%comp r0 int))).
apply well_formed_update_w_add_interface; auto.
apply valid_interface_path_step with (lc:=comp_list) (id:=id0) (backup:=backup); auto.
inversion H0; auto.
destruct r0; auto.
intuition. congruence.
apply well_formed_component_individuals with (lc:=c':: backup); auto.
left;auto.
split; eauto.
intros.
destruct H5; subst; eauto.
Qed.
Lemma root_config_is_unaffected_by_add_interface:
forall s id t p acc co f ct cd s',
well_formed s ->
Mk_interface id t p acc co f ct cd / s ~~~> Done / s' ->
(s->id%comp) = (s'->id%comp) /\
(s->path%comp) = (s'->path%comp) /\
(s->iclass%comp) = (s'->iclass%comp) /\
(s->controlLevel%comp) = (s'->controlLevel%comp) /\
(s->bindings%comp) = (s'->bindings%comp) /\
(s->interfaces%comp) = (s'->interfaces%comp).
Proof.
intros.
destruct s; simpl.
inversion H. destruct H2 as (Hp, (Hic, (Hc, (Hl, Hw)))); subst.
inversion H0; subst. clear H0.
unfold add_interface in H13.
functional induction add_interface_aux l p (Interface id t p acc co f ct cd);
try thus inversion H13; intuition.
Qed.
Making Well Formed Bindings!
Lemma appending_binding_keeps_component_well_formed:
forall id p ic cl lc li lb b,
well_formed_component (Component id p ic cl lc li lb) ->
valid_binding b lc li ->
well_formed_component (Component id p ic cl lc li (b :: lb)).
Proof.
intros.
apply WellFormedComponent; intros; simpl in *.
Case "Well Formed SubComponents".
eauto.
Case "Unique Ids in SubComponents".
assert ((Component id p ic cl lc li lb)->subComponents%comp = lc).
auto.
rewrite <- H1.
eauto.
Case "Well Formed Interfaces".
assert ((Component id p ic cl lc li lb)->interfaces%comp = li).
auto.
rewrite <- H1.
eauto.
Case "Well Formed Bindings".
intro; intro.
destruct H1; subst; auto.
assert (well_formed_bindings lb lc li).
destruct stronger_inheritance with (c:=(Component id p ic cl lc li lb)); auto.
destruct H3;auto.
unfold well_formed_bindings in H2.
apply H2; auto.
Qed.
Hint Resolve appending_binding_keeps_component_well_formed.
Lemma adding_interface_maintains_component_id:
forall c b,
(add_binding_in_component c b)->id%comp = (c->id)%comp.
Proof.
intros.
functional induction add_binding_in_component c b; refl.
Qed.
Hint Resolve adding_interface_maintains_component_id.
Lemma unique_ids_is_preserved_by_adding_comp:
forall c r b,
unique_ids (c :: r) ->
unique_ids (add_binding_in_component c b :: r).
Proof.
intros.
assert ((add_binding_in_component c b ->id)%comp = (c->id)%comp).
auto.
apply Unique_Step with (c:=add_binding_in_component c b) (r:=r); auto.
rewrite H0.
inversion H;
inversion H1; subst; auto.
eauto.
Qed.
Hint Resolve unique_ids_is_preserved_by_adding_comp.
Lemma add_binding_fact:
forall lc b,
add_binding_aux lc nil b = nil.
Proof.
intros; refl.
Qed.
Hint Resolve add_binding_fact.
Lemma add_binding_fact_nil_comps:
forall p b lc,
lc = nil ->
add_binding_aux lc p b = nil.
Proof.
intros.
functional induction add_binding_aux lc p b;
try congruence; auto.
inversion e0.
inversion e0.
Qed.
Hint Resolve add_binding_fact_nil_comps.
Lemma lookup_comp_fact:
forall c lc id p ic cl lc0 li lb r,
Some c = lc [id] ->
well_formed_components (Component id p ic cl lc0 li lb :: r) ->
lookup lc id = Some (Component id p ic cl lc0 li lb, r) ->
c = Component id p ic cl lc0 li lb.
Proof.
intros.
inversion H0.
clear H3 H0.
unfold lookup in H1.
functional induction lookup_aux lc id (nil:list component).
Case "Exit 1/3".
inversion H.
Case "Exit 2/3".
inversion H1; subst. clear H1.
simpl in e0.
unfold get_component in H.
simpl in H.
rewrite e0 in H.
inversion H; auto.
Case "Exit 3/3".
apply IHo;auto.
unfold get_component in H.
rewrite e0 in H;
auto.
Qed.
Hint Resolve lookup_comp_fact.
Lemma lookup_none_comp_fact:
forall lc id r X,
lookup_aux lc id X = None ->
X = nil ->
None = get_component_with_path_aux (id :: r) lc.
Proof.
intros.
functional induction lookup_aux lc id X.
Case "Exit Branch 1/3".
unfold get_component_with_path_aux.
destruct r.
refl.
unfold lookup.
refl.
Case "Exit Branch 2/3".
inversion H.
Case "Exit Branch 3/3".
unfold get_component_with_path_aux.
destruct r.
unfold get_component.
rewrite e0.
fold get_component.
functional induction lookup_aux r0 id (c :: nil); try refl.
inversion H.
unfold get_component; rewrite e1.
fold get_component.
apply IHo0; auto.
intros.
inversion H1.
unfold lookup;
unfold lookup_aux;
rewrite e0.
fold lookup_aux.
rewrite H.
auto.
Qed.
Hint Resolve lookup_none_comp_fact.
Lemma lookup_get_fact_gen'2:
forall lc id i c c' r X,
unique_ids lc ->
lookup_aux lc id X = Some (c, r) ->
X = nil ->
lc[i] = Some c' ->
(c::r)[i] = Some c'.
Proof.
intros.
apply get_component_commutes_on_l with (l:=lc); eauto.
apply lookup_unique_ids_gen2 with (lc:=lc) (id:=id) (X:=X); subst; auto.
rewrite app_nil_r; auto.
Qed.
Lemma lookup_query_fact:
forall lc id' c backup id c1,
unique_ids lc ->
lookup lc id' = Some (c, backup) ->
lc [id] = Some c1 ->
(c :: backup) [id] = Some c1.
Proof.
intros.
unfold lookup in H0.
apply lookup_get_fact_gen'2 with (lc:=lc) (id:=id') (X:=nil); auto.
Qed.
Hint Resolve lookup_query_fact.
Lemma prime_list_lookup:
forall some_lc some_id id p ic cl lc' li lb backup i0 c1 lc,
unique_ids some_lc ->
lookup some_lc some_id = Some (Component id p ic cl lc' li lb, backup) ->
some_lc [i0] = Some c1 ->
((Component id p ic cl lc li lb :: backup) [i0] = Some c1 \/
(Component id p ic cl lc li lb :: backup) [i0] = Some (Component id p ic cl lc li lb)).
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=i0).
Case "Ids are Equal".
right.
unfold get_component; simpl.
assert ((id == i0) = true).
eauto.
rewrite H2; reflexivity.
Case "Ids are not Equal".
left.
unfold get_component; simpl.
assert ((id == i0) = false).
eauto.
rewrite H2.
fold get_component.
assert (((Component id p ic cl lc' li lb) :: backup)[i0] = Some c1).
apply lookup_query_fact with (lc:=some_lc) (id':=some_id);auto.
unfold get_component in H3; simpl in H3; rewrite H2 in H3; auto.
Qed.
Lemma interfaces_are_the_same:
forall some_lc some_id id p ic cl lc' li lb backup i0 c1 lc,
unique_ids some_lc ->
lookup some_lc some_id = Some (Component id p ic cl lc' li lb, backup) ->
some_lc [i0] = Some c1 ->
forall x,
(Component id p ic cl lc li lb :: backup) [i0] = Some x ->
(x->interfaces%comp) = (c1->interfaces%comp).
Proof.
intros.
destruct prime_list_lookup with
(some_lc:=some_lc) (some_id:=some_id) (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc':=lc')
(li:=li) (lb:=lb) (backup:=backup) (i0:=i0) (c1:=c1) (lc:=lc); auto.
rewrite H2 in H3.
destruct x; destruct c1.
inversion H3; subst; auto.
rewrite H2 in H3.
destruct x; inversion H3; subst.
simpl. clear H3.
assert (c1->id%comp = i0).
eauto.
assert ((Component id p ic cl lc li lb->id%comp = i0)).
eauto.
simpl in H4.
assert ((Component id p ic cl lc' li lb->id%comp) = some_id).
eauto.
simpl in H5.
assert (some_lc [some_id] = Some (Component id p ic cl lc' li lb)).
eauto.
rewrite H4 in H5.
rewrite <- H5 in H6.
rewrite H1 in H6.
inversion H6.
simpl; auto.
Qed.
Lemma get_component_fact'':
forall id p ic cl lc lb' li lb r i,
forall x,
(Component id p ic cl lc li lb :: r) [i] = Some x ->
(Component id p ic cl lc li lb' :: r) [i] = Some x \/
(Component id p ic cl lc li lb' :: r) [i] = (Some (Component id p ic cl lc li lb')).
Proof.
intros.
destruct ident_dec with (id1:=id) (id2:=i).
Case "Ids are Equal".
assert ((id == i) = true).
eauto.
right.
simpl; rewrite H0; auto.
Case "Ids are not Equal".
left.
assert ((id == i) = false).
eauto.
simpl in *; rewrite H0 in *; auto.
Qed.
Hint Resolve get_component_fact''.
Lemma get_component_fact_same_interfaces':
forall id p ic cl lc lb' li lb r i,
forall x y,
(Component id p ic cl lc li lb :: r) [i] = Some x ->
(Component id p ic cl lc li lb' :: r) [i] = Some y ->
(x->interfaces)%comp = (y->interfaces)%comp.
Proof.
intros.
destruct get_component_fact'' with (id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc)
(lb':=lb') (li:=li) (lb:=lb) (r:=r) (i:=i) (x:=x); auto.
Case "Head of the list".
assert (x = y).
rewrite H1 in H0.
inversion H0;auto.
destruct x; destruct y; simpl.
inversion H2;auto.
Case "Not the Head of the List".
rewrite H1 in H0.
destruct ident_dec with (id1:=id) (id2:=i).
SCase "Ids are equal".
assert ((id == i) = true).
eauto.
unfold get_component in H.
simpl in H.
rewrite H2 in H.
destruct x.
inversion H; subst.
simpl.
destruct y; simpl; subst.
inversion H0; auto.
SCase "Ids are not equal".
assert ((id == i) = false).
eauto.
unfold get_component in H; simpl in H.
rewrite H2 in H.
fold get_component in H.
unfold get_component in H1; simpl in H1.
rewrite H2 in H1.
fold get_component in H1.
clear n H2.
assert (x = Component id p ic cl lc li lb').
rewrite H in H1.
inversion H1; auto.
destruct x; inversion H2; subst.
destruct y; simpl.
inversion H0; auto.
Qed.
Hint Resolve get_component_fact_same_interfaces'.
Lemma valid_adding_binding_fact:
forall b0 c' i r b,
unique_ids (c' ->subComponents)%comp ->
In b0 (c' ->bindings)%comp ->
(add_binding_aux (c' ->subComponents)%comp (i :: r) b) <> nil ->
valid_binding b0 (c' ->subComponents)%comp (c' ->interfaces)%comp ->
valid_binding b0 (add_binding_aux (c' ->subComponents)%comp (i :: r) b) (c' ->interfaces)%comp.
Proof.
intros b0 c' i r b Hunique.
intros.
functional induction (add_binding_aux (c' ->subComponents)%comp (i :: r) b); try congruence.
Case "Exit Branch 1/2".
destruct b0.
SCase "Normal Binding".
functional induction add_binding_in_component c b.
simpl in *.
functional induction (normal_binding i0 i1 i2 i3 lc (c' ->interfaces)%comp);
try inversion H1.
unfold normal_binding in *.
destruct get_component_fact'' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0)
(lb':=b::lb) (li:=li) (lb:=lb) (r:=r0) (i:=i0) (x:=c1);
destruct get_component_fact'' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0)
(lb':=b::lb) (li:=li) (lb:=lb) (r:=r0) (i:=i2) (x:=c2);
eauto.
SSCase "Both head of the list".
rewrite H4; rewrite H5.
rewrite e3; rewrite e2; auto.
SSCase "Head of the list, in the tail".
rewrite H4; rewrite H5.
rewrite e2.
assert ( (c2->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=b::lb) (li:=li)
(lb:=lb) (r:=r0) (i:=i2); eauto.
rewrite H6 in e3.
rewrite e3; auto.
SSCase "In the tail of the list, the head of the list".
rewrite H4; rewrite H5.
rewrite e3.
assert ( (c1->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=b::lb) (li:=li)
(lb:=lb) (r:=r0) (i:=i0); eauto.
rewrite H6 in e2.
rewrite e2; auto.
SSCase "Both in the tail".
assert ( (c2->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=b::lb) (li:=li)
(lb:=lb) (r:=r0) (i:=i2); eauto.
assert ( (c1->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=b::lb) (li:=li)
(lb:=lb) (r:=r0) (i:=i0); eauto.
rewrite H6 in e3.
rewrite H7 in e2.
rewrite H4; rewrite H5.
rewrite e3; rewrite e2; auto.
SCase "Export Binding".
functional induction add_binding_in_component c b.
simpl in *.
unfold export_binding. Focus.
functional induction export_binding i0 i1 i2 lc (c' ->interfaces)%comp.
SSCase "Exit Branch 1/3".
inversion H1.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb)
(li:=li) (lb:=lb) (r:=r0) (i:=i1) (x:=c'0); eauto.
SSSCase "Head".
rewrite H2;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H2; rewrite e1.
assert ( (c'0->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
eauto.
rewrite <- H3.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
inversion H1.
SCase "Import Binding".
functional induction add_binding_in_component c b.
simpl in *.
unfold import_binding.
functional induction import_binding i0 i1 i2 lc (c' ->interfaces)%comp.
SSCase "Exit Branch 1/3".
inversion H1.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb)
(li:=li) (lb:=lb) (r:=r0) (i:=i1) (x:=c'0); eauto.
SSSCase "Head".
rewrite H2;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H2; rewrite e1.
assert ( (c'0->interfaces%comp) = (Component id p0 ic cl lc0 li (b :: lb) ->interfaces)%comp).
eauto.
rewrite <- H3.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
inversion H1.
Case "Exit Branch 2/2".
clear H0.
destruct b0.
SCase "Normal Binding".
functional induction
(update_sub_components c'0 (add_binding_aux (c'0 ->subComponents)%comp r0 b)).
clear IHl1 y0.
simpl in *.
functional induction (normal_binding i0 i1 i2 i3 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0)
(c1:=c1) (lc:=lc0);
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i2)
(c1:=c2) (lc:=lc0); auto.
unfold normal_binding.
rewrite H4; rewrite H3; rewrite e2; rewrite e3; auto.
unfold normal_binding.
rewrite H3; rewrite H4.
simpl. rewrite e2.
assert ((c2 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (cl:=cl) (ic:=iclass)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i2) (lc:=lc0); auto .
simpl in H5; subst.
rewrite e3;auto.
unfold normal_binding.
rewrite H4; rewrite H3; simpl; rewrite e3.
assert ((c1 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0) (lc:=lc0); auto .
simpl in H5; subst.
rewrite e2;auto.
unfold normal_binding.
rewrite H4; rewrite H3. simpl.
assert ((c1 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0) (lc:=lc0); auto .
simpl in H5.
assert ((c2 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i2) (lc:=lc0); auto .
simpl in H6.
rewrite H5 in e2.
rewrite H6 in e3.
rewrite e2; rewrite e3; auto.
SCase "Export Binding".
functional induction
(update_sub_components c'0 (add_binding_aux (c'0 ->subComponents)%comp r0 b)).
clear IHl1 y0.
simpl in *.
functional induction (export_binding i0 i1 i2 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1)
(c1:=c'0) (lc:=lc0); auto.
unfold export_binding.
rewrite H3; rewrite e2; rewrite e1; auto.
unfold export_binding.
rewrite H3.
simpl. rewrite e1.
assert ((c'0 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1) (lc:=lc0); auto .
simpl in H4; subst.
rewrite e2;auto.
SCase "Import Binding".
functional induction
(update_sub_components c'0 (add_binding_aux (c'0 ->subComponents)%comp r0 b)).
clear IHl1 y0.
simpl in *.
functional induction (import_binding i0 i1 i2 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1)
(c1:=c'0) (lc:=lc0); auto.
unfold import_binding.
rewrite H3; rewrite e2; rewrite e1; auto.
unfold import_binding.
rewrite H3.
simpl. rewrite e1.
assert ((c'0 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1) (lc:=lc0); auto .
simpl in H4; subst.
rewrite e2;auto.
Qed.
Lemma well_formed_adding_bindings:
forall lc b p,
well_formed_components lc ->
valid_component_binding' b p lc ->
well_formed_components (add_binding_aux lc p b ).
Proof.
intros.
inversion H0.
Case "Path is nil".
assert (add_binding_aux lc p b= nil).
simpl in *; rewrite H1; eauto.
rewrite H3; auto.
Case "Path is not Nil".
functional induction (add_binding_aux lc p b);
inversion H1; subst; auto; clear H1.
SCase "Exit Branch 1/2".
assert (well_formed_components (c :: r)).
eauto.
split; intros.
SSCase "Unique Ids".
eauto.
SSCase "Well Formed Components".
destruct H3; subst; eauto.
functional induction add_binding_in_component c b.
apply appending_binding_keeps_component_well_formed; eauto.
destruct H2.
assert (x->id%comp = c_id).
eauto.
subst.
assert (((Component id p ic cl lc0 li lb)->id)%comp = (x->id%comp)).
apply lookup_id_fact with (l:=lc) (r:=r);auto.
simpl in H3; subst.
assert (x = Component (x ->id)%comp p ic cl lc0 li lb).
simpl in *; subst.
eauto.
assert ((x ->subComponents)%comp = lc0).
inversion H5; auto.
assert ((x ->interfaces)%comp = li).
inversion H5; auto.
rewrite H5 in *; rewrite H6 in *; auto.
SCase "Exit Branch 2/2".
destruct H2.
unfold get_component_with_path_aux in H1.
rewrite e0 in H1.
destruct r.
SSCase "Tail of Path is nil".
inversion y.
SSCase "Tail of Path is not nil".
assert (well_formed_components (add_binding_aux (c' ->subComponents)%comp (i :: r) b)).
apply IHl; eauto.
Focus.
clear -H0 e0.
inversion H0; inversion H.
destruct H1. clear H.
apply ValidComponentBinding_Step.
exists x.
split; auto.
clear -e0 H1.
unfold get_component_with_path_aux in H1.
rewrite e0 in H1.
exact H1.
split; intros; eauto.
destruct H4. subst. auto.
SSSCase "Component is the head of the list". Focus.
assert ((update_sub_components c' (add_binding_aux (c' ->subComponents) (i :: r) b)
->subComponents)%comp =
(add_binding_aux (c' ->subComponents%comp) (i :: r) b)).
eauto.
assert ((update_sub_components c' (add_binding_aux (c' ->subComponents) (i :: r) b)
->interfaces)%comp = (c'->interfaces%comp)).
eauto.
apply WellFormedComponent; intros.
rewrite H4 in *; eauto.
rewrite H4 in *; eauto.
inversion H1; auto.
rewrite H5 in *.
assert (well_formed_component c').
eauto.
eauto.
rewrite H4 in *; rewrite H5 in *.
assert (
((update_sub_components c' (add_binding_aux (c' ->subComponents) (i :: r) b)
->bindings)%comp =
(c'->bindings%comp)
)).
eauto.
rewrite H6 in *.
clear H5 H6 H4.
assert (well_formed_bindings
(c' ->bindings)%comp
((c' ->subComponents)%comp)
(c' ->interfaces)%comp).
assert (well_formed_component c').
eauto.
inversion H4;auto.
intro; intro.
unfold well_formed_bindings in H4.
assert (valid_binding b0 (c' ->subComponents)%comp (c' ->interfaces)%comp).
auto.
clear H4.
apply valid_adding_binding_fact; auto.
apply well_formed_inheritance; eauto.
destruct (add_binding_aux (c' ->subComponents)%comp (i :: r) b).
inversion y0.
intuition.
congruence.
SSSCase "Component is in the tail".
assert (In c lc).
eauto.
eauto.
Qed.
Lemma root_config_is_unaffected_by_add_binding:
forall s b s',
well_formed s ->
Mk_binding b / s ~~~> Done / s' ->
(s->id%comp) = (s'->id%comp) /\
(s->path%comp) = (s'->path%comp) /\
(s->iclass%comp) = (s'->iclass%comp) /\
(s->controlLevel%comp) = (s'->controlLevel%comp) /\
(s->interfaces%comp) = (s'->interfaces%comp).
Proof.
intros.
destruct s; simpl.
inversion H. destruct H2 as (Hp, (Hic, (Hc, (Hl, Hw)))); subst.
inversion H0; subst. clear H0.
unfold add_binding in H6.
functional induction add_binding_aux l (b ->path)%bind b;
try thus inversion H6.
Qed.
Lemma adding_binding_auxiliary:
forall p lc b,
well_formed_components lc ->
valid_path p lc ->
add_binding_aux lc p b = nil ->
p <> nil ->
False.
Proof.
intros.
functional induction add_binding_aux lc p b; try congruence.
Case "1/3".
inversion H0;
inversion H3; subst. clear H2 H3.
eauto.
Case "2/3".
inversion H0;
inversion H3; subst.
eauto.
Case "3/3".
apply IHl; eauto.
destruct r.
inversion y.
intuition.
inversion H3.
Qed.
Lemma adding_binding_unaffect_bindings:
forall lc li lb I P IC CL,
well_formed_component (Component I P IC CL lc li lb) ->
forall lc' b,
valid_path (b->path%bind) lc ->
(b->path%bind) <> nil ->
lc' = add_binding_aux lc (b->path%bind) b ->
well_formed_components lc' ->
well_formed_bindings lb lc' li.
Proof.
intros.
functional induction add_binding_aux lc (b ->path)%bind b; subst; try congruence.
Case "1/5".
assert (False).
inversion H0;
inversion H2; subst. clear H2 H1.
unfold lookup in e0.
eauto.
inversion H2.
Case "2/5".
assert (well_formed_component (add_binding_in_component c b )).
destruct H3.
apply H3; left; auto.
functional induction add_binding_in_component c b.
inversion H; simpl in *; subst.
inversion e0.
assert (well_formed_bindings lb (Component id p ic cl lc0 li0 lb0 :: r) li).
eauto.
intro; intro.
unfold well_formed_bindings in H8.
assert (valid_binding b0 (Component id p ic cl lc0 li0 lb0 :: r) li).
apply H8; auto.
destruct b0; simpl in *.
SCase "Normal Binding".
unfold normal_binding.
functional induction normal_binding i i0 i1 i2 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb0)
(li:=li0) (lb:=lb0) (r:=r) (i:=i) (x:=c1);
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb0)
(li:=li0) (lb:=lb0) (r:=r) (i:=i1) (x:=c2); auto.
SSSCase "Both in the Head".
rewrite H12; rewrite H13;
rewrite e2; rewrite e3; auto.
SSSCase "Head of the list, tail of the list".
rewrite H13; rewrite H12.
assert ( (c2->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
rewrite <- H14.
rewrite e3; rewrite e2; auto.
SSSCase "In the tail, head of the list".
rewrite H13; rewrite e3.
rewrite H12.
assert ( (c1->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
rewrite <- H14.
rewrite e2; auto.
SSSCase "Both in the tail".
rewrite H13; rewrite H12.
assert ( (c1->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
assert ( (c2->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
rewrite <- H14.
rewrite e2.
rewrite <- H14 in H15.
rewrite <- H15.
rewrite e3; auto.
SSCase "Exit Branch 2/3".
fromfalse.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Export Binding".
unfold export_binding.
functional induction export_binding i i0 i1 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb0)
(li:=li0) (lb:=lb0) (r:=r) (i:=i0) (x:=c'); auto.
SSSCase "Head".
rewrite H12;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H12; rewrite e1.
assert ( (c'->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
rewrite <- H13.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Import Binding".
unfold import_binding.
functional induction import_binding i i0 i1 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=b::lb0)
(li:=li0) (lb:=lb0) (r:=r) (i:=i0) (x:=c'); auto.
SSSCase "Head".
rewrite H12;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H12; rewrite e1.
assert ( (c'->interfaces%comp) = (Component id p ic cl lc0 li0 (b :: lb0) ->interfaces)%comp).
eauto.
rewrite <- H13.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
fromfalse.
Case "3/5".
assert (False).
inversion H0;
inversion H2; subst. clear H2 H1.
unfold lookup in e0.
eauto.
fromfalse.
Case "4/5".
assert (False).
apply adding_binding_auxiliary with (p:=r) (lc:=(c' ->subComponents)%comp) (b:=b); eauto.
destruct r.
inversion y.
intuition.
inversion H2.
fromfalse.
Case "5/5".
clear IHl.
assert (well_formed_bindings lb lc li).
inversion H; simpl in *; subst; auto.
eauto.
Qed.
Removing Well Formed Bindings!
Lemma element_in_removed_set_is_in_original:
forall b lb,
In b (remove_binding_from_list b lb) ->
In b lb.
Proof.
intros.
functional induction remove_binding_from_list b lb.
Case "1/3".
inversion H.
Case "2/3".
left.
symmetry; auto.
Case "3/3".
right.
apply IHl.
destruct H; auto.
subst.
destruct binding_dec with (b:=b) (b':=b).
SCase "Same binding".
assert ((b ==b)%bind = true).
auto.
congruence.
SCase "Not same binding".
congruence.
Qed.
Lemma removing_binding_yields_a_subset_of_original:
forall b b' lb,
In b (remove_binding_from_list b' lb) ->
In b lb.
Proof.
intros.
destruct binding_dec with (b:=b) (b':=b').
subst.
apply element_in_removed_set_is_in_original; auto.
functional induction remove_binding_from_list b' lb.
simpl in H. inversion H.
right. apply IHl; auto.
destruct H.
subst.
left; auto.
right; apply IHl; auto.
Qed.
Hint Resolve removing_binding_yields_a_subset_of_original.
Lemma well_formed_removing_binding_from_list:
forall b lc lb li,
well_formed_bindings lb lc li ->
forall lb', lb' = remove_binding_from_list b lb ->
well_formed_bindings lb' lc li.
Proof.
intros.
unfold well_formed_bindings in H.
intro; intro.
apply H. subst.
apply removing_binding_yields_a_subset_of_original with (b':=b); auto.
Qed.
Hint Resolve well_formed_removing_binding_from_list.
Lemma well_formed_removing_binding_from_component:
forall c b,
well_formed_component c ->
forall c', c' = remove_binding_from_component c b ->
well_formed_component c'.
Proof.
intros.
subst.
unfold remove_binding_from_component.
destruct c.
inversion H; simpl in *; subst;
apply WellFormedComponent; simpl; auto.
apply well_formed_removing_binding_from_list with (b:=b) (lb:=l1); auto.
Qed.
Hint Resolve well_formed_removing_binding_from_component.
Lemma removing_binding_keeps_components_ids_unique:
forall c r b,
unique_ids (c :: r) ->
unique_ids (remove_binding_from_component c b :: r).
Proof.
intros.
functional induction remove_binding_from_component c b.
apply Unique_Step with
(c:=Component id p ic cl lc li (remove_binding_from_list b lb))
(r:=r); simpl; auto.
Case "Id of the head is not in tail".
inversion H; inversion H0; subst; auto.
Case "Tail have unique ids".
inversion H; inversion H0; auto.
Qed.
Hint Resolve removing_binding_keeps_components_ids_unique.
Lemma well_formed_component_minus_one_binding:
forall i p ic c lc li b r,
well_formed_component (Component i p ic c lc li (b :: r)) ->
well_formed_component (Component i p ic c lc li r).
Proof.
intros.
inversion H; simpl in *; subst.
apply WellFormedComponent; simpl; auto.
unfold well_formed_bindings in H3.
intro; intro.
apply H3.
right; auto.
Qed.
Hint Resolve well_formed_component_minus_one_binding.
Lemma removing_binding_from_list_keeps_bindings_well_formed:
forall b b' r lc li,
well_formed_bindings (b :: r) lc li ->
well_formed_bindings (b :: remove_binding_from_list b' r) lc li.
Proof.
intros.
functional induction remove_binding_from_list b' r; auto.
Case "Branch 1/2".
apply IHl.
unfold well_formed_bindings in H.
intro; intro.
apply H.
destruct H0; subst; auto.
left; auto.
right; right; auto.
Case "Branch 2/2".
clear IHl.
intro; intro.
apply H.
destruct H0; subst.
left; auto.
destruct H0; subst.
right; left; auto.
right; right; eauto.
Qed.
Hint Resolve removing_binding_from_list_keeps_bindings_well_formed.
Lemma removing_a_binding_keeps_component_well_formed:
forall c b,
well_formed_component c ->
well_formed_component (remove_binding_from_component c b).
Proof.
intros.
destruct c. simpl.
apply WellFormedComponent; simpl; intros; eauto.
functional induction remove_binding_from_list b l1; auto.
Case "Branch 1/2".
apply IHl2; eauto.
Case "Branch 2/2".
clear IHl2.
inversion H; simpl in *; subst; auto.
Qed.
Hint Resolve removing_a_binding_keeps_component_well_formed.
Lemma valid_removing_binding_fact:
forall b0 c' r b,
unique_ids (c' ->subComponents)%comp ->
In b0 (c' ->bindings)%comp ->
(remove_binding_aux (c' ->subComponents)%comp r b) <> nil ->
valid_binding b0 (c' ->subComponents)%comp (c' ->interfaces)%comp ->
valid_binding b0 (remove_binding_aux (c' ->subComponents)%comp r b) (c' ->interfaces)%comp.
Proof.
intros b0 c' r b Hunique.
intros.
functional induction (remove_binding_aux (c' ->subComponents)%comp r b); try congruence.
Case "Exit Branch 1/2".
destruct b0.
SCase "Normal Binding".
functional induction remove_binding_from_component c b.
simpl in *.
functional induction (normal_binding i i0 i1 i2 lc (c' ->interfaces)%comp);
try inversion H1.
unfold normal_binding in *.
destruct get_component_fact'' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0)
(lb':=(remove_binding_from_list b lb)) (li:=li)
(lb:=lb) (r:=r) (i:=i) (x:=c1);
destruct get_component_fact'' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0)
(lb':=(remove_binding_from_list b lb)) (li:=li)
(lb:=lb) (r:=r) (i:=i1) (x:=c2);
eauto.
SSCase "Both head of the list".
rewrite H4; rewrite H5.
rewrite e3; rewrite e2; auto.
SSCase "Head of the list, in the tail".
rewrite H4; rewrite H5.
rewrite e2.
assert ( (c2->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=remove_binding_from_list b lb) (li:=li)
(lb:=lb) (r:=r) (i:=i1); eauto.
rewrite H6 in e3.
rewrite e3; auto.
SSCase "In the tail of the list, the head of the list".
rewrite H4; rewrite H5.
rewrite e3.
assert ( (c1->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=remove_binding_from_list b lb) (li:=li)
(lb:=lb) (r:=r) (i:=i); eauto.
rewrite H6 in e2.
rewrite e2; auto.
SSCase "Both in the tail".
assert ( (c2->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=remove_binding_from_list b lb) (li:=li)
(lb:=lb) (r:=r) (i:=i1); eauto.
assert ( (c1->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
apply get_component_fact_same_interfaces' with (id:=id) (p:=p0) (ic:=ic) (cl:=cl)
(lc:=lc0) (lb':=remove_binding_from_list b lb) (li:=li)
(lb:=lb) (r:=r) (i:=i); eauto.
rewrite H6 in e3.
rewrite H7 in e2.
rewrite H4; rewrite H5.
rewrite e3; rewrite e2; auto.
SCase "Export Binding".
functional induction remove_binding_from_component c b.
simpl in *.
unfold export_binding.
functional induction export_binding i i0 i1 lc (c' ->interfaces)%comp.
SSCase "Exit Branch 1/3".
inversion H1.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=remove_binding_from_list b lb)
(li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'0); eauto.
SSSCase "Head".
rewrite H2;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H2; rewrite e1.
assert ( (c'0->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
eauto.
rewrite <- H3.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
inversion H1.
SCase "Import Binding".
functional induction remove_binding_from_component c b.
simpl in *.
unfold import_binding.
functional induction import_binding i i0 i1 lc (c' ->interfaces)%comp.
SSCase "Exit Branch 1/3".
inversion H1.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p0) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=remove_binding_from_list b lb)
(li:=li) (lb:=lb) (r:=r) (i:=i0) (x:=c'0); eauto.
SSSCase "Head".
rewrite H2;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H2; rewrite e1.
assert ( (c'0->interfaces%comp) = (Component id p0 ic cl lc0 li (remove_binding_from_list b lb) ->interfaces)%comp).
eauto.
rewrite <- H3.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
inversion H1.
Case "Exit Branch 2/2".
clear H0.
destruct b0.
SCase "Normal Binding".
functional induction
(update_sub_components c'0 (remove_binding_aux (c'0 ->subComponents)%comp r b)).
clear IHl0 y0.
simpl in *.
functional induction (normal_binding i i0 i1 i2 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i)
(c1:=c1) (lc:=lc0);
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1)
(c1:=c2) (lc:=lc0); auto.
unfold normal_binding.
rewrite H4; rewrite H3; rewrite e2; rewrite e3; auto.
unfold normal_binding.
rewrite H3; rewrite H4.
simpl. rewrite e2.
assert ((c2 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (cl:=cl) (ic:=iclass)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1) (lc:=lc0); auto .
simpl in H5; subst.
rewrite e3;auto.
unfold normal_binding.
rewrite H4; rewrite H3; simpl; rewrite e3.
assert ((c1 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i) (lc:=lc0); auto .
simpl in H5; subst.
rewrite e2;auto.
unfold normal_binding.
rewrite H4; rewrite H3. simpl.
assert ((c1 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i) (lc:=lc0); auto .
simpl in H5.
assert ((c2 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i1) (lc:=lc0); auto .
simpl in H6.
rewrite H5 in e2.
rewrite H6 in e3.
rewrite e2; rewrite e3; auto.
SCase "Export Binding".
functional induction
(update_sub_components c'0 (remove_binding_aux (c'0 ->subComponents)%comp r b)).
clear IHl0 y0.
simpl in *.
functional induction (export_binding i i0 i1 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0)
(c1:=c'0) (lc:=lc0); auto.
unfold export_binding.
rewrite H3; rewrite e2; rewrite e1; auto.
unfold export_binding.
rewrite H3.
simpl. rewrite e1.
assert ((c'0 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0) (lc:=lc0); auto .
simpl in H4; subst.
rewrite e2;auto.
SCase "Import Binding".
functional induction
(update_sub_components c'0 (remove_binding_aux (c'0 ->subComponents)%comp r b)).
clear IHl0 y0.
simpl in *.
functional induction (import_binding i i0 i1 lc (c' ->interfaces)%comp);
try inversion H1.
destruct prime_list_lookup with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass)
(cl:=cl) (lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0)
(c1:=c'0) (lc:=lc0); auto.
unfold import_binding.
rewrite H3; rewrite e2; rewrite e1; auto.
unfold import_binding.
rewrite H3.
simpl. rewrite e1.
assert ((c'0 ->interfaces)%comp = (Component id0 p0 iclass cl lc0 li lb->interfaces%comp)).
symmetry.
apply interfaces_are_the_same with
(some_lc:=lc) (some_id:=id) (id:=id0) (p:=p0) (ic:=iclass) (cl:=cl)
(lc':=lc') (li:=li) (lb:=lb) (backup:=backup) (i0:=i0) (lc:=lc0); auto .
simpl in H4; subst.
rewrite e2;auto.
Qed.
Lemma valid_removing_binding_fact':
forall b0 r b lc lb li id p ic cl,
well_formed_component (Component id p ic cl lc li lb) ->
unique_ids lc ->
In b0 lb ->
(remove_binding_aux lc r b) <> nil ->
valid_binding b0 lc li ->
valid_binding b0 (remove_binding_aux lc r b) li.
Proof.
intros.
replace lc with ((Component id p ic cl lc li lb)->subComponents%comp); auto.
apply valid_removing_binding_fact; auto.
Qed.
Lemma well_formed_removing_bindings:
forall lc b p,
well_formed_components lc ->
well_formed_components (remove_binding_aux lc p b ).
Proof.
intros.
functional induction remove_binding_aux lc p b; auto.
Case "Branch 1/2".
split.
SCase "Ids are unique".
assert (unique_ids (c :: r)).
eauto.
auto.
SCase "Well Formed Components".
intros.
destruct H0; subst; eauto.
Case "Branch 2/2".
unfold update_sub_components.
destruct c'.
simpl.
simpl in *.
assert (well_formed_components (Component i p i0 c l l0 l1 :: backup)).
eauto.
split.
SCase "Ids are unique".
inversion H0.
inversion H1; inversion H3; subst.
apply Unique_Step with
(c:=Component i p i0 c (remove_binding_aux l r b) l0 l1 )
(r:=r0); simpl; eauto.
SCase "Well formed components".
intros.
destruct H1; subst; eauto.
assert (well_formed_components (remove_binding_aux l r b)).
apply IHl; eauto.
clear e0 IHl.
assert (well_formed_component (Component i p i0 c l l0 l1)).
inversion H0.
apply H3; left; auto.
apply WellFormedComponent; simpl; intros; eauto.
inversion H2; simpl in *; subst; auto.
intro; intro.
apply valid_removing_binding_fact' with (id:=i) (lb:=l1) (p:=p) (ic:=i0) (cl:=c); auto.
destruct (remove_binding_aux l r b).
inversion y0.
discriminate.
Qed.
Lemma root_config_is_unaffected_by_remove_binding:
forall s b s',
well_formed s ->
Rm_binding b / s ~~~> Done / s' ->
(s->id%comp) = (s'->id%comp) /\
(s->path%comp) = (s'->path%comp) /\
(s->iclass%comp) = (s'->iclass%comp) /\
(s->controlLevel%comp) = (s'->controlLevel%comp) /\
(s->interfaces%comp) = (s'->interfaces%comp).
Proof.
intros.
destruct s; simpl.
inversion H. destruct H2 as (Hp, (Hic, (Hc, (Hl, Hw)))); subst.
inversion H0; subst. clear H0.
unfold remove_binding in H5.
functional induction remove_binding_aux l (b->path%bind) b;
try thus destruct s'; inversion H5; subst; simpl; intuition.
Qed.
Lemma removing_binding_auxiliary:
forall p lc b,
well_formed_components lc ->
valid_path p lc ->
remove_binding_aux lc p b = nil ->
p <> nil ->
False.
Proof.
intros.
functional induction remove_binding_aux lc p b; try congruence.
Case "1/3".
inversion H0;
inversion H3; subst. clear H2 H3.
eauto.
Case "2/3".
inversion H0;
inversion H3; subst.
eauto.
Case "3/3".
apply IHl; eauto.
destruct r.
inversion y.
intuition.
inversion H3.
Qed.
Lemma removing_binding_unaffect_bindings:
forall lc li lb I P IC CL,
well_formed_component (Component I P IC CL lc li lb) ->
forall lc' b,
valid_path (b->path%bind) lc ->
(b->path%bind) <> nil ->
lc' = remove_binding_aux lc (b->path%bind) b ->
well_formed_components lc' ->
well_formed_bindings lb lc' li.
Proof.
intros.
functional induction remove_binding_aux lc (b ->path)%bind b; subst; try congruence.
Case "1/5".
assert (False).
inversion H0;
inversion H2; subst. clear H2 H1.
unfold lookup in e0.
eauto.
inversion H2.
Case "2/5".
assert (well_formed_component (remove_binding_from_component c b )).
destruct H3.
apply H3; left; auto.
functional induction remove_binding_from_component c b.
inversion H; simpl in *; subst.
inversion e0.
assert (well_formed_bindings lb (Component id p ic cl lc0 li0 lb0 :: r) li).
eauto.
intro; intro.
assert (valid_binding b0 (Component id p ic cl lc0 li0 lb0 :: r) li).
apply H8; auto.
destruct b0; simpl in *.
SCase "Normal Binding". Focus.
unfold normal_binding.
functional induction normal_binding i i0 i1 i2 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=(remove_binding_from_list b lb0))
(li:=li0) (lb:=lb0) (r:=r) (i:=i) (x:=c1);
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=(remove_binding_from_list b lb0))
(li:=li0) (lb:=lb0) (r:=r) (i:=i1) (x:=c2); auto.
SSSCase "Both in the Head".
rewrite H13; rewrite H12;
rewrite e2; rewrite e3; auto.
SSSCase "Head of the list, tail of the list".
rewrite H13;
rewrite H12.
assert ( (c2->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
rewrite <- H14.
rewrite e3; rewrite e2; auto.
SSSCase "In the tail, head of the list".
rewrite H13.
rewrite H12.
assert ( (c1->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
rewrite <- H14.
rewrite e2; auto.
rewrite e3; auto.
SSSCase "Both in the tail".
rewrite H13; rewrite H12.
assert ( (c1->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
assert ( (c2->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
rewrite <- H15. rewrite e3.
rewrite <- H14 in H15.
rewrite H15; rewrite e2; auto.
SSCase "Exit Branch 2/3".
fromfalse.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Export Binding".
unfold export_binding.
functional induction export_binding i i0 i1 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=(remove_binding_from_list b lb0))
(li:=li0) (lb:=lb0) (r:=r) (i:=i0) (x:=c'); auto.
SSSCase "Head".
rewrite H12;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H12; rewrite e1.
assert ( (c'->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
rewrite <- H13.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
fromfalse.
SCase "Import Binding".
unfold import_binding.
functional induction import_binding i i0 i1 (Component id p ic cl lc0 li0 lb0 :: r) li.
SSCase "Exit Branch 1/3".
fromfalse.
SSCase "Exit Branch 2/3".
destruct get_component_fact'' with
(id:=id) (p:=p) (ic:=ic) (cl:=cl) (lc:=lc0) (lb':=(remove_binding_from_list b lb0))
(li:=li0) (lb:=lb0) (r:=r) (i:=i0) (x:=c'); auto.
SSSCase "Head".
rewrite H12;
rewrite e2;
rewrite e1; auto.
SSSCase "Tail of the list".
rewrite H12; rewrite e1.
assert ( (c'->interfaces%comp) = (Component id p ic cl lc0 li0 ((remove_binding_from_list b lb0)) ->interfaces)%comp).
eauto.
rewrite <- H13.
rewrite e2; auto.
SSCase "Exit Branch 3/3".
fromfalse.
Case "3/5".
assert (False).
inversion H0;
inversion H2; subst. clear H2 H1.
unfold lookup in e0.
eauto.
inversion H2.
Case "4/5".
assert (False).
apply removing_binding_auxiliary with (p:=r) (lc:=(c' ->subComponents)%comp) (b:=b); eauto.
destruct r.
inversion y.
intuition.
inversion H2.
inversion H2.
Case "5/5".
clear IHl.
assert (well_formed_bindings lb lc li).
inversion H; simpl in *; subst; auto.
eauto.
Qed.