如何證明Coq中的命題擴展性？

我試圖證明關於Prop的替代定理，並且我很失敗。以下定理是否可以用coq來證明，如果不是，爲什麼不能。如何證明Coq中的命題擴展性？

Theorem prop_subst: 
    forall (f : Prop -> Prop) (P Q : Prop), 
     (P <-> Q) -> ((f P) <-> (f Q)).

問題是，邏輯上的證明是歸納。支柱沒有歸納定義，據我所知。 Coq如何證明這樣一個定理？

來源

2012-06-17 Mayer Goldberg

我不認爲你可以證明這一點，但我不知道的細節... – Ptival

我可以把它作爲公理，但是這將是一種粗俗，不是嗎？ –

@MayerGoldberg對不起，太快閱讀你的問題;-) –

你所尋找的被稱爲「外延性：」

http://coq.inria.fr/V8.1/faq.html#htoc41

http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

http://en.wikipedia.org/wiki/Extensionality

編輯：

可以承認謂語擴展性，如Coq FAQ中所述。

來源

2012-06-17 16:27:34

我不認爲這是擴展性：請注意，我只使用一個函數（作爲上下文），而不是兩個，如同擴展性一樣。我想要的是所謂的參照透明度：如果A <-> B，那麼在任何表達式中，除了包含A的表達式，我應該能夠用B代替A.另一方面，也許你的意思是「命題擴展性」，它不是一樣，但似乎給了我想要的東西。 –

答案如下：我找的屬性叫做命題擴展性，意思是forall p q : Prop, (p <-> q) -> (p = q)。相反，是微不足道的。這是在Library Coq.Logic.ClassicalFacts中定義的東西，以及來自經典，即非直覺邏輯的其他事實。上面的定義叫做prop_extensionality，可以使用如下：Axiom EquivThenEqual: prop_extensionality。現在，您可以應用EquivThenEqual，將其用於重寫等。感謝Kristopher Micinski指出的擴展性。

來源

2012-06-17 17:09:44

該死的，你打敗了我;-)，我正準備向你指出FAQ –

這個部分當你自己的答案最合適時，你可以通過將你的答案標記爲可接受的來幫助我學習Coq。你會得到聲望點。不要害羞 - 堆棧溢出是爲了這樣工作。 – minopret

這是命題的擴展性。

Lemma blah: forall (P Q: Prop), (forall (f:Prop -> Prop), f Q -> f P) -> P = Q. 
    intros P Q H. 
    apply (H (fun x => x = Q)). 
    reflexivity. 
Qed. 

Section S. 

Hypothesis prop_subst: 
    forall (f : Prop -> Prop) (P Q : Prop), 
    (P <-> Q) -> ((f P) <-> (f Q)). 

Lemma prop_subst_is_ext: forall P Q, (P <-> Q) -> P = Q. 
    intros. 
    apply blah. 
    intro f. 
    destruct (prop_subst f P Q); assumption. 
Qed. 

End S. 

Check prop_subst_is_ext.

來源

2014-01-28 22:51:28

如何證明Coq中的命題擴展性？

回答

相關問題