Beweis der Irrelevanz in Coq?

Gibt es eine Möglichkeit, den folgenden Satz in Coq zu beweisen?

Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.

BEARBEITEN : Ein Versuch, eine kurze Erklärung für "Was ist der irrelevante Beweis" zu geben (korrigiere mich, wenn ich falsch oder ungenau bin)

Die Grundidee ist, dass in der Propositionswelt (oder der PropArt in Coq) die Beweisbarkeit einer Proposition, nicht die Beweise dafür, für Sie (und Sie sollten) wirklich wichtig ist. Es kann viele (oder keine) geben. Falls Sie mehrere Beweise haben, sind diese aus Sicht der Beweisbarkeit gleich, da sie den gleichen Satz beweisen . Ihre Unterscheidung spielt also keine Rolle. Dies unterscheidet sich von der Rechen Sicht , wo man wirklich über die Unterscheidung von zwei Begriffen kümmern, zum Beispiel, im Grunde, Sie wollen nicht die beiden Bewohner des boolTyps (oder Setin Coq Worte), nämlich trueund falsegleich zu sein. Aber wenn Sie sie eingeben Prop, werden sie gleich behandelt.

lo.logic type-theory proof-assistants coq Tag
quelle

Faszinierend. Ich bin sicher, Sie werden innerhalb weniger Minuten eine Antwort auf die Coq-Mailingliste erhalten. (Stellen Sie sicher, dass Sie die Antwort hier posten, wenn Sie dies tun.)

Dave Clarke

Können Sie für diejenigen von uns, die neugierig sind, worum es in Ihrer Frage geht, aber mit Coq nicht vertraut sind, vielleicht einen oder zwei Sätze hinzufügen, die erklären, was dieser Satz auf Englisch bedeutet? (Und vielleicht, worum es bei "Beweis irrelevanz" geht?)

Joshua Grochow

@Joshua, ich bin nicht ausreichend, um es im Detail zu erklären, denn es ist auch neu für mich, deshalb hat es mich auch eine ganze Weile verwirrt. Aber trotzdem, hier ist mein Versuch (siehe im Frageteil).

Tag

A \to B

$A \rightarrow B$

A

$A$

B

$B$

B

$B$

A

$A$

Antworten:

Der Beweis der Irrelevanz im Allgemeinen wird von der Theorie hinter Coq nicht impliziert. Sogar der Beweis der Irrelevanz für die Gleichheit ist nicht impliziert. es ist äquivalent Streicher Axiom K . Beide können als Axiome hinzugefügt werden .

Es gibt Entwicklungen, in denen es nützlich ist, über Beweisobjekte zu argumentieren, und Beweisunrelevanz macht dies nahezu unmöglich. Möglicherweise sollten diese Entwicklungen alle Objekte enthalten, deren Struktur neu Setformuliert werden soll, aber mit der grundlegenden Coq-Theorie ist die Möglichkeit gegeben.

Es gibt eine wichtige Untergruppe von Beweisen, die immer irrelevant ist. Streichers Axiom K gilt immer für entscheidbare Bereiche, dh Gleichheitsnachweise für entscheidbare Mengen sind eindeutig. Der allgemeine Beweis befindet sich im Eqdep_decModul in der Coq-Standardbibliothek. Hier ist Ihr Theorem als Konsequenz (mein Beweis hier ist nicht unbedingt der eleganteste):

Require Bool.
Require Eqdep_dec.
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
  intros; apply Eqdep_dec.eq_proofs_unicity; intros.
  destruct (Bool.bool_dec x y); tauto.
Qed.

Für diesen speziellen Fall ist hier ein direkter Beweis (inspiriert durch den allgemeinen Beweis in Eqdep_dec.v). Zuerst definieren wir einen kanonischen Beweis von true=b(wie in Coq üblich, ist es einfacher, die Konstante zuerst zu haben). Dann zeigen wir, dass jeder Beweis true=bdafür sein muss refl_equal true.

Let nu b (p:true = b) : true = b :=
  match Bool.bool_dec true b with
    | left eqxy => eqxy
    | right neqxy => False_ind _ (neqxy p)
  end.
Lemma bool_pcanonical : forall (b : bool) (p : true = b), p = nu b p.
Proof.
  intros. case p. destruct b.
  unfold nu; simpl. reflexivity.
  discriminate p.
Qed.

Wenn Sie Coq mit klassischer Logik erweitern, erhalten Sie den Beweis der Irrelevanz. Intuitiv ausgedrückt gibt Ihnen die klassische Logik ein Entscheidungsorakel für Aussagen, und das ist gut genug für Axiom K. Das Coq-Standardbibliotheksmodul enthält einen Beweis Classical_Prop.

Gilles 'SO - hör auf böse zu sein'
quelle