The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

  I've got some problem trying to use rewrite in some deep occurrence 
of a subterm.

 In the following example (attached file), the rewrite fails, whilst an 
iterated application
of op_m succeeds. What is failing in the class declaration for having a 
"rewrite H" ok ?

Pierre





Require Import Relations.

Require Import Setoid Morphisms.

Class SemiGroup (A:Type) :={
 _eq : A -> A -> Prop;
 op : A -> A -> A;
 neutral : A ;
 op_equiv :> Equivalence _eq;
 op_comm : forall x y:A, _eq (op x y) (op y x);
 op_assoc : forall x y z:A, _eq (op x (op y z)) (op (op x y) z);
 n_def : forall x, _eq (op neutral x) x;
 op_m : Morphism (_eq ==> _eq ==> _eq) op
}.

Lemma Essai `(SemiGroup A) : forall a b c d e, _eq a b ->
                                             _eq (op (op (op a c) d) e)
                                                 (op (op (op b c) d) e).
Proof.
 intros A SG a b c d e H. 
  (*
  
  rewrite H. (* fails *)

  *)
 repeat apply op_m; try reflexivity;assumption.
Qed.