The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I was wondering if there's a version of [change] that requires only equality, rather than convertibility, or a version of [subst] that applies to terms and not just identifiers?  [change] only works when the terms are convertible, and [subst] only works if one them is an identifier.  I wrote a version myself (see below), but I'm wondering if there's something that does this in Coq, already.  Thanks.

(* equivalent to [change x with y], but requires that [x = y] be provable with [taceq],

   rather than that [x] and [y] are convertible *)

Tactic Notation "generalized_change" constr(x) "with" constr(y) "by" tactic(taceq) :=

  let xeqy := fresh in

    assert (xeqy : x = y) by (taceq || symmetry; taceq);

      let x' := fresh in

        pose x as x';

          let xeqx' := fresh in

            let x'eqy := fresh in

              assert (xeqx' : x = x') by reflexivity;

                change x with x';

                  assert (x'eqy : x' = y) by (transitivity y; exact xeqy || symmetry; exact xeqy || trivial);

                    clear xeqx';

                      clearbody x';

                        subst x';

                          clear xeqy.

-Jason