当用户定义的策略中的模式匹配(与match goal with)时，我们可以使用?x绑定 Gallina 项，以便以后我们可以引用它。我们可以在一个子句(... ?x ... ?y ...)中使用多个这样的标识符，或者我们甚至可以使用相同的标识符(... ?x ... ?x ...)来表示为了使子句匹配，相同的加利纳项必须出现在这两个位置。 在某种程度上，这限制了可能与"相同"要求的匹配。这很方便，但能够提出"不同"的要求会更方便(原文如此)。有没有办法编写形式... ?x ... ?y ...的匹配子句，其中我们要求受?x和?y约束的术语是可区分的？
我所说的可区分并不一定意味着不相等，而只是不同(它们的名称[或表示]不一致)。例如，假设我有两个术语a,b:C。这两个项可能是相等的，因为我们可以证明命题a = b，但这与我的目的无关。a和b彼此区别在于它们的名字不同。
那么，我可以通过提出两个元变量?x和?y必须绑定不同项的要求来进行模式匹配吗？
为了把它放在某个上下文中，假设我们已经定义了对，投影，并R成为一些(适当类型的)二进制关系。假设我不知何故在我的假设中以以下两个结束。
H : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a
我希望能够在我的策略中编写一个匹配子句，该子句只会匹配H而不是H'。有什么诀窍吗？
如果没有办法只匹配H，那么也许我可以同时匹配两者，我将a绑定到?x，c(或再次a)绑定到?y。但是，在匹配子句的右侧，我想在x和y之间执行一些">它们不同吗？"检查，并在两者绑定字面上相同的术语的情况下idtac。
有几种策略可以检查两个项是否相等。
我认为你可以把它与tryif或assert_fails结合起来，做你想做的事。
match goal with
| [H : ... |- _] => tryif (constr_eq x y) then fail else some_tactic
end.