The Coq mailing list

[franck.barbier AT franckbarbier.com]

Hi,

I wonder why (PS : I'm not a Coq expert at all) I cannot apply (bidirectional)
substitutions between inhabitants of 'sig isConcrete' and '{x : Class |
isConcrete x}'.

My Coq code just simulates the fact that in object-oriented programming, one
cannot instantiate an "abstract" class.

Any idea? Thanks in advance...

Require ListSet.
Require Import String.

Open Scope list_scope.
Open Scope string_scope.

Definition isAbstract_label : string := "isAbstract".
Definition isComposite_label : string := "isComposite".
Definition class_label := "class".
Definition name_label := "name".
Definition ownedAttribute_label := "ownedAttribute".
Definition type_label := "type".

Definition N := 100.

Inductive Class : Type :=
    BBoolean | (* UML Boolean *)
    CClass |
    PProperty |
    instantiate : Class -> string -> Class |
    instantiate' : Class -> string -> ListSet.set Property -> Class
with Property : Type :=
    Null : Property | (* 'Null' is introduced in the MOF Core Specification,
v2.0, p. 11 *)
    set_isAbstract : Property |
    set_ownedAttribute : string -> Class -> nat -> nat -> bool -> Property | 
(*
attribute name, attribute type, lower bound, upper bound, isComposite or not 
*)
    set_superClass : Class -> Property.

Definition ownedAttribute(c : Class) : ListSet.set Property := match c with
  | BBoolean => nil
  | CClass => (set_ownedAttribute isAbstract_label BBoolean 1 1
true)::(set_ownedAttribute ownedAttribute_label PProperty 0 N true)::nil
  | PProperty => (set_ownedAttribute isComposite_label BBoolean 1 1
true)::(set_ownedAttribute class_label CClass 0 1 false)::nil
  | instantiate _ _ => nil
  | instantiate' _ _ l => l
end.

Inductive isAbstract(c : Class) : Prop :=
  isAbstractDef : ListSet.set_In set_isAbstract (ownedAttribute c) ->
isAbstract c.

Inductive isConcrete(c : Class) : Prop :=
  isConcreteDef : ~ isAbstract c -> isConcrete c.

Lemma CClass_is_concrete : isConcrete CClass.
Proof.
  constructor.
  intro.
  destruct H.
  destruct H.
  discriminate.
  elim H.
  discriminate.
  trivial.
Qed.

(* 'make_instance' (simplified version only) just creates a class from a
concrete (ie, non abstract) class: *)

Definition make_instance (c : {x : Class | isConcrete x}) (n : string) : Class
:= match c with (* 'sig isConcrete' does not work?  *)
    exist c' _ => instantiate c' n
end.

Definition ooo := exist (fun x => isConcrete x) CClass CClass_is_concrete.

Definition Object := make_instance (exist (fun x => isConcrete x) CClass
CClass_is_concrete) "Object".