Skip to Content.
Sympa Menu

coq-club - [Coq-Club]morphisms and modules

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]morphisms and modules


chronological Thread 
  • From: "Aaron Bohannon" <bohannon AT cis.upenn.edu>
  • To: "Coq List" <coq-club AT pauillac.inria.fr>
  • Subject: [Coq-Club]morphisms and modules
  • Date: Thu, 9 Nov 2006 14:13:47 -0500
  • Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:message-id:date:from:sender:to:subject:mime-version:content-type:content-transfer-encoding:content-disposition:x-google-sender-auth; b=inXjeoViw2lJHfFM0uBqH07NHoTqcIorpITMUnnCBiEzlBequKw0bfpuVoCrw/G3GFD2JlnxW0pk8dyctg04dzQOudOjkN755VCv8zKh4IcpyrZShH3NUSi/Yhl4TetW1N3/0H2UpWde5Yj2fbgga5QZ2b1qR/9cuok2geUPlqM=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I am observing some strange interactions between modules and morphisms.

First of all, testing whether a relation is "registered" appears to be
a syntactic check that does account for covertability or sharing
constraints indicated by modules, which is a bit of a hassle.

More strange is the following situation.  I have the code:

...
(* Module ASD := Foo (AS).  (* Line 1 *) *)
...
setoid_replace (union X X) with X using relation AS.Equal.  (* Line 2 *)
...

This "setoid_replace" on Line 2 works perfectly when Line 1 is not
executed.  However, by uncommenting Line 1 and changing *nothing* else
in the file, I get the following error message at Line 2:

Error: refiner was given an argument "ASD.MP.FM.EqualSetoid_morphism" of type
"let ASetoidClass :=
   SymmetricReflexive variance (Seq_sym t Equal ASD.MP.FM.Equal_ST)
     (Seq_refl t Equal ASD.MP.FM.Equal_ST) in
 Morphism_Theory (cons ASetoidClass (singl ASetoidClass)) Iff_Relation_Class"
instead of
"Morphism_Theory
   (cons (FM.EqualSetoid Covariant) (singl (FM.EqualSetoid Covariant)))
   (iff_relation tt)"

I suspect this has to do with the fact that a some relations and some
of their morphisms (in my particular case, the ones in FSetFacts),
which were already registered, are being re-registered by this functor
instantiation, and this is causing problems.  But does this mean that
functors declaring morphisms should only ever be instantiated once?
Or is there a way around this?

-Aaron





Archive powered by MhonArc 2.6.16.

Top of Page