Mit einer rekursiven Funktion berechnen, die durch wohldefinierte Induktion definiert ist

Question

Wenn ich Function verwende, um eine nicht strukturell rekursive Funktion in Coq zu definieren, verhält sich das resultierende Objekt merkwürdig, wenn eine bestimmte Berechnung angefordert wird. Anstatt das Ergebnis direkt anzugeben, gibt die Eval compute in ...-Direktive einen ziemlich langen (typischerweise 170.000 Zeilen) Ausdruck zurück. Es scheint, dass Coq nicht alles auswerten kann und daher einen vereinfachten (aber langen) Ausdruck anstelle nur eines Werts zurückgibt.

Das Problem scheint von der Art und Weise zu kommen, wie ich die Verpflichtungen von Function generiert zu beweisen. Zuerst dachte ich, das Problem käme von den undurchsichtigen Begriffen, die ich benutzt habe, und ich habe alle Lemmas in transparente Konstanten umgewandelt. Gibt es übrigens eine Möglichkeit, die in einem Begriff auftretenden undurchsichtigen Begriffe aufzulisten? Oder eine andere Möglichkeit, undurchsichtige Lemmas in transparente zu verwandeln?

Ich bemerkte dann, dass das Problem genauer aus dem Beweis kam, dass die verwendete Reihenfolge begründet ist. Aber ich habe seltsame Ergebnisse.

Zum Beispiel definiere ich log2 auf die natürlichen Zahlen durch wiederholtes Anwenden div2. Hier ist die Definition:

Function log2 n {wf lt n} := 
    match n with 
    | 0 => 0 
    | 1 => 0 
    | n => S (log2 (Nat.div2 n)) 
    end. 

Ich bekomme zwei Beweispflichten. Der erste prüft, ob n die Relation lt in den rekursiven Aufrufen berücksichtigt und leicht zu beweisen ist.

forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1) 

intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n. 

Der zweite überprüft, dass lt eine fundierte Bestellung ist. Dies ist bereits in der Standardbibliothek nachgewiesen. Das entsprechende Lemma ist Coq.Arith.Wf_nat.lt_wf.

Wenn ich diesen Beweis verwende, verhält sich die resultierende Funktion normal. Eval compute in log24 10. gibt 3 zurück.

Aber wenn ich den Beweis selbst machen will, bekomme ich nicht immer dieses Verhalten. Erstens, wenn ich den Beweis mit Qed anstelle von Defined beende, ist das Ergebnis der Berechnung (selbst bei kleinen Zahlen) ein komplexer Ausdruck und keine einzelne Zahl. Also verwende ich Defined und versuche nur transparente Lemmas zu verwenden.

Hier ist Lemma1 ein Beweis für die fundierte Induktion der natürlichen Zahlen. Auch hier kann ich bereits existierende Lemmas verwenden, wie lt_wf_ind, lt_wf_rec, lt_wf_rec1, die sich in Coq.Arith.Wf_nat oder sogar well-founded lt befinden. Das erste funktioniert nicht, es scheint, weil es undurchsichtig ist. Die drei anderen arbeiten.

Ich versuchte, es direkt unter Verwendung der Standardinduktion auf den natürlichen Zahlen, nat_ind zu beweisen. Dies ergibt:

Lemma lemma1 : forall n (P:nat -> Prop), 
    (forall n, (forall p, p < n -> P p) -> P n) -> P n. 
Proof. 
    intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)). 
    simpl in H0. apply H0 with (n:=S n). 
    - intros. inversion H1. 
    - intros. inversion H2. 
    + apply H. exact H1. 
    + apply H1. assumption. 
    - apply le_n. 
Defined. 

Mit diesem Beweis (und einigen Varianten davon), log2 hat das gleiche seltsame Verhalten. Und dieser Beweis scheint nur transparente Objekte zu verwenden, also ist das Problem vielleicht nicht da.

Wie kann ich einen Function definieren, der verständliche Ergebnisse zu bestimmten Werten liefert?

Answer 1

Ich habe es geschafft, Pin-Point an die Stelle, die Probleme verursacht: es ist inversion H2. in lemma1. Es stellt sich heraus, dass wir nicht brauchen, dass Fall-Analyse und intuition den Beweis beenden kann (dies nicht der Fall Muster-Match auf H2):

Lemma lemma1 : forall n (P:nat -> Prop), 
    (forall n, (forall p, p < n -> P p) -> P n) -> P n. 
Proof. 
    intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)). 
    simpl in H0. apply H0 with (n:=S n). 
    - intros. inversion H1. 
    - intros. intuition. 
    - apply le_n. 
Defined. 

Wenn wir lemma1 mit diesem Beweis verwenden, die Berechnung von log2 10 Ergebnisse in 3.

By the way, hier meine Version von lt_wf2 ist (es läßt uns auch berechnen):

Lemma lt_wf2 : well_founded lt. 
Proof. 
    unfold well_founded; intros n. 
    induction n; constructor; intros k Hk. 
    - inversion Hk. 
    - constructor; intros m Hm. 
    apply IHn; omega. 
(* OR: apply IHn, Nat.lt_le_trans with (m := k); auto with arith. *) 
Defined. 

