The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I have more questions about 'rewrite' tactics. Here is an artificial example, which illustrates what I am trying to do. I need to rewrite a part of an _expression_ under Leibnitz equality.

Require Import Coq.Program.Basics.

Require Import Coq.Program.Combinators.

Require Import Coq.Setoids.Setoid.

Unset Printing Notations.

Lemma Foo

      {A:Type}

      (f0 f1 f2 f3 f4: A->A)

  :

    compose f1 (compose f2 (compose f3 f4))  =

    compose f1 (compose (compose f2 f3) f4).

Proof.

  intros.

  (* I know, `using reflexivity` works here, but I want to prove by rewriting *)

  (* The following does not work. Error: Tactic failure: Nothing to rewrite. *)

  try rewrite <- compose_assoc at 2.

  (* However, the following works OK. *)

  replace (compose f2 (compose f3 f4)) with (compose (compose f2 f3) f4)

    by apply compose_assoc.

  reflexivity.

Qed.

The equation I am working with are actually much more elaborate than one above, and rewriting parts of it using 'replace' makes my proofs difficult to read.I have to copy-paste ~100 line expressions into 'replace' arguments.

I would love to be able to rewriting positionally, using something like 'rewrite lemma at 2.' If standard rewrite tactics, does not allows this, perhaps it could be automated somehow?

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060