Ensuring two metavariables aren't unified to the same result

Question

I'm trying to write a tactic which will automatically pick up inconsistencies in Setoid-based hypotheses.

For instance, If I have the following hypotheses,

  H1 : x == y
  H2 : z == y
  H3 : x =/= z

I would like to be able to solve this with some combination of exfalso, apply, transitivity, and symmetry. When using this tactic:

  match goal with
    [ eq1 : ?X == ?Z |- _ ] =>
    match goal with
      [ eq2 : ?Y == ?Z |- _ ] =>
        match goal with
          [ eq3 : ?X =/= ?Y |- _ ] => exfalso; apply eq3; [...]

        end
    end
  end.

eq1 and eq2 will be bound to the same hypothesis. Is there any way to ensure that ?X and ?Y are unified to distinct variables?

Answer 1

I believe that the fact that eq1 and eq2 are bound to the same hypothesis is not a problem, because match backtracks when it chooses a failing branch. Here is a proof that discharges a similar goal, with setoid equality being replaced by Leibniz equality:

Lemma test T (x y z : T) : x = y -> z = y -> x <> z -> False.
Proof.
intros.
match goal with
| eq1 : ?X = ?Y |- _ =>
  match goal with
  | eq2 : ?Z = ?Y |- _ =>
    match goal with
    | eq3 : ?X <> ?Z |- _ => destruct (eq3 (eq_trans eq1 (eq_sym eq2)))
    end
  end
end.
Qed.

Note that this could also have been written in a more compact form:

Lemma test T (x y z : T) : x = y -> z = y -> x <> z -> False.
Proof.
intros.
match goal with
| eq1 : ?X = ?Y,
  eq2 : ?Z = ?Y,
  eq3 : ?X <> ?Z |- _ => destruct (eq3 (eq_trans eq1 (eq_sym eq2)))
end.
Qed.

Edit

If you absolutely want to prevent overlapping matches early, you can also use the fail tactic to force backtracking:

Lemma test T (x y z : T) : x = y -> z = y -> False.
Proof.
intros.
match goal with
| eq1 : ?X = ?Y |- _ =>
  match goal with
  | eq2 : ?Z = Y |- _ =>
    match Z with
    | X => fail 1
    | _ => idtac eq1 eq2
    end
  end
end.
Abort.

If Coq binds eq1 and eq2 to the same hypothesis, the first branch of the third match will activate and call fail 1. This has the effect of choosing the next branch in the second-closest backtracking point -- in this case, the second match, which binds eq2. Running this code prints two different hypothesis names in the response buffer.

(If you replace fail 1 by fail 0 (or simply fail), Coq will instead choose the next branch of the closest backtracking point, which is the third match. Since the next branch accepts all values, it will run idtac eq1 eq2 no matter what, which on my machine ends up printing H0 H0.)

Note that in your example, you could have also matched eq1 and eq2 simultaneously to prevent them from being equal. For instance, the following snippet, which tries to force this equality, fails:

Lemma test T (x y z : T) : x = y -> z = y -> False.
Proof.
intros.
match goal with
| eq1 : ?X = ?Y,
  eq2 : ?Z = ?Y |- _ =>
    match Z with
    | X => idtac eq1 eq2
    end
end.
Abort.

(* Error: No matching clauses for match. *)