The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Here is a script to illustrate Abhishek's reply.

Require Coq.Setoids.Setoid.

Goal forall A B C:Prop, (B<->C) -> C /\ A -> B /\ A.
Proof.
  intros * H1.
  rewrite H1.
  exact (fun x => x).

Qed.

The so-called "setoid rewriting" mechanism can be extended with arbitrary relation (preferably transitive and reflexive ones). The documentation is here: [ http://coq.inria.fr/refman/Reference-Manual029.html ]. But you may want to take it one step at a time.

The [apply] tactic can work with equivalences too, if you want a less involved mechanism:

Goal forall A B C:Prop, (B<->C) -> C /\ A -> B /\ A.
Proof.
  intros * H1.
  intros [H2 H3].
  split.
  + apply H1.
    assumption.
  + assumption.
Qed.

/Arnaud Spiwack

On 21 September 2014 18:03, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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.)