Mefresa.GCM.Base

More on Idents

In a standard programming language, like say OCaml, trying to get the head element of some list will yield an exception if the list is empty. In Coq however, it is not the case, as there is no "built-in" notion of exception. As such, functions like hd expect a parameter that defines a default value to return in the cases where one would usually use an exception in a standard programming scenario. Therefore, we will actually need to define a special identifier.

Definition ErrorIdent : ident := Ident "ExceptionIdent".

On Paths

The above definitions are not sufficient to model an interface. Indeed, the GCM Component Model is an hierarchical component model. The way we encode this shall be discussed later, but for now we can focus on the fact that in order to identify an interface we need to locate it in the hierarchy. Therefore, we need another field indicating its position, we shall call it path.

Definition path : Type := list ident.
Naturaly, two paths are equal if all identifiers constituting them are equal.

Function beq_path (p p':path) {struct p} : bool :=
  match p, p' with
    | nil, nil => true
    | id :: r, id' :: r' => if (id != id') then false else beq_path r r'
    | _, _ => false
  end.

Bind Scope path_scope with path.
Delimit Scope path_scope with path.
Notation "p1 '==' p2" := (beq_path p1 p2) (at level 80) : path_scope.
Notation "p1 '!=' p2" := (~~ beq_path p1 p2) (at level 80) : path_scope.

Lemma path_refl:
  forall p : path, (p == p)%path = true.
Proof.
  induction p; simpl; auto.
  destruct ident_dec with (id1:=a) (id2:=a).
  assert ((a==a) = true).
    auto.
  unfold bneq_ident.
  rewrite H. auto.
  congruence.
Qed.

Hint Resolve path_refl.

Lemma path_eq_reflection:
  forall p p' : path, (p==p')%path=true <-> p=p'.
Proof.
  induction p; induction p'; split; intros; simpl in *; try congruence.
  assert ((a==a0)=true -> a = a0).
    auto.
  assert ((a!=a0)=true -> a <> a0).
    auto.
  unfold bneq_ident in *.
  destruct ((a == a0)).
  assert (a = a0); auto.
  subst. apply f_equal.
  apply IHp; auto.
  congruence.
  inversion H; subst. clear H.
  destruct ident_dec with (id1:=a0) (id2:=a0).
  assert ((a0==a0) = true).
    auto.
  unfold bneq_ident.
  rewrite H.
  apply IHp. refl.
  congruence.
Qed.