Erstellen und Vergleichen von Sets in Coq

Question

Ich habe Probleme zu verstehen, ob es möglich ist zu beweisen, dass zwei Sätze (in diesem Fall normale Sprachen) identisch und damit austauschbar sind. Soweit ich weiß, können Mengen gleichwertig sein, selbst wenn sie nicht konstruktiv gleich sind.

Reguläre Sprachen sind Sätze von Strings, aber ich sehe nicht, wie man das sagt r1 = r2, so dass etwas wie Symmetrie in einem Beweis verwendet werden kann.

Hier ist meine RegularLanguage Erklärung:

Inductive RegularLanguage (A : Set) : Set := 
    | EmptyLang : RegularLanguage A 
    | EmptyStr : RegularLanguage A 
    | Unit : A -> RegularLanguage A 
    | Union : 
    RegularLanguage A 
    -> RegularLanguage A 
    -> RegularLanguage A 
    | Concat : 
    RegularLanguage A 
    -> RegularLanguage A 
    -> RegularLanguage A 
    | KleeneStar : RegularLanguage A -> RegularLanguage A 
. 

Auch wenn ich sage die Art eingestellt ist, bedeutet dies nicht eine Reihe von Zeichenfolgen erstellen, soweit ich sehen kann. Brauche ich eine Funktion vom Typ RegularLanguage -> Set of strings?

Vielen Dank für die Hilfe.

Answer 1

Es gibt ein paar Missverständnisse über einige Coq-Konzepte, die ich versuchen werde zu klären.

Zuerst sollten Sie in Coq Set nicht als das ansehen, was wir in der traditionellen Mathematik "set" nennen. Stattdessen sollten Sie es als Typ anzeigen. Coq hat auch Type, aber für die Zwecke dieses Beitrags können Sie sowohl Set als auch Type als austauschbar anzeigen. Um Verwirrung zu vermeiden, verwende ich ab sofort "set", um auf das übliche Konzept der traditionellen Mathematik zu verweisen, und "type", um auf Elemente von Set und Type in Coq zu verweisen.

Also, was genau ist der Unterschied zwischen einem Satz und einem Typ? Nun, in der normalen Mathematik macht es Sinn, sich zu fragen, ob irgendetwas ein Mitglied irgendeines gegebenen Satzes ist. Wenn wir also die Theorie der regulären Ausdrücke in der normalen Mathematik entwickeln würden und jeder reguläre Ausdruck als eine Menge betrachtet würde, würde es Sinn machen, Fragen wie 0 \in EmptyLang zu stellen, denn auch wenn 0 eine natürliche Zahl ist, könnte es sein das Element eines beliebigen Satzes a priori. Als weniger konstruiertes Beispiel ist die leere Zeichenfolge sowohl ein Mitglied der vollständigen Sprache (d. H. Diejenige, die alle Zeichenfolgen enthält) als auch der Kleene-Schließung einer beliebigen Basissprache.

In Coq dagegen hat jedes gültige Element der Sprache genau einen Typ. Die leere Zeichenfolge hat beispielsweise den Typ list A für einige A, die [] : list A geschrieben wird. Wenn wir versuchen zu fragen, ob zu einer regulären Sprache gehört, die die Syntax "hat Typ" verwendet, erhalten wir einen Fehler; versuche, z.B.

Check ([] : EmptyLang). 

Beide Sätze und Typen können als Sammlungen von Elementen sehen, aber Typen sind in gewisser Hinsicht restriktiver: zum Beispiel, einer der Kreuzung von zwei Sätzen nehmen, aber es gibt keinen Weg, um die Kreuzung von zwei der Einnahme Arten.

Zweitens, wenn Sie

Inductive RegularLanguage (A : Set) : Set := (* ... *) 

dies nicht nicht bedeuten schreiben, dass die Elemente, die Sie unter dem Header-Liste setzt noch Typen definieren. Dies bedeutet, dass Sie für jeden Typ A (der (A : Set) Teil) einen neuen Typ definieren, notiert RegularLanguage A (der RegularLanguage (A : Set) : Set Teil), dessen Elemente frei durch die Liste der Konstruktoren angegeben sind. So haben wir

EmptyLang : RegularLanguage nat 

RegularLanguage nat : Set 

aber wir nicht haben

EmptyLang : Set 

(noch einmal, können Sie versuchen, alle oben genannten Urteile in Coq eingeben, um zu sehen, welche akzeptiert werden und welche nicht).

Sein „frei erzeugt“ bedeutet insbesondere, dass die Konstrukteure Sie sind injektiv und disjoint aufgeführt. Wie zuvor erwähnt, ist es insbesondere nicht der Fall, dass Union l1 l2 = Union l2 l1; in der Tat werden Sie in der Regel Union l1 l2 <> Union l2 l1 beweisen können. Das Problem ist, dass es eine Diskrepanz zwischen dem Begriff der Gleichheit gibt, den Sie für induktiv definierte Typen in Coq bekommen (den Sie nicht ändern können), und dem beabsichtigten Gleichheitsbegriff für reguläre Sprachen.

Während es einige Wege gibt, denke ich, dass die einfachste ist, die setoid rewrite Funktion zu verwenden. Dies würde zuerst das Definieren einer Funktion oder eines Prädikats umfassen (z. B. wie es larsr vorgeschlagen hat, eine boolesche Funktion regexp_match : RegularLanguage A -> list A -> bool), um zu bestimmen, wann eine reguläre Sprache eine Zeichenfolge enthält. Sie können dann eine Äquivalenzrelation auf Sprachen definieren:

Definition regexp_equiv A (l1 l2 : RegularLanguage A) : Prop := 
    forall s, regexp_match l1 s = regexp_match l2 s. 

und verwenden setoid Rewrite mit dieser Äquivalenzrelation neu zu schreiben. Es gibt jedoch einen kleinen Vorbehalt, der besagt, dass Sie nur mit einer Äquivalenzrelation in Kontexten umschreiben können, die mit dieser Äquivalenzrelation kompatibel sind, und Sie müssen Lemmas explizit dafür nachweisen. Weitere Details finden Sie in der reference manual.

Answer 2

Zwei verschiedene Elemente in der Menge RegularLanguage A sind nicht gleich, wenn sie aus verschiedenen Konstruktoren bestehen. Betrachten Sie L1 = (a | b) und L2 = (b | a). Hier L1 <> L2 weil die Argumente zu den Konstruktoren unterschiedlich sind.

In Ihrer Schreibweise könnte L1 Union nat (Unit nat 1) (Unit nat 2)) sein und L2 ist Union nat (Unit nat 2) (Unit nat 1)).

Stattdessen möchten Sie sagen, dass es eine Funktion regexp_match : A -> RegularLanguage A -> list A -> bool gibt, die Zeichenfolgen in der angegebenen Sprache übereinstimmen. Sie müssen diese Funktion implementieren.

Zwei Regexps sind gleich, wenn sie übereinstimmen und die gleichen Zeichenfolgen ablehnen. Zum Beispiel für L1 und L2:

Lemma L1_eq_L2 : forall S, regexp_match L1 S = regexp_match L2 S. 

Wenn Sie dies unter Beweis stellen können, dann können Sie diese verwenden regexp_match L1 S mit regexp_match L2 S und umgekehrt zu ersetzen, wo Sie wollen.