The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

The following code type-checks, and seems to be approximately what you want, though I don't think it actually works (the coercion statements give, e.g., " Warning: POL does not respect the uniform inheritance condition " and the [exact x] on the last line gives "Anomaly: apply_coercion. Please report."  I'll report this bug, if it's not already in the bug tracker, momentarily.):

Definition Concept := Type.

Definition PrimitiveType : Concept := Type.

Definition RelationType : Concept := Type.

Definition PartOf (A B:PrimitiveType) : RelationType := prod A B.

Definition ContainedIn (A B:PrimitiveType) : RelationType := prod A B.

Definition HasLocation (A B:PrimitiveType) : RelationType := prod A B.

Axiom SR1 : forall (A B:PrimitiveType), ContainedIn A B ->  PartOf A B.

Coercion SR1 : ContainedIn>->  PartOf.

Parameters A B : PrimitiveType.

Definition POL(p:PartOf A B) := fst p.

Coercion POL : PartOf >-> A.

Definition POR(p:PartOf A B) := snd p.

Coercion POR : PartOf >-> B.

Goal forall x : PartOf A B, A.

  intro x. exact x.

My first guess would be that Coq wants a definite target class for coercions, and doesn't like coercions to arbitrary/unspecified types.  This seems to be supported by what  http://coq.inria.fr/doc/Reference-Manual023.html says about the uniform inheritance condition.

I hope this helps.

-Jason

On Sun, Jun 24, 2012 at 4:25 AM, Richard Dapoigny <richard.dapoigny AT univ-savoie.fr> wrote:

Hi,
We are actually thinking about a type-theoretical model of ontologies which uses parameterized coercions. However, we get the error "Cannot find the target class." with the following Coq code:

Definition Concept := Type.
Definition PrimitiveType : Concept := Type.
Definition RelationType : Concept := Type.

Definition PartOf (A B:PrimitiveType) : RelationType := prod A B.
Definition ContainedIn (A B:PrimitiveType) : RelationType := prod A B.
Definition HasLocation (A B:PrimitiveType) : RelationType := prod A B.

Axiom SR1 : forall (A B:PrimitiveType), ContainedIn A B ->  PartOf A B.
Coercion SR1 : ContainedIn>->  PartOf.

Coercion POL(A B:PrimitiveType)(p:PartOf A B) := fst p. (*<- error *)
Coercion POR(A B:PrimitiveType)(p:PartOf A B) := snd p. (*<- error *)

In fact when I put "A" instead of fst p, it works but it is not the semantically expected result. If someone has an idea of how to solve this problem?

Thanks in advance,
Richard

--
And the wounded skies above say
it's much too much too late.
Well, maybe we should all be praying for time.