coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: AUGER Cédric <sedrikov AT gmail.com>
- Cc: Richard Dapoigny <richard.dapoigny AT univ-savoie.fr>, coq-club AT inria.fr
- Subject: Re: [Coq-Club] Exception
- Date: Sat, 10 Nov 2012 19:32:02 -0500
As I understand it, [Class Foo := Bar :> Baz] is shorthand for
Class Foo := Bar.
Coercion Bar : Foo >-> Baz.
(or [Foo >-> Funclass] or [Foo >-> Sortclass], if [Baz] is a sort or a function type.)
Disclaimer: I haven't read the source-code of Coq.
-Jason
On Sat, Nov 10, 2012 at 2:54 PM, AUGER Cédric <sedrikov AT gmail.com> wrote:
Le Sat, 10 Nov 2012 19:43:50 +0100,
Richard Dapoigny <richard.dapoigny AT univ-savoie.fr> a écrit :
I am not used to ':>' annotations.
> Hi,
> With the following code fragment:
> (* Basic universes *)
> Definition Universal := Type.
> Definition Concept : Universal := Type.
> Definition Association : Universal := Type.
> Definition OntoType(c:Type) := Type.
> Definition OntoDomain(c:Type) := Type.
>
> Parameter Relation : (OntoType Concept) -> (OntoType Concept) ->
> Prop.
>
> Structure PT : OntoType Concept := {}.
> Structure PD : OntoType PT := {PDsub :> PT}.
> Structure ED : OntoType PT := {EDsub :> PT}.
> Structure AB : OntoType PT := {ABsub :> PT}.
> Structure R : OntoType AB := {Rsub :> AB}.
> ...
>
> Class RelOnto (X Y:OntoType Concept) : Association :=
> { RelOnto_prop : Relation X Y}.
>
> Class Reflexive : Prop :=
> Reflexivity : forall X:OntoType Concept, Relation X X.
>
> Class Irreflexive : Prop :=
> Irreflexivity : forall (X Y:OntoType Concept), ~Relation X
> X.
>
> Class Antisymmetric : Prop :=
> Antisymmetry : forall (X Y :OntoType Concept), Relation X
> Y -> Relation Y X -> X = Y.
>
> Class Asymmetric : Prop := {
> Asym_Irr :> Irreflexive ;
> Asym_Anti :> Antisymmetric}.
>
> Class Transitive : Prop :=
> Transitivity : forall X Y Z:OntoType Concept, Relation X
> Y -> Relation Y Z -> Relation X Z.
>
> Class POR : Prop := {
> POR_R :> Reflexive ;
> POR_AS :> Antisymmetric ;
> POR_T :> Transitive }.
>
> Class PartOf {X Y:OntoType Concept} : Prop := {
> PartOf_s :> RelOnto X Y;
> PartOf_p :> POR }.
> ============================================
> I got the following error:
> "Anomaly: Uncaught exception Option.IsNone. Please report.Compilation
> output:
> File "C:\Users\Richard\Desktop\Documents\Coq-programs/JLComp1.v",
> line 73, characters 0-123:
>
> Anomaly: Uncaught exception Option.IsNone. Please report."
> If anyone has an explanation...
> Thanks in advance,
> Richard
>
>
>
>
Some remarks:
→ replacing :> with : works at this place (PartOf_s)
→ changing the type of RelOnto to return 'Type' and not 'Association'
works
PartOf_s is a little strange as it is a Type as part of a Prop.
That is no projection can be defined.
PartOf_s : ∀ X Y, (PartOf X Y : Prop)
→ (RelOnto X Y : Association (*=Type*))
is thus illegal.
I do not know how ':>' really works. If it is just a simple projection
definition followed by adding a rule to search automatically an
instance, that can explain your bug: it tries to turn a non-existing
projection into an instance. Some hack may have been done to allow
replacing Association with Type, but forgot to deal with more complexes
Type universes.
- [Coq-Club] Exception, Richard Dapoigny, 11/10/2012
- Re: [Coq-Club] Exception, AUGER Cédric, 11/10/2012
- Re: [Coq-Club] Exception, Jason Gross, 11/11/2012
- Re: [Coq-Club] Exception, AUGER Cédric, 11/10/2012
Archive powered by MHonArc 2.6.18.