Stream: Coq users

Topic: Recreating unification of apply and rewrite

view this post on Zulip Patrick Nicodemus (Oct 19 2022 at 15:55):

I am trying to figure out how to write something analogous to the first order unification done by apply and rewrite, for slightly different purposes.

I have a theorem of the form \forall x, A x = B x
and my goal is of the form P(A(t)). I am trying to get hold of the equality A(t) = B(t) that would come from specializing x to t.
Ideally I am looking for an approach that would still work even if the left hand side of the given equality only agrees with a subterm of the goal up to convertibility, not strict syntactic equality

Last updated: Sep 28 2023 at 11:01 UTC