The Coq mailing list

[Carsten Varming <varming AT cmu.edu>]

Hi,

The main problem is with the type class resolution. The type of eqT in the 
morphism declaration is (sort T), but the resolution algorithm is looking 
for (sort' (str_str' T)), and it doesn't know that (sort T) and
(sort' (str_str' T)) are equal.

Below I have changed the definition of your morphism such that it works.

Carsten Varming

Require Import Relation_Definitions Setoid Morphisms.

Variable A : Type.

Structure str := Str { sort :> Type }.

Structure str' := Str' { sort' :> Type }.
Definition str_str' (T : str) := Str' T.

Variable eqT : forall T : str, T -> T -> Prop.
Variable op : forall T : str', T  -> bool.

Add Parametric Relation (T : str) : T (eqT T)
  reflexivity proved by _
  symmetry proved by _
  transitivity proved by _ as eqT_rel.
Proof. Admitted.

Set Printing All.

Add Parametric Morphism (T : str) : (op (str_str' T))
with signature ((@eqT _ : sort' (str_str' T) -> _ -> _) ==> @eq _)%signature 
as eqT_op.
Admitted.

(* Here comes the problem *)
Goal forall (T : str) (a b : T), eqT _ a b ->
  op (str_str' T) b = true -> op (str_str' T) a = true.
Proof.
intros T a b eab ob.
rewrite -> (eab). (* <= it doesn't work *)
Abort.



On Mon, 13 Dec 2010, Cyril Cohen wrote:

> On 13/12/2010 15:16, Cyril Cohen wrote:
> > I managed to reduce my issue to the joint example.
>
> I'm sorry, I just noticed that I didn't even need to put canonical 
> structures. Here is the new example.