coq - coq 将前提“否定不等于”更改为“等于”

Question

假设我有这样的前提：

H2: ~ a b c <> a b c

我希望将其更改为：

a b c = a b c

在哪里

a 是术语 -> 术语 -> 术语

b 和 c 都是 Term

我该怎么做？谢谢！

Answer 1

如果展开 和 的定义~，<>您的假设具有以下类型：

H2: (a b c = a b c -> False) -> False

因此，您希望实现的是逻辑学家通常所说的“双重否定消除”。它不是一个直观可证明的定理，因此在ClassicalCoq 的模块中定义（详见http://coq.inria.fr/distrib/V8.4/stdlib/Coq.Logic.Classical_Prop.html）：

Classical.NNPP : forall (p : Prop), ~ ~ p -> p

我假设您的实际问题比 更复杂a b c = a b c，但为了提及它，如果您真的关心获得该特定假设，您可以安全地证明它，甚至无需查看 H2：

assert (abc_refl : a b c = a b c) by reflexivity.

---

如果您的实际示例没有立即反身并且相等实际上是错误的，那么您可能希望将目标转变为表明 H2 是荒谬的。您可以通过消除 H2 ( elim H2.，这基本上是对False类型进行切割) 来做到这一点，您将最终进入上下文：

H2 : ~ a b c <> a b c
EQ : a b c = a b c
=====================
False

---

我不确定所有这些是否有帮助，但您可能过于简化了您的问题，因此我无法提供更多关于您的真正问题的见解。

Answer 2

只需稍微考虑一下 Ptival 的答案 - 如果您的预期目标没有被 简单地解决reflexivity，您仍然可以取得进展，前提是您的 具有可判定的相等性Term，例如通过应用这个小引理：

Section S.
  Parameter T : Type.
  Parameter T_eq_dec : forall (x y : T), {x = y} + {x <> y}.

  Lemma not_ne : forall (x y : T), ~ (x <> y) -> x = y.
  Proof.
    intros.
    destruct (T_eq_dec x y); auto.
    unfold not in *.
    assert False.
    apply (H n).
    contradiction.
  Qed.
End S.