Ich glaube, der Using Coq's evaluation mechanisms in anger Blog-Eintrag von Xavier Leroy diese Art von Verhalten erklärt.

Es eliminiert den Beweis der Gleichheit zwischen den Köpfen vor dem Rückfall über die Schwänze und schließlich entscheiden, ob eine linke oder eine rechte zu produzieren. Dies macht den linken/rechten Teil des Endergebnisses abhängig von einem Beweisterm, was sich im Allgemeinen nicht verringert!

In unserem Fall beseitigen wir den Beweis der Ungleichheit (inversion H2.) im Beweis von lemma1 und der Function Mechanismus macht unsere Berechnungen auf einem Beweis Begriff abhängen. Daher kann der Auswerter nicht fortgesetzt werden, wenn n> 1.

Und der Grund inversion H1. im Körper des Lemmas Berechnungen nicht beeinflussen besteht darin, dass für n = 0 und n = 1 wird log2 n definiert innerhalb des match Expression als Basis Fällen.

Um diesen Punkt zu illustrieren, lassen Sie mir ein Beispiel zeigen, wenn wir Auswertung von log2 n beliebigen Werten n und n + 1 unserer Wahl zu verhindern, wo n > 1 und nirgendwo sonst!

Lemma lt_wf2' : well_founded lt. 
Proof. 
    unfold well_founded; intros n. 
    induction n; constructor; intros k Hk. 
    - inversion Hk.   (* n = 0 *) 
    - destruct n. intuition. (* n = 1 *) 
    destruct n. intuition. (* n = 2 *) 
    destruct n. intuition. (* n = 3 *) 
    destruct n. inversion Hk; intuition. (* n = 4 and n = 5 - won't evaluate *) 
    (* n > 5 *) 
    constructor; intros m Hm; apply IHn; omega. 
Defined. 

Wenn Sie das modifizierte Lemma in der Definition von log2 verwenden werden Sie sehen, dass es überall außer n = 4 und n = 5 berechnet.Nun, fast überall - Berechnungen mit großen nat s können in Stack-Überlauf oder Segmentierungsfehler zur Folge hat, wie Coq uns warnt:

Warnung: Stapelüberlauf oder Segmentierungsfehler passiert, wenn mit großer Zahl in nat arbeiten (beobachteter Schwellwert kann von 5000 bis 70000 variieren abhängig von Ihren Systemgrenzen und dem ausgeführten Befehl).

Und log2 Arbeit für n = 4 und n = 5 auch für die oben „fehlerhaft“ sicher zu machen, wir log2 wie diese

Function log2 n {wf lt n} := 
    match n with 
    | 0 => 0 
    | 1 => 0 
    | 4 => 2 
    | 5 => 2 
    | n => S (log2 (Nat.div2 n)) 
    end. 

fügt die erforderlichen Beweise am Ende ändern könnte.

---

Die „begründete“ Beweis muss transparent sein und verlassen sich nicht auf Pattern-Matching auf Beweis Objekten, weil die Function Mechanismus tatsächlich die lt_wf Lemma verwendet die Abnahme Beendigung Wache zu berechnen.

fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0} 

Es ist leicht zu sehen, dass x0 : Prop, so wird sie gelöscht, wenn: Wenn wir den von Eval produzierte Begriff suchen (in einem Fall, wo Auswertung ein nat zu produzieren ausfällt), werden wir etwas in diese Richtung sehen Extrahieren des Funktionsprogramms log2 in, sagen wir OCaml, aber Coqs interner Evaluierungsmechanismus muss es verwenden, um eine Beendigung sicherzustellen.

Answer 2

Das Reduktionsverhalten von Funktionen, die durch eine fundierte Rekursion in Coq definiert sind, ist im Allgemeinen nicht sehr gut, auch wenn Sie Ihre Beweise für transparent erklären.Der Grund dafür ist, dass Begründungsargumente in der Regel mit komplizierten Beweisklauseln durchgeführt werden müssen. Da diese Beweisbegriffe letztendlich in wohlbegründeten rekursiven Definitionen erscheinen, wird die "Vereinfachung" Ihrer Funktion alle diese Beweisbegriffe erscheinen lassen, wie Sie bemerkt haben.

Es ist einfacher, sich auf benutzerdefinierte Taktiken und Lemmas zu verlassen, um auf diese Weise definierte Funktionen zu reduzieren. Zuerst würde ich empfehlen, Program Fixpoint über Function zu favorisieren, weil letzteres viel älter ist und (glaube ich) weniger gut gepflegt. So würden Sie mit einer Definition am Ende wie folgt:

Require Import Coq.Numbers.Natural.Peano.NPeano. 
Require Import Coq.Program.Wf. 
Require Import Coq.Program.Tactics. 

Program Fixpoint log2 n {wf lt n} := 
    match n with 
    | 0 => 0 
    | 1 => 0 
    | n => S (log2 (Nat.div2 n)) 
    end. 

Next Obligation. 
admit. 
Qed. 

Nun, man muss nur die program_simpl Taktik verwenden müssen Anrufe log2 zu vereinfachen. Hier ein Beispiel:

Lemma foo : log2 4 = 2. 
Proof. 
    program_simpl. 
Qed.