Mefresa.GCM.CoreElementsFacts

A Few More Words on Interfaces, Bindings and Components

In this section we define the means to ease the manipulation of our core elements. For each, we define the projections to its fields, along with some syntactic sugar to improve readability.
Moreover, whenever appropriate we define functions that may be useful at a later stage.

Require Export Mefresa.GCM.Base.
Require Export Mefresa.GCM.Interface.
Require Export Mefresa.GCM.Binding.
Require Export Mefresa.GCM.Component.
Require Export Mefresa.GCM.Examples.
Components will be our first-class citizens. As such it is of our interest to define several general purpose functions for them.

Function component_interface_id_exists (id:ident) (l:list component) {struct l} : bool :=
  match l with
      | nil => false
      | c :: r => if interface_id_exists id (c->interfaces%comp) then
                      true
                  else
                       component_interface_id_exists id r
    end.

Function get_component (id:ident) (l:list component) {struct l}: option component :=
    match l with
      | nil => None
      | e :: r => if (e->id)%comp == id then Some e else get_component id r
    end.

Notation "l '[' id ']'" := (get_component id l) (at level 60, right associativity).

Lemma membership_fact:
  forall l id c,
  l [id] = Some c ->
  In c l.
Proof.
  intros.
  functional induction get_component id l.
  Case "1/3".
    thus inversion H.
  Case "2/3".
    inversion H; subst. clear H.
    thus left; auto.
  Case "3/3".
    right.
    thus apply IHo; auto.
Qed.

Lemma get_component_correct:
  forall l c id,
    l [id] = Some c ->
    (c ->id)%comp = id.
Proof.
  intros.
  functional induction get_component id l; auto.
  Case "Branch 1/2".
    thus inversion H.
  Case "Branch 2/2".
    thus inversion H; subst; auto.
Qed.

Hint Resolve membership_fact get_component_correct.

Definition get_subComponent (id:ident) (c:component) : option component :=
   get_component id (c->subComponents)%comp.

Function remove_component_from_list (id:ident) (l:list component) {struct l}: list component :=
    match l with
      | nil => nil
      | e :: r => if (e->id)%comp == id then
                    remove_component_from_list id r
                  else
                    e :: remove_component_from_list id r
    end.
Moreover, since some of our functions return option components, we may need to compare those as well. As such, we define the following function:

Definition beq_opt_comp opt_comp1 opt_comp2 : bool :=
  match opt_comp1, opt_comp2 with
    | Some comp1, Some comp2 => beq_ident (comp1->id)%comp (comp2->id)%comp
    | _, _ => false
  end.

Notation "s1 '==' s2" := (beq_opt_comp s1 s2) (at level 80) : opt_comp_scope.
Notation "s1 '!=' s2" := (~beq_opt_comp s1 s2) (at level 80) : opt_comp_scope.

Bind Scope opt_comp_scope with option component.
Delimit Scope opt_comp_scope with opt_comp.

Inductive not_in_l i l: Prop :=
  | NotInNil : l = (nil: list component) ->
                not_in_l i l
  | NotInStep : forall (a:component) (r:list component),
                l = a :: r ->
                (((a->id)%comp == i) = false) ->
                not_in_l i r ->
                not_in_l i l.

Lemma not_in_l_nil:
  forall id, not_in_l id nil.
Proof.
  intro.
  thus apply NotInNil; reflexivity.
Qed.

Hint Resolve not_in_l_nil.

Definition not_in_list (i:ident) (l:list component) : Prop :=
   forall e, In e l -> (((e->id)%comp == i) = false).

Lemma same_nots':
  forall i l, not_in_list i l -> not_in_l i l.
Proof.
  intros.
  induction l.
  apply NotInNil.
  reflexivity.
  unfold not_in_list in H.
  assert (((a ->id)%comp == i) = false).
  apply H with (e:=a); intuition.
  apply NotInStep with (a:=a) (r:=l).
  reflexivity.
  unfold not_in_list in H.
  apply H with (e:=a).
  intuition.
  apply IHl.
  unfold not_in_list.
  intros.
  apply H.
  intuition.
Qed.

Lemma same_nots:
  forall i l, not_in_l i l -> not_in_list i l.
