The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a variant of [change _ with _ in *] that does not fail if [change _ with _ in H] fails for some particular hypothesis, but succeeds for all the other ones?  I've constructed a tactic that has the behavior I want, but it seems somewhat hacky, and I'm wondering if anyone has or knows of a better solution.  The first two [change] attempts in the following code fail, while the third one has the tactic I made/the behavior I'm looking for.  Thanks.

Definition first (a b : Type) := a.

Goal forall a b c d (a' := first a b) (b' := first c d), a = b -> False.

  intros.

  (* change a with (first a' a) in *. *) (* Error: Cannot create self-referring hypothesis a' *)

  (* repeat match goal with

           | [ H : _ |- _ ] => progress change a with (first a' a) in H |- *

         end. *) (* loops forever *)

  Local Ltac do_for_each_hyp' tac fail_if_seen :=

    match goal with

      | [ H : _ |- _ ] => fail_if_seen H; tac H; try do_for_each_hyp' tac ltac:(fun H' => fail_if_seen H'; match H' with | H => fail 1 | _ => idtac end)

    end.

  Local Ltac do_for_each_hyp tac := do_for_each_hyp' tac ltac:(fun H => idtac).

  change a with (first a' a); do_for_each_hyp ltac:(fun H => change a with (first a' a) in H).

-Jason