The Coq mailing list

[Coq User <coquser AT googlemail.com>]

Can you give an example?

On Tue, Aug 25, 2009 at 10:16 PM, Tom Harke <harke AT cs.pdx.edu> wrote:

It appears that in 1 of the 3 branches you're packaging up an Object
as a SpecialObject, then in the other 2 branches the first thing you do
is unpackage it to get an Object again.  Granted, the unpacking is implicit
since you've got a coercion.  You can refactor this code to eliminate
the packing/repacking in the corecursive call, using a worker/wrapper
transformation, in which case my suggestion of using Object appears to be
appropriate.  After finishing the corecursive "worker", use Definition
for a simple "wrapper" converting the Object to the SpecialObject (with
the name "someString").

Again, this type-checks, and it meets your revised specification,
but it's hard to answer such problems if you don't tell us what
you're trying to do, and you leave irrelevant code in the example.

I chose my wording poorly ... when I read the definition of SpecialObject
I ignored the CoInductive keyword since there is no recursion in the definition
and so, IIUC, calling it CoInductive doesn't do much.  Perhaps an expert
could explain this more coherently.

On Tue, Aug 25, 2009 at 08:16:10PM +0100, Coq User wrote:
> But SpecialObject is Coinductive.  I've changed Singleton to be Coinductive
> and the problem is still there.  I need singleton:SpecialObject as opposed
> to singleton:Object.
>
> Require Import String.
> Require Import List.
>
> Section Example.
>
> (*Encoding of the Standard Example MetaModel*)
> (*Top*)
> CoInductive Top:Set :=
> | Build_Top (name:string)
> with
> Object:Set :=
> | Build_Object (features:list Feature)(super:Top)
> with
> Feature:Set :=
> | Build_Feature (superfeat:Top)(featOwningObject:Object)
> .
> (*SpecialObject*)
> CoInductive SpecialObject:Set :=
> | Build_SpecialObject (info:string)(superObj:Object)
> with
> Singleton:Set :=
> Build_Singleton (superSingleton:SpecialObject).
>
> (*Singleton Functions*)
> (*Top Functions*)
> Definition superSingleton:Singleton -> SpecialObject:=
>      (fun d:Singleton =>
>          match d with
>          | (Build_Singleton sup) =>sup
>          end).
> Coercion superSingleton:Singleton >-> SpecialObject. (*Type Coercion*)
>
> (*Top Functions*)
> Definition name:Top -> string:=
>      (fun d:Top =>
>          match d with
>          | (Build_Top elName) => elName
>          end).
>
> (*Object Functions*)
> Definition features:Object -> list Feature:=
>      (fun d:Object =>
>          match d with
>          | (Build_Object feats sup) => feats
>          end).
> Definition super:Object -> Top:=
>      (fun d:Object =>
>          match d with
>          | (Build_Object feats sup) => sup
>          end).
> Coercion super : Object >-> Top. (*Type Coercion*)
>
> (*Feature Functions*)
> Definition featOwningObject:Feature -> Object:=
>      (fun d:Feature =>
>          match d with
>          | (Build_Feature sup p) => p
>          end).
> Definition superfeat:Feature -> Top:=
>      (fun d:Feature =>
>          match d with
>          | (Build_Feature sup p) => sup
>          end).
> Coercion superfeat : Feature >-> Top. (*Type Coercion*)
>
> (*SpecialObject Functions.*)
> Definition info:SpecialObject -> string:=
>      (fun d:SpecialObject =>
>          match d with
>          | (Build_SpecialObject inf sup) => inf
>          end).
> Definition superObj:SpecialObject -> Object:=
>      (fun d:SpecialObject =>
>          match d with
>          | (Build_SpecialObject inf sup) => sup
>          end).
> Coercion superObj : SpecialObject >-> Object.
>
>
>
>
> (*Instantiaing a SpecialObject is where the error occurs.*)
>
> (*SpecialObject Metamodel Instance*)
> CoFixpoint singleton:SpecialObject :=
>     Build_Singleton (*Several Levels of Inheritance*)
>     (   (*Supertype of Singleton*)
>         Build_SpecialObject "someString"
>         (
>            Build_Object (*Supertype of SpecialObject*)
>            (featureOne::featureTwo::nil) (*List of related Example Feature*)
>            (
>                Build_Top (*Supertype of Object*)
>                "singleton" (*Name.*)
>            )
>        )
>     )
> with
> featureOne:Feature :=
>     (
>         Build_Feature
>         (
>             (Build_Top (*Supertype of Feature*)
>             "featureOne" (*Name.*)
>             )
>
>          ) singleton
>      ) (*Object that owns the Feature *)
> with
> featureTwo:Feature :=
>     (
>         Build_Feature(
>           Build_Top (*Supertype of Feature*)
>           "featureTwo" (*Name.*)
>         )
>      )
>      singleton (*Object that owns the Feature*)
> .
> End Example.
>
>
>
>
> On Tue, Aug 25, 2009 at 7:04 PM, Tom Harke <harke AT cs.pdx.edu> wrote:
>
> > When you use CoFixpoint the result type must be CoInductive.
> > So, I can get your example to check if I change
> > > CoFixpoint singleton:SpecialObject :=
> > to
> > > CoFixpoint singleton:Object :=
> > though I don't know if this is what you want.
> >