The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hi,

On 13/12/2010 16:04, Carsten Varming wrote:
> 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.

Thank you for this answer.

I tried to adapt your fix to the complete case, and now it works in the 
trivial cases. However, I still have issues each time the type of the 
arguments does not fit exactly the one I declared for the morphism. Here 
is a new reduced example of my problem.

Since (sort' (str_str' T)) and sort T are convertible, why does the 
resolution fail ?

Cheers,
--
Cyril Cohen
Require Import Relation_Definitions Setoid Morphisms.

Variable A : Type.

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

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

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

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

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

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

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

Print HintDb typeclass_instances.

Goal forall (T : str) (a b : T), eqT _ a b -> eqT _ (op _ a) (op _ b).
Proof.
intros T a b eab.
rewrite eab. (* success *)
Abort.


Goal forall (T : str) (a b : T), eqT _ a b -> eqT _ (op _ (op' _ a)) (op _ 
(op' _ b)).
Proof.
intros T a b eab.
rewrite eab. (* success *)
Abort.

Goal forall (T : str) (a b : T), eqT _ a b -> eqT _ (op' _ (op _ a)) (op' _ 
(op _ b)).
Proof.
intros T a b eab.
rewrite eab. (* fail *)
Abort.