COQ變化前提「的否定不等於」到「等於」

假設我有這樣一個前提：COQ變化前提「的否定不等於」到「等於」

H2: ~ a b c <> a b c

而且我希望將它更改爲：

a b c = a b c

凡

a是術語 - >術語 - >術語

b和c都是術語

我該怎麼辦？謝謝！

來源

2013-03-03 yanhan

如果你展開的~和<>的定義，你假設有以下類型：

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

我不知道是否所有的這有幫助，但是你可能會過分簡化你的問題，這樣我就不能提供更多關於你的真正問題的見解。

來源

2013-03-03 17:35:36 Ptival

嗨Ptival，我已經簡化了整體的問題，但總體上可以只通過解決什麼我上面張貼解決。沒有意識到它需要NNPP。謝謝！併爲真正遲到的答覆道歉。 – yanhan 2013-03-23 00:36:38

只是一點點想法添加到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.

來源

2013-03-03 21:08:50 t0yv0

COQ變化前提「的否定不等於」到「等於」

回答

相關問題