Patrick Nicodemus (Jan 20 2024 at 02:28): Patrick Nicodemus (Jan 20 2024 at 02:28):The documentation says that in a match statement, Ltac2 ?id variables will only bind to closed terms. That makes sense, but then how should we match an open term?
For example, suppose I have forall x : A,N and M which is closed. I want to decide whether M unifies (or is syntactically identical) with N for the appropriate instantation of x. Intuitively the way I would think to do this is by constructing a pattern N[x/?y], where the free variable y is replaced with an Ltac2 variable, and we then try to unify this pattern with M, but this seems incompatible with ?id only binding closed terms as we can't get N[x/?y] easily to begin with.
Patrick Nicodemus (Jan 20 2024 at 17:19):I will give a more concrete example. Say I know forall x. A(x) -> B(x) and I want to write a tactic which replaces all occurrences A with B in the hypothesis. Say I have a hypothesis forall x1 x2... xn, A(t(x1,... xn)) and I want to replace it with forall x1 x2 ... xn, B(t(x1,... xn)). How can I check that A(t(x1,...xn)) is unifiable with A(x) in order to decide which ones I should try this on?
Last updated: Oct 12 2024 at 12:01 UTC