是否可以在 Ltac-match 中绑定不同的术语？

Question

match goal with当在用户定义的策略中进行模式匹配（with ）时，我们可以使用?x绑定一个 Gallina term，以便稍后我们可以引用它。我们可以在一个子句中使用多个这样的标识符 ( ... ?x ... ?y ...)，甚至可以使用相同的标识符 ( ... ?x ... ?x ...) 来指示为了使子句匹配，相同的 Gallina 术语必须出现在这两个位置中。在某种程度上，这限制了与“相同性”要求的可能匹配。这很方便，但如果还能够提出“不同”的要求，那就更方便了（原文如此）。有没有一种方法可以编写形式的匹配子句，其中我们要求和... ?x ... ?y ...所约束的术语是可区分的？?x?y

我所说的可区分并不一定意味着不相等，而只是不同（它们的名称[或表示]不一致）。例如，假设我有两个术语a,b:C。从我们可以证明命题 的意义上来说，这两个术语可能是相等的a = b，但这与我的目的无关。彼此的区别在于它们的名称a不同。b

?x那么，我可以通过提出两个元变量和?y必须绑定不同术语的要求来进行模式匹配吗？

为了将其置于某种上下文中，假设我们已经定义了对、投影和 letR是某种（适当类型的）二元关系。假设我以某种方式最终得到以下两个假设。

H  : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a

我希望能够在我的策略中编写一个仅匹配H而不匹配的匹配子句H'。有什么窍门吗？

如果没有办法只匹配H，那么也许我可以匹配两者，我绑定a到?x和c（或再次a）到?y。但是，然后，在匹配子句的右侧，我想在和 之间执行一些“它们不同吗？ ”检查，以防两者绑定字面上相同的术语。xyidtac

Answer 1

有几种策略可以检查两项是否相等。

我认为你可以将它与tryif或assert_fails做你想做的事情。

match goal with
  | [H : ... |- _] => tryif (constr_eq x y) then fail else some_tactic
end.