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: May 31 2023 at 03:30 UTC