COQ变化前提“的否定不等于”到“等于”

Question

假设我有这样一个前提：

H2: ~ a b c <> a b c 

而且我希望将它更改为：

a b c = a b c 

凡

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

b和c都是术语

我该怎么办？谢谢！

Answer 1

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

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

因此，要达到什么是什么逻辑学家通常所说的“双重否定淘汰”。这不是一个intuitionistically，可证明的定理，因此在Classical模块勒柯克（见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.