确保两个元变量不统一到相同的结果

Question

我正在尝试编写一种策略，它会自动找出基于 Setoid 的假设中的不一致之处。

例如，如果我有以下假设，

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

我希望能够通过 exfalso、apply、transitivity 和 symmetry 的某种组合来解决这个问题。使用此策略时：

  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 和 eq2 将绑定到相同的假设。有什么方法可以确保 ?X 和 ?Y 统一到不同的变量？

Answer 1

我相信 eq1 和 eq2 绑定到同一个假设这一事实不是问题，因为 match 在选择失败分支时回溯。这是一个实现类似目标的证明，其中 setoid 等式被莱布尼茨等式取代：

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.

请注意，这也可以写成更紧凑的形式：

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.

编辑

如果你绝对想尽早防止重叠匹配，你也可以使用fail策略强制回溯：

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.

如果 Coq 将 eq1 和 eq2 绑定到同一个假设，则第三个 match 的第一个分支将激活并调用 fail 1。这具有在第二个最近的回溯点中选择下一个分支的效果——在本例中，secondmatch，它绑定 eq2。运行此代码在响应缓冲区中打印两个不同的假设名称。

（如果将 fail 1 替换为 fail 0（或简单地 fail），Coq 将改为选择最近回溯点的下一个分支，即第三个 match。因为下一个分支接受所有值，所以无论如何它都会运行 idtac eq1 eq2，在我的机器上最终打印 H0 H0。）

请注意，在您的示例中，您还可以同时匹配 eq1 和 eq2 以防止它们相等。例如，以下试图强制实现相等的代码片段失败了：

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. *)

确保两个元变量不统一到相同的结果

Ensuring two metavariables aren't unified to the same result

coq

coq-tactic