The Coq mailing list

[Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 24/06/2012 18:31, Jason Gross a écrit : 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

Dear Jason,
Thanks for your pompt help. In fact, parameterized coercions have been addressed by Z. Luo in some papers but so far, no implementation has been provided. So, perhaps a solution is possible with type classes from M Sozeau. We will investigate this road.
Thanks again.
Richard

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.

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

begin:vcard
fn:Richard Dapoigny
n:Dapoigny;Richard
email;internet:richard.dapoigny AT univ-savoie.fr
tel;work:+33 450 09 65 29
tel;cell:+33 621 35 31 43
version:2.1
end:vcard