Ich möchte forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q. in Coq beweisen oder verfälschen. Hier ist mein Ansatz.
Aber inversion H tut nichts. Ich denke, es liegt vielleicht daran, dass die Unabhängigkeit des Coq bewiesen ist (ich bin kein englischer Muttersprachler und ich kenne die genauen Wörter nicht, bitte vergib meine Unwissenheit), und coq macht es unmöglich, One = Two - & gt; Falsch. Aber wenn ja, warum muss man den Inhalt eines Beweises eliminieren?
Ohne den obigen Satz kann ich das Folgende oder seine Negationen nicht beweisen.
%Vor%Meine Frage ist also:
forall (P Q : Prop),
(P -> Q) -> (Q -> P) -> P = Q. in Coq bewiesen oder verfälscht werden? inversion H nichts tut; liegt es daran, dass der Coq-Nachweis unabhängig ist, und wenn ja, warum verschwendet Coq dabei Energie? Das von Ihnen erwähnte Prinzip, forall P Q : Prop, (P <-> Q) -> P = Q , wird normalerweise als propositional extensionality bezeichnet. Dieses Prinzip ist in Coqs Logik nicht beweisbar, und ursprünglich war die Logik so entworfen worden, dass sie als ein Axiom ohne Schaden hinzugefügt werden konnte. So kann man in der Standardbibliothek ( Coq.Logic.ClassicalFacts ) viele Sätze über dieses Prinzip finden, die es mit anderen bekannten logischen Prinzipien des klassischen Denkens verbinden. Überraschenderweise hat kürzlich herausgefunden, dass Coqs Logik damit nicht vereinbar ist Prinzip, aber aus einem sehr subtilen Grund. Dies wird als Fehler angesehen, da die Logik so entworfen wurde, dass dies als ein Axiom ohne Schaden hinzugefügt werden konnte. Sie wollten dieses Problem in der neuen Version von Coq beheben, aber ich weiß nicht, was der aktuelle Status davon ist. Ab Version 8.4 ist propositionale Extensionalität in Coq inkonsistent.
Wenn dieser Fehler in zukünftigen Versionen von Coq behoben wird, sollte es in Coq weder möglich sein, dieses Prinzip zu beweisen noch zu widerlegen. Mit anderen Worten, das Coq-Team möchte, dass dieses Prinzip unabhängig von Coqs Logik ist.
inversion H macht da nichts, weil die Regeln für das Beweisen von Beweisen (Dinge, deren Typ ein Prop ist) sich von denen für das Beweisen von Nichtbeweisen unterscheiden (Dinge, deren Typ ein Type ist) . Sie wissen vielleicht, dass Beweise in Coq nur Begriffe sind. Unter der Haube baut inversion im Wesentlichen den folgenden Begriff:
Wenn Sie versuchen, dasselbe mit einer Version von bool in Prop zu tun, erhalten Sie einen informativeren Fehler:
Tatsächlich ist einer der Gründe dafür, dass Coq so entworfen wurde, dass es mit einem anderen Prinzip namens proof irrelevance kompatibel ist (ich denke, das ist es, was Sie mit "Beweisunabhängigkeit" meinen).
Tags und Links coq equality dependent-type proof curry-howard