Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Exception

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Exception


Chronological Thread 
  • 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 :

> 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
>
>
>
>

I am not used to ':>' annotations.
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.




Archive powered by MHonArc 2.6.18.

Top of Page