Patrick Nicodemus (Nov 06 2022 at 23:27): Patrick Nicodemus (Nov 06 2022 at 23:27):I have a few situations where I need a tactic that behaves very slightly different than apply or rewrite.
I was thinking I could write this in Ltac or Ltac2 using the pattern matching features in there. But I don't know how to emulate the behavior of apply and rewrite on quantified hypotheses forall x : A, B(x) -> t(x) = s(x).
For a concrete example I want to write an Ltac function that takes a hypothesis forall x1 : A1, forall x2 : A2(x1), ... forall xn : An(x1,.... n-1), t(x1.... xn) = s(x1.... xn) and checks to see if t(x1.... xn) can be unified with a subterm of the goal, and if so, return the list of instantiations (x1 := a1, ... xn := an).
(My specific motivation is that I have very large terms and the setoid rewrite typeclass unification is very slow. I need to hide or obscure these terms so that the setoid rewrite can perform more efficiently, but I can only do that after I get the unification I need.)
This doesn't sound trivial but I suspect it should be doable with some out of the box unification tools exposed by Ltac or Ltac2, I just don't know exactly what to use. The pattern matching tool in Pattern.v seems useful here but it only accepts patterns with one hole - should I write a recursive algorithm which leverages that to extend to the case of n possibly dependent holes rather than one hole, or is there some function which is more adequate to the purpose?
Last updated: Apr 20 2024 at 15:01 UTC