は<a href="https://coq.inria.fr/faq#htoc37" rel="nofollow">Coq FAQ</a>は公理と言うコック

公理。これはどのライブラリで宣言されていますか？論理的にはセクションにあるように、また古典的にもそうではありません。は<a href="https://coq.inria.fr/faq#htoc37" rel="nofollow">Coq FAQ</a>は公理と言うコック

出典

2016-06-25 k_g

ところで、もっと面白い質問は、この非常に強力な公理のために覚えているユースケースです。 – ejgallego

@ejgallego私は等価クラスが互いに素であることを証明しようとしています。私は確かに建設的な方法があると確信していますが、私はプルーフを建設的なロジックに強制しようとするより標準的なロジックの中で物事を証明することにもっと興味があります。私は公理の最小化に対する欲求を理解していますが、実用的な定理証明のために、中間、機能的な拡張性、および述語の拡張性は非常に有用であることが多いと思います。 –

@ejgallegoハスケルでSTを使うようなもの。しばしば、言語の原則からやや逸脱して、それを実用化するものがあります。コメントのために –

Extensionality_Ensemblesは、あなたが投稿公理と同等です。

出典

2016-06-27 18:33:03

私は公理は現在の標準ライブラリでは宣言されていないと思います。それは非常に強いものです（あなたがClassicalFacts.vで見ることができるように）ので、あなた自身でそれを宣言する必要があります。あなたの特定のケースは、それから、次は+関数extensionalityは、私は思う：Ensemblesライブラリから

Require Import ClassicalFacts. 
Require Import FunctionalExtensionality. 

Axiom pe : prop_extensionality. 

Lemma pred_extensionality A (P Q : A -> Prop) : 
    (forall x, P x <-> Q x) -> P = Q. 
Proof. now intros H; apply functional_extensionality; intros x; apply pe. Qed.

出典

2016-06-25 23:35:21 ejgallego

よろしくお願いいたします。私も同様のことをやってしまいましたが、私がインポートできるライブラリがあるかどうか疑問に思っていました。 –

@k_g [Logic.Diaconescu']（https://coq.inria.fr/library/Coq.Logic） .Diaconescu.html）には、 'PredicateExtensionality'公理が定義されていますが、' bool - > Prop'述語のために定義されています。 –

は<a href="https://coq.inria.fr/faq#htoc37" rel="nofollow">Coq FAQ</a>は公理と言うコック

答えて

関連する問題