coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]morphisms and modules, Aaron Bohannon
Archive powered by MhonArc 2.6.16.