Wann reduziert die Terminierungsprüfung einen Datensatz Accessor

Question

Ich stolpere über Verhalten von Coqs Termination Checker, die ich mir nicht erklären kann. Bedenken Sie:

Require Import Coq.Lists.List. 

Record C a := { P : a -> bool }. 

Arguments P {_}. 

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C). 

Definition list_C {a} (a_C : C a) : C (list a) := {| P := list_P a_C |}. 

(* Note that *) 
Eval cbn in  fun a C => (P (list_C C)). 
(* evaluates to: fun a C => list_P C *) 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works, using a local record *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P1 a_C) in 
    let list_C' := Build_C _ (list_P tree_C) in 
    match t with Node _ x ts => orb (P a_C x) (P list_C' ts) end. 

(* Works too, using list_P directly *) 
Fixpoint tree_P2 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P2 a_C) in 
    match t with Node _ x ts => orb (P a_C x) (list_P tree_C ts) end. 

(* Does not work, using a globally defined record. Why not? *) 
Fixpoint tree_P3 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := Build_C _ (tree_P3 a_C) in 
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end. 

Die erste und zweite Beispiel zeigt, dass, wenn sie versuchen, zu verstehen, ob ein Fixpunkt ist beendet, Coq der Lage ist, Rekord Accessoren zu lösen, im Grunde die Bewertung, was wir in tree_P1 zu geschrieben, was wir in tree_P2 schrieb.

Aber das scheint nur zu funktionieren, wenn der Datensatz lokal (let tree_C :=…) erstellt wird, nicht, wenn es mit Definition definiert ist.

Aber Fixpoint kann andere Definitionen gut durchsehen, z.B. durch list_P. Also was ist das Besondere an Aufzeichnungen, und kann ich Coq akzeptieren tree_P3?

Answer 1

Nach einiger Lektüre der Abschlussprüfung in Coq, ich glaube ich die Lösung gefunden:

Die Kontrolleur Kündigung wird immer lokale Definitionen entfalten, und Beta-verringern. Deshalb funktioniert tree_P1 funktioniert.

Der Abschlussprüfer auch wird, falls erforderlich, entfalten Definitionen, die aufgerufen werden (wie list_C', P, existsb), weshalb tree_P2 funktioniert.

Der Terminierungsprüfer wird jedoch keine Definitionen auffalten, die in einer match … with-Klausel wie list_C erscheinen. Hier ist ein minimales Beispiel dafür:

(* works *) 
Fixpoint foo1 (n : nat) : nat := 
    let t := Some True in 
    match Some True with | Some True => 0 
         | None => foo1 n end. 

(* works *) 
Fixpoint foo2 (n : nat) : nat := 
    let t := Some True in 
    match t with | Some True => 0 
       | None => foo2 n end. 

(* does not work *) 
Definition t := Some True. 

Fixpoint foo3 (n : nat) : nat := 
    match t with | Some True => 0 
       | None => foo3 n end. 

Ein Work-around für den originalen Code ist, um sicherzustellen, dass alle Definitionen genannt werden (und nicht muster abgeglichen), um sicherzustellen, dass die Abschlussprüfer sie entfalten . Wir können das tun, indem Sie auf eine Fortsetzung Übertragungsstil Schalt:

Require Import Coq.Lists.List. 

Record C_dict a := { P' : a -> bool }. 

Definition C a : Type := forall r, (C_dict a -> r) -> r. 

Definition P {a} (a_C : C a) : a -> bool := 
    a_C _ (P' _). 

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C). 

Definition list_C {a} (a_C : C a) : C (list a) := 
    fun _ k => k {| P' := list_P a_C |}. 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works now! *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in 
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end. 

Dies funktioniert auch mit Typklassen, wie Typenklasse Auflösung indepenent dieser Fragen ist:

Require Import Coq.Lists.List. 

Record C_dict a := { P' : a -> bool }. 

Definition C a : Type := forall r, (C_dict a -> r) -> r. 
Existing Class C. 

Definition P {a} {a_C : C a} : a -> bool := a_C _ (P' _). 

Definition list_P {a} `{C a} : list a -> bool := existsb P. 

Instance list_C {a} (a_C : C a) : C (list a) := 
    fun _ k => k {| P' := list_P |}. 

Inductive tree a := Node : a -> list (tree a) -> tree a. 

(* Works now! *) 
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool := 
    let tree_C : C (tree a) := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in 
    match t with Node _ x ts => orb (P x) (P ts) end. 

Answer 2

Für Frage 1. Ich glaube, dass in tree_P1 die Definition der Klasseninstanz innerhalb der fix Konstruktion und reduziert zum Zeitpunkt der Beendigung der Prüfung ist.

Die folgende Definition wird abgelehnt, wie Sie zu Recht betonen.

Fixpoint tree_P1' {a} `{C a} (t : tree a) : bool := 
    let tree_C := Build_C _ tree_P1' in 
    match t with Node _ x ts => orb (P x) (@P _ (* mark *) _ ts) end. 

In dieser Definition ist die Klasseninstanz nach dem Kommentar benötigt (* mark *) wird durch die Definition Sie auf Linie haben gefüllt 7. Aber diese Definition lebt außerhalb des fix Konstrukt und wird von der Abschlussprüfung nicht reduziert werden auf die gleiche Weise. Als Ergebnis bleibt ein Vorkommen von tree_P1', das nicht auf ein Baumargument angewendet wird, im Code, und der Terminierungsprüfer kann nicht feststellen, dass dieses Vorkommen nur für Argumente verwendet wird, die kleiner als das ursprüngliche Argument sind.

Dies ist eine wilde Vermutung, weil wir den Körper der Funktion, die abgelehnt wird, nicht sehen können.