Proof.
  induction 1.
  subst.
  unfold not_in_list.
  intros.
  inversion H.
  subst.
  unfold not_in_list.
  intros.
  destruct H.
  subst.
  exact H0.
  unfold not_in_list in IHnot_in_l.
  apply IHnot_in_l.
  exact H.
Qed.

Hint Resolve same_nots same_nots.

Lemma not_in_congruence:
      forall c l,
        not_in_l (c->id%comp) l ->
        In c l ->
        False.
Proof.
  intros.
  apply same_nots in H.
  unfold not_in_list in H.
  assert (((c ->id)%comp == (c ->id)%comp) = false).
    apply H; auto.
  assert (((c ->id)%comp <> (c ->id)%comp)).
    eauto.
  congruence.
Qed.

Inductive unique_ids (l:list component) : Prop :=
  | Unique_Base: l = nil -> unique_ids l
  | Unique_Step: forall c r,
                 l = c :: r ->
                 not_in_l (c->id%comp) r ->
                 unique_ids r ->
                 unique_ids l.

Lemma unique_ids_nil:
  unique_ids nil.
Proof.
  thus apply Unique_Base; reflexivity.
Qed.

Lemma unique_ids_one:
  forall x, unique_ids (x :: nil).
Proof.
  intros.
  eapply Unique_Step; auto.
  thus apply unique_ids_nil.
Qed.

Lemma unique_ids_sublist:
  forall c r,
   unique_ids (c :: r) ->
    unique_ids r.
Proof.
  intros.
  inversion H.
  Case "List is nil".
    thus inversion H0.
  Case "List is not nil".
    thus inversion H0; subst; auto.
Qed.

Lemma unique_subset_gen:
  forall l1 l2,
    unique_ids (app l1 l2) ->
    unique_ids l2.
Proof.
  intros.
  induction l1.
  rewrite app_nil_l in H;auto.
  apply IHl1.
  rewrite <- app_comm_cons in H.
  inversion H.
  inversion H0.
  inversion H0; subst; auto.
Qed.

Lemma unique_subset:
  forall c r acc,
    unique_ids (app (cons c r) acc) ->
    unique_ids (cons c acc).
Proof.
  intros.
  assert (unique_ids acc).
    apply unique_subset_gen with (l1:=c::r);auto.
  apply Unique_Step with (c:=c) (r:=acc);auto.
  inversion H.
  Case "Nil".
    inversion H1.
  Case "Not Nil".
    inversion H1; subst. clear H1.
    clear H.
    induction r.
    SCase "R is Nil".
      rewrite app_nil_l in H2; auto.
    SCase "R is not Nil".
      apply IHr;auto.
      inversion H2; inversion H; subst; auto.
      inversion H3; inversion H; subst; auto.
Qed.

Lemma unique_ids_fact:
forall c r e,
    unique_ids (c :: r) ->
    In e r ->
    ((e->id%comp) == (c->id%comp)) = false.
Proof.
  intros.
  inversion H; inversion H1; subst. clear H1.
  apply same_nots in H2.
  unfold not_in_list in H2.
  apply H2; auto.
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.

Definition unique_ids' (l:list component) : Prop :=
  forall c c', In c l ->
               In c' l ->
               ((c->id)%comp == (c'->id)%comp) = false.

Lemma same_unique_ids:
  forall l,
     unique_ids' l ->
     unique_ids l.
Proof.
  induction l;intros.
  Case "l is nil".
    apply Unique_Base; reflexivity.
  Case "l is not nil".
    apply Unique_Step with (c:=a) (r:=l);auto.
    unfold unique_ids' in H.
    apply same_nots';auto.
    unfold not_in_list; intros.
    apply H; auto.
    right; exact H0.
    left; reflexivity.
    apply IHl.
    unfold unique_ids' in H.
    unfold unique_ids'; intros.
    apply H.
    right; auto.
    right; auto.
Qed.

Hint Resolve unique_ids_nil same_unique_ids unique_ids_sublist unique_ids_one.

Function in_l (id:ident) (l:list component) {struct l}: Prop :=
  match l with
    | nil => False
    | c :: r => (c->id)%comp = id \/ in_l id r
  end.

Hint Resolve internal_or_external visibility_dec beq_visibility_symmetry
              beq_visibility_reflexivity interfaces_fact.