coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: franck.barbier AT franckbarbier.com
- To: coq-club AT inria.fr
- Subject: [Coq-Club] UML built with inductive types...
- Date: Mon, 2 May 2011 16:08:27 +0200
Hi,
Trying to specify UML by inductive types, I stumble (again!) over the problem
(see '??????' below) of proving that 'S n <> n' (Naturals metaphor). I have an
'instantiate' creation protocol below and (simplified version) of course I
expect 'instantiate c <> c'. However, Coq asks me to prove it...
PS : I already got inputs from Adam and Vincent Dema, Sylvain Heraut on that
(previous posts) but difficulties remain...
Help appreciated.
Require Import List.
Require Import String.
Definition isAbstract_label : string := String "+" (String "i" (String "s"
(String "A" (String "b" (String "s" (String "t" (String "r" (String "a"
(String
"c" (String "t" (EmptyString))))))))))).
Print isAbstract_label.
Definition isComposite_label : string := String "+" (String "i" (String "s"
(String "C" (String "o" (String "m" (String "p" (String "o" (String "s"
(String
"i" (String "t" (String "e" (EmptyString)))))))))))).
Print isComposite_label.
Definition type_navigation_label : string := String "+" (String "t" (String
"y"
(String "p" (String "e" (EmptyString))))).
Print type_navigation_label.
Inductive Class : Type :=
BBoolean | (* UML Boolean *)
CClass |
PProperty |
instantiate : NonAbstractClass -> Property -> Property -> Class | (*
Axiom:
an abstract class has no direct instances *)
inheritsFrom : Property -> Property -> Property -> Class (* One may
inherit
from 'CClass'? Does it matter? *)
with Property : Type :=
Null | (* 'Null' is introduced in the MOF Core Specification, v2.0, p. 11
*)
set_isAbstract : Property |
set_isComposite : Property |
set_ownedAttribute : string -> Class -> nat -> nat -> Property -> Property
| (* attribute name, attribute type, lower bound, upper bound, isComposite or
not *)
set_superClass : Class -> Property (* Inheritance *)
with NonAbstractClass : Type :=
ToNonAbstract : Class -> NonAbstractClass.
Definition Object := instantiate (ToNonAbstract CClass) Null Null. (* MOF Core
Specification, v2.0, p. 15 *)
Definition Element := inheritsFrom (set_superClass Object) set_isAbstract
Null.
(* MOF Core Specification, v2.0, p. 15 *)
Definition NamedElement := inheritsFrom (set_superClass Element)
set_isAbstract
Null. (* Infrastructure v2.3, p. 92 *)
Definition TType := inheritsFrom (set_superClass NamedElement) set_isAbstract
Null. (* Infrastructure v2.3, p. 92 *)
Definition TypedElement := inheritsFrom (set_superClass NamedElement)
set_isAbstract (set_ownedAttribute type_navigation_label TType 0 1 Null). (*
Infrastructure v2.3, p. 92 *)
Definition MultiplicityElement := inheritsFrom (set_superClass Element)
set_isAbstract Null. (* Infrastructure v2.3, p. 64. 4 attributes are missing
*)
Definition Classifier := inheritsFrom (set_superClass TType) set_isAbstract
Null. (* Infrastructure v2.3, p. 50 *)
Definition Relationship := inheritsFrom (set_superClass Element)
set_isAbstract
Null. (* Infrastructure v2.3, p. 105 *)
Definition DirectedRelationship := inheritsFrom (set_superClass Relationship)
set_isAbstract Null. (* Infrastructure v2.3, p. 105 *)
Definition Generalization := inheritsFrom (set_superClass
DirectedRelationship)
Null. (* Infrastructure v2.3, p. 50 *)
(* 'Class' inherits from 'Classifier' while both 'Class' and 'Classifier'
already inherit from 'Type'? *) (* Infrastructure v2.3, p. 111 *)
Definition Association := inheritsFrom (set_superClass Classifier)
(set_superClass Relationship) Null. (* Infrastructure v2.3, p. 111 *)
Fixpoint class(c : Class) : Class := match c with
| instantiate (ToNonAbstract c') _ _ => c'
| inheritsFrom (set_superClass super) _ _ => class super (* Problem here:
inheriting from 2 classes or more which do not belong to the same modeling
level! *)
| _ => CClass (* BBoolean => CClass | CClass => CClass | PProperty => CClass
*)
end.
Eval compute in (class Object).
Eval compute in (class Element).
Inductive instance_of(c' : Class) : Class -> Prop := (* e.g., 'instance_of
CClass Object' *)
def : forall c, c' = class c -> instance_of c' c.
Eval compute in (instance_of CClass Object).
Fixpoint metaness(n : nat) (c : Class) : Class := match n with (* Kuhne's
paper
p. 377 *)
| 0 => c
| S m => class (metaness m c)
end.
Definition superClass(c : Class) : Set := match c with (* MOF Core
Specification, v2.0, p. 33, 'superClass' navigation from 'Class' to 'Class' *)
| CClass => forall c : Class, c = TType (* MOF Core Specification, v2.0, p. 33
. Il y a aussi un h�ritage de Classifier p. 111*)
| PProperty => forall c : Class, c = TypedElement /\ c = MultiplicityElement
(*
MOF Core Specification, v2.0, p. 33 *)
| inheritsFrom p1 p2 p3 => forall c : Class, set_superClass c = p1 \/
set_superClass c = p2 \/ set_superClass c = p3
| _ => Empty_set
end.
Definition ownedAttribute(c : Class) : list Property := match c with
| CClass => cons (set_ownedAttribute isAbstract_label BBoolean 1 1
set_isComposite) nil
| PProperty => cons (set_ownedAttribute isComposite_label BBoolean 1 1
set_isComposite) nil
| inheritsFrom p1 p2 p3 => p1::p2::p3::nil
| _ => nil
end.
Eval compute in (ownedAttribute Object).
Eval compute in (ownedAttribute Element).
Lemma No_loop : forall c : Class, forall p p' : Property, instantiate
(ToNonAbstract c) p p' <> c.
Proof.
intros.
induction c.
intros;discriminate.
intros;discriminate.
intros;discriminate.
injection.
intros.
(* ?????????????? *)
admit.
admit.
(* ????????????? *)
Save.
Axiom No_loop' : forall c : Class, forall p p' : Property, inheritsFrom
(set_superClass c) p p' <> class c.
Lemma Instantiation_quasi_irreflexivity : forall c : Class, c = class c -> c =
CClass.
Proof.
induction c;trivial.
intros.
destruct n.
simpl in H.
rewrite H.
destruct (No_loop c p p0).
exact H.
intros.
destruct p;trivial.
simpl in H.
rewrite H.
destruct (No_loop' c p0 p1).
exact H.
Save.
- [Coq-Club] UML built with inductive types..., franck . barbier
- Re: [Coq-Club] UML built with inductive types..., Pierre Casteran
Archive powered by MhonArc 2.6.16.