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, inGoal 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
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
- [Coq-Club] Version of [rewrite] that searches by convertibility rather than exact pattern matching?, Jason Gross, 07/12/2012
- Re: [Coq-Club] Version of [rewrite] that searches by convertibility rather than exact pattern matching?, Enrico Tassi, 07/12/2012
Archive powered by MHonArc 2.6.18.