The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi Franck,

  Your problem is certainly related with mutually inductive types.

  I've attached a file where I kept only some significant constructors and
deleted all non-pertinent definitions and lemmas for dealing only with
the "admit" parts of your proof.

The solution  consists in defining a size for the terms of your inductive
types (in fact three size functions).
Then the proof on No_loop is very simple.


Note that you must have a look at some sections of the reference manual
that deal with mutually inductive types :
http://coq.inria.fr/refman/Reference-Manual011.html#@command229
and http://coq.inria.fr/refman/Reference-Manual013.html#Scheme-examples

Every proof by induction or recursive definition (like the size 
functions) will
have to deal not only with Class but also with the other types :
Property and NonAbstractClass.

A last remark:
When submitting problems like this one, it would be better to delete
all non pertinent informations from the code you send to us.
I could write the solution I have attached only after having deleted
a few constructors and all definitions that were not used in No_loop.

Best regards,

Pierre
Require Import List.
Require Import String.

Inductive Class : Type :=
    BBoolean | (* UML Boolean *)
    instantiate : NonAbstractClass -> Property -> Property -> Class 
with Property : Type :=
    Null :Property| 
    set_ownedAttribute : string -> Class -> nat -> nat -> Property -> 
Property 
with NonAbstractClass : Type :=
   ToNonAbstract : Class -> NonAbstractClass.




Fixpoint sizeC  (c:Class) : nat := match c with
| BBoolean => 1
|instantiate n p p' => S(sizeN n + sizeP p + sizeP p')
end
with sizeP (p:Property) : nat :=
  match p with 
 Null => 1
| set_ownedAttribute s c n n' p => S(sizeC c + sizeP p)
end
with sizeN  (n:  NonAbstractClass):nat :=
match n with  ToNonAbstract c => S (sizeC c)
end.

Scheme Class_ind' := Induction for Class Sort Prop with
       Property_ind' := Induction for Property Sort Prop with 
       NonAbstract_ind' :=  Induction for NonAbstractClass Sort Prop.         
    

Lemma bigger : forall (c:Class)(p p':Property),
 sizeC c < sizeC (instantiate
(ToNonAbstract c) p p').
intros;simpl.
Require Import Omega.
omega.
Qed.


Lemma No_loop : forall c : Class, forall p p' : Property, instantiate
(ToNonAbstract c) p p' <> c.
Proof.
intros c p p' e.

 generalize (bigger c p p'); rewrite e; omega.
Qed.