Verwirrt über Mustervergleich in Record Konstruktionen in Coq

Question

Ich habe Coq für eine sehr kurze Zeit verwendet und ich stoße immer noch mit einigen Dingen in Wände. Ich habe ein Set mit einer Record-Konstruktion definiert. Jetzt muss ich einen Mustervergleich durchführen, um es zu benutzen, aber ich habe Probleme, es richtig zu benutzen. Erstens, das sind meine Elemente.

Inductive element : Set := 
| empty : element 
. 
. 
. 
| fun_m : element -> element -> element 
| n_fun : nat -> element -> element 
. 

Ich hebe die Elemente mit bestimmtem Merkmale eine Teilmenge von ihnen den nächsten Weg zu machen:

Inductive esp_char : elements -> Prop := 
| esp1 : esp_char empty 
| esp2 : forall (n : nat)(E : element), esp_char E -> esp_char (n_fun n E). 

Record especial : Set := mk_esp{ E : element ; C : (esp_char E)}. 

Nun, ich brauche Definition zu verwenden und beheben Punkt auf den ‚especial‘ Elemente, nur die zwei, die ich ausgewählt habe. Ich habe die Dokumentation zu verlesen und was ich bekommen ist, dass ich so etwas tun bräuchten:

Fixpoint Size (E : especial): nat := 
match E with 
|{|E := empty |}  => 0 
|{|E := n_fun n E0|} => (Size E0) + 1 
end. 

Natürlich ist dies sagt mir, dass ich alles, was auf dem induktiven Teil der Elemente fehlt bin so ich hinzufügen {|E := _ |}=> 0, oder irgendetwas, nur um die Induktion voll zu machen. Auch dies zu tun, finde ich dann dieses Problem:

|{|E := n_fun n E0|} => (Size E0) + 1 

Error: 
In environment 
Size : especial -> nat 
E : especial 
f : element 
i : esp_char f 
n : nat 
E0 : element 
The term "E0" has type "element" while it is expected to have type "especial". 

Was ich nicht in der Lage gewesen zu tun, ist das letzte, was zu beheben, ich habe einen Lemma zu beweisen, dass, wenn n_fun n E0 ‚especial‘ ist dann E0 besonders ist, aber ich kann baue es nicht so im Fixpoint. Ich habe auch die Größe für "alle Elemente" definiert und dann einfach die "besonderen" in einer Definition ausgewählt, aber ich möchte direkten Mustervergleich direkt auf dem Set "besonders" vornehmen können. Danke für deinen Beitrag.

EDIT: Vergaß zu erwähnen, dass ich auch einen Zwang habe, immer besondere Elemente zu senden.

EDIT: Dies ist der Ansatz, den ich vor der Veröffentlichung hatte:

Fixpoint ElementSize (E : element): nat := 
match E with 
| n_fun n E0 => (ElementSize E0) + 1 
| _ => 0 
end. 

Definition Size (E : especial) := ElementSize E. 

Answer 1

Ich habe versucht zu tun hätte:

Lemma mk_especial_proof n E : esp_char (n_fun n E) -> esp_char E. 
Proof. now intros U; inversion U. Qed. 

Fixpoint Size (E : especial): nat := 
match E with 
|{|E := empty    |} => 0 
|{|E := n_fun n E0; C := P |} => (Size (mk_esp E0 (mk_especial_proof _ _ P))) + 1 
|{|E := fun_m E1 E2  |} => 0 
end. 

Dies wird jedoch die Beendigung Prüfung fehlschlagen. Ich weiß nicht, wie ich dieses Problem mit Datensätzen lösen kann. Ich würde definitiv dem Ansatz folgen, den ich in den Kommentaren erwähnt habe (mit einem Fixpunkt über dem Basis-Datentyp).

EDIT: Einzelne Fixpunktlösung hinzugefügt.

Fixpoint size_e e := 
    match e with 
    | empty  => 0 
    | fun_m e1 e2 => 0 
    | n_fun _ e => 1 + size_e e 
    end. 

Definition size_esp e := size_e (E e). 

Answer 2

Ich habe Ihr Beispiel auf dieses reduziert, aber Sie können leicht zu Ihrer Definition zurückkehren. Wir haben eine Menge und eine durch ein induktives Prädikat definierte Teilmenge. Oft verwendet man dazu Sigma-Typen, mit der Notation {b | Small b}, aber es ist eigentlich die selbe wie die in Ihrem Beispiel verwendete Record Definition, also egal :-).

Inductive Big : Set := (* a big set *) 
| A 
| B (b0 b1:Big) 
| C (b: Big). 

Inductive Small : Big -> Prop := (* a subset *) 
| A' : Small A 
| C' (b:Big) : Small b -> Small (C b). 

Record small := mk_small { b:Big ; P:Small b }. 

Hier ist eine Lösung.

Lemma Small_lemma: forall b, Small (C b) -> Small b. 
Proof. intros b H; now inversion H. Qed. 

Fixpoint size (b : Big) : Small b -> nat := 
    match b with 
     | A => fun _ => 0 
     | B _ _ => fun _ => 0 
     | C b' => fun H => 1 + size b' (Small_lemma _ H) 
    end. 

Definition Size (s:small) : nat := 
    let (b,H) := s in size b H. 

Lage sein, die Hypothese H in den match -branches zu verwenden, wird sie in der Branche als ein Funktionsargument gesendet. Sonst wird die Zerstörung von b unter H nicht durchgeführt, und Coq kann nicht beweisen, dass wir eine strukturelle Rekursion unter H durchführen.