Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Version of [rewrite] that searches by convertibility rather than exact pattern matching?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Version of [rewrite] that searches by convertibility rather than exact pattern matching?


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Version of [rewrite] that searches by convertibility rather than exact pattern matching?
  • Date: Wed, 11 Jul 2012 19:34:12 -0400

Hi,
Is there a version of rewrite that pattern matches based on convertibility rather than syntactic equality?  The problem that I'm running in to is that, in
Goal forall A (a a' : A), id a = id a' -> a = a'.
      intros A a a' H.
      (* rewrite H. *) (* fails *)
      exact H.

the [rewrite H] fails.  Sometimes, [simpl in *] isn't a good solution, because I've made opaque constants so that I can pattern match on them (and if they were transparent, then [simpl] destroys the information that I need to easily do pattern matching). I can write a tactic like
Ltac generalized_rewrite H :=
      match type of H with
        | ?a = _ => match goal with
                      | [ |- appcontext[?a'] ] => change a' with a; rewrite H
                    end
      end.

but I think this tends to be slow when the goal is large.  Does anyone have a better solution?

Thanks.

-Jason



Archive powered by MHonArc 2.6.18.

Top of Page