The Coq mailing list

[franck.barbier AT franckbarbier.com]

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.