When pattern matching (with match goal with) in a user-defined tactic, we can use ?x to bind a Gallina term, so that later we can refer to it. We can use several such identifiers in one clause (... ?x ... ?y ...) or we can even use the same identifier (... ?x ... ?x ...) to indicate that in order for the clause to match, the same Gallina term must appear in those two positions. In a way, this constraints the possible matches with a "sameness" requirement. That's handy, but it would be handier (sic) to also be able to pose a "different" requirement. Is there a way to write a match-clause of the form ... ?x ... ?y ... where we require that the terms bound by ?x and ?y are distinguishable?
By distinguishable I don't necessarily mean not-equal, but just different (their names [or representations] don't coincide). For example, say I have two terms a,b:C. The two terms might be equal in the sense that we can prove the proposition a = b, but that's irrelevant for my purposes. What makes a and b distinguishable from each other is that their names are different.
So, can I pattern-match by posing a requirement that two meta-variables ?x and ?y must bind different terms?
To put this in some context, say we have defined pairs, projections and let R be some (appropriately typed) binary relation. Suppose I somehow end up with the following two in my assumptions.
H : R (proj1 (pair a b)) c
H' : R (proj1 (pair a b)) a
I would like to be able to write a match-clause in my tactic that will only match H and not H'. Is there a trick for that?
If there is no way to only match H, then perhaps I could match both, where I bind a to ?x and c (or again a) to ?y. But then, on the right-hand-side of the match-clause I would like to perform some "are-they-different?" check between x and y and do idtac in case the two bind literally the same terms.
There are several tactics to check whether two terms are equal.
I think you can combine it with tryif or assert_fails to do what you want.
match goal with
| [H : ... |- _] => tryif (constr_eq x y) then fail else some_tactic
end.