The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Can someone explain to me why the (e)rewrite in the following fails?  (The ones prefixed with [Fail].)  I'm looking for an explanation that will teach me more about the internals of (e)rewrite, and how they figure out what to rewrite with.

(**)

Set Implicit Arguments.

Reserved Infix "#" (at level 65, left associativity).

Record PreCategory :=

  {

    Object :> Type;

    Morphism : Object -> Object -> Type;

    Identity : forall x, Morphism x x;

    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f # g" := (Compose f g);

    Associativity : forall x1 x2 x3 x4

                           (m1 : Morphism x1 x2)

                           (m2 : Morphism x2 x3)

                           (m3 : Morphism x3 x4),

                      (m3 # m2) # m1 = m3 # (m2 # m1)

  }.

Infix "#" := (@Compose _ _ _ _).

Goal forall (C : PreCategory) (H0 H1 : Object C) (H2 : Morphism C H1 H0)

            (H3 H4 : Object C) (H5 : Morphism C H3 H4) (H6 : Morphism C H4 H1)

            (F0' : Object C -> PreCategory) (H10 : Object (F0' H1))

            (H13 : Object (F0' H3)) (f : Object (F0' H1) -> Object (F0' H0))

            (m' : forall s d : Object C,

                    Morphism C s d -> Object (F0' s) -> Object (F0' d))

            (H16 : Morphism (F0' H0) (m' H3 H0 (H2 # H6 # H5) H13)

                            (m' H3 H0 (H2 # (H6 # H5)) H13))

            (H14 : Morphism (F0' H0) (f (m' H3 H1 (H6 # H5) H13)) (f H10))

            (H15 : Morphism (F0' H0) (m' H3 H0 (H2 # (H6 # H5)) H13)

                            (f (m' H3 H1 (H6 # H5) H13))),

       H14 # H15 # H16 = H14 # (H15 # H16).

Proof.

  intros.

  rewrite (@Associativity _ _ _ _ _ H16 H15 H14). (* succeeds *)

  Undo.

  Fail erewrite Associativity. (* Error: Cannot refine with term

 "eq_ind_r

    (fun _ : Morphism ?81 ?82 ?85 => H14 # H15 # H16 = H14 # (H15 # H16))

    ?207 (Associativity ?81 ?82 ?83 ?84 ?85 ?201 ?202 ?203)"

because a metavariable has several occurrences. *)

  Fail rewrite Associativity. (* Error: Unable to find an instance for the variables p, x1, x2, x3, x4. *)

  (* We can generalize the types of the morphisms, and then it works *)

  repeat match goal with

           | [ |- appcontext[@Compose _ (?f ?x) _ _] ]

             => generalize dependent (f x); intros

           | [ |- appcontext[@Compose _ _ (?f ?x) _] ]

             => generalize dependent (f x); intros

           | [ |- appcontext[@Compose _ _ _ (?f ?x)] ]

             => generalize dependent (f x); intros

         end;

    clear.

  erewrite Associativity. (* success *)

  Undo.

  rewrite Associativity. (* success *)

(**)

Thanks,

Jason