The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

rewrite can be made to work for other relations.

If you try rewrite H1, the error message will ask you to add the following line above:

Require Coq.Setoids.Setoid.

Then rewrite H1 will do exactly what you wanted.

You can read chapter 3 of the following article to understand how the rewrite functionality can be extended for arbitrary (Prop valued) relations in arbitrary contexts.

http://www.labri.fr/perso/casteran/CoqArt/TypeClassesTut/typeclassestut.pdf

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sun, Sep 21, 2014 at 11:51 AM, Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com> wrote:

Hi,

In the standard library (theories/Init/Logic.v), there is this:

  Theorem and_cancel_l : forall A B C : Prop,
    (B -> A) -> (C -> A) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
  Proof.
    intros; tauto.
  Qed.

As part of the exercise, I have tried to create a corresponding proof-script without automation.

At one point, I was in this state:

  1 subgoal
  A : Prop
  B : Prop
  C : Prop
  H1 : B <-> C
  ______________________________________(1/1)
  C /\ A -> B /\ A

and yearned to make the following step:

        replace all occurrences of "B" with "C" (this step is justified by "H1 : B <-> C"

and find myself here:

  1 subgoal
  A : Prop
  B : Prop
  C : Prop
  H1 : B <-> C
  ______________________________________(1/1)
  C /\ A -> C /\ A

Is there a tactic that would allow me/us to do this kind of step?
(just like as we can take advantage of equalities by "rewrite" tactics.)