Die Coq FAQ sagt, dass das Axiom:Wo ist die Extensionalität von Prädikaten Axiom Coq
Extensionality of predicates: ∀ P Q:A→ Prop, (∀ x, P(x) ↔ Q(x)) → P=Q
mit Coq konsistent ist. In welcher Bibliothek wird dies behauptet? Es ist nicht in der Logik, wie der Abschnitt impliziert, noch ist es in der Klassik.
Extensionality_Ensembles aus der Ensembles Bibliothek entspricht dem Axiom Sie auf dem Laufenden.
Ich denke, dass das Axiom in der aktuellen Standardbibliothek nicht deklariert ist; es ist ein ziemlich starker (wie Sie in ClassicalFacts.v sehen können), also müssen Sie es selbst erklären. Ihren speziellen Fall folgt daraus + Funktion Extensionalität Ich denke:
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.
OK danke! Ich habe etwas Ähnliches gemacht, aber ich habe mich gefragt, ob es eine Bibliothek gibt, die ich importieren könnte. –
@k_g Nur eine Bemerkung: in ['Logic.Diaconescu'] (https://coq.inria.fr/library/Coq.Logic .Diaconescu.html) wir haben das 'PredicateExtensionality'-Axiom definiert, aber für' bool -> Prop'-Prädikate. –
BTW, IMHO eine interessantere Frage ist, was ist der Anwendungsfall Sie für dieses sehr starke Axiom denken. – ejgallego
@ejgallego Ich versuche zu beweisen, dass Äquivalenzklassen disjunkt sind. Ich bin mir ziemlich sicher, dass es einen konstruktiven Weg dafür gibt, aber ich bin mehr daran interessiert, Dinge innerhalb der Standardlogik zu beweisen, als zu versuchen, die Beweise in konstruktive Logik zu zwingen. Ehrlich gesagt, während ich den Wunsch nach Minimalität von Axiomen verstehe, denke ich, dass für praktische Theorembeweise, ausgeschlossene mittlere, funktionale Extensionalität und sogar Extensionalität von Prädikaten oft sehr nützlich sind. –
@ejgallego Wie ST in Haskell. Oft ist es etwas vom Prinzip der Sprache abzuweichen, was es praktisch macht. –