The Coq mailing list

[anoun AT labri.fr]

Hi,
I'm using the setoid theory in my development and I found some problems to
define  morphisms
In what follows, I will illustrate this problem in a simpl example:

Require Import Setoid.
Require Import Arith.
Require Import Relations.
Require Import Compare_dec.
Require Import ArithRing.
Require Import Omega.
Set Implicit Arguments.


(* We represent integers as pairs of Peano numbers *)

Delimit Scope Z'_scope with Z'.

Open Scope Z'_scope.


Inductive Z' : Set :=
 mkZ' : nat -> nat -> Z'.


(* The equivalence relation on Z' *)

Definition  Z'eq (z z':Z') :  Prop :=
 let (a, b) := z in
   let (c, d) := z' in  a + d = b + c.

Notation "a =Z= b" := (Z'eq a b)  (at level 70): Z'_scope.
(* Z'eq is an equivalence relation *)

Lemma Z'eq_refl : reflexive Z' Z'eq.
Admitted.

Lemma Z'eq_sym : symmetric _ Z'eq.
Admitted.

Lemma Z'eq_trans : transitive _ Z'eq.
Admitted.

(* We can now build a setoid *)

Theorem Z'oid : Setoid_Theory _ Z'eq.
  split.
 exact Z'eq_refl.
 exact Z'eq_sym.
 exact Z'eq_trans.
Qed.


Add Setoid Z' Z'eq Z'oid as Z'_register.

We define now an inductive predicate Z'pos for positive integers:
If we consider that the predicate is defined within the sort Prop, we will be
able to add it as a morphism without any problem

Inductive Z'pos : Z' -> Prop :=
mkpos : forall (a b:nat), b < a -> Z'pos (mkZ' a b).


Add Morphism Z'pos : pos_morph.
destruct x1.
destruct x2.
simpl.
split;
 inversion 1;split;omega.
Qed.


this is because the compatibility lemma (pos_morph) generated is the 
following:
forall (z1 z2:Z'), z1=Z=z2 ->Z'pos z1 <->Z'pos z2.

But if we define our predicate in sort Type (or Set), we will be unable to 
prove
the compatibility lemma associated

Inductive Z'pos2 : Z' -> Type :=
mkpos2 : forall (a b:nat), b < a -> Z'pos2 (mkZ' a b).


Add Morphism Z'pos2 : pos_morph2.
???
The compatibility lemma in this case uses the leibnitz equality as an
equivalence relation on Type.
forall (z1 z2:Z'), z1=Z=z2 ->Z'pos2 z1 =Z'pos2 z2.

I need to add inductives predicates defined within sort Set as morphisms but 
as
we saw below this is not possible using the cvs version of Coq
How can we solve that?
Is it possible to modify the type of the generated lemma by replacing leibnitz
equality by another equivalence relation on sort Set (e.g. eqSet which 
reflects
the <-> of Prop??)
Inductive eqSet(A B:Set):Set:=
|mk_eq_set:(A->B)->(B->A)->eqSet A B.

Thanks a lot in advance for your answers and comments
Regards,
Houda

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.