Wie kann man die Vererbung in Coq ausdrücken?

Question

Wie bekomme ich die Alleltern eines Elements in Coq? ich einen Satz in Coq wie folgt definieren:

Inductive Gen : Set := 
| BGen : nat -> nat -> Gen. 

Es gibt viele Fälle, wie:

Definition g1 = BGen 1 2. 
Definition g2 = BGen 2 3. 

Nun, ich möchte den Eltern Element von 3 erhalten, das heißt [1,2]. Ich schreibe eine Funktion:

Fixpoint parents (c : nat) (l : list Gen) := 
match l with 
| [] => [] 
| (BGen p c') :: l' => if beq_nat c c' 
        then [p] 
        else parents c l' 
end. 

Ich kann nur die direkt Eltern erhalte [2] von 3: Wie kann ich die alle Eltern wie [1,2] in diesem Beispiel erhalten?

Answer 1

Sie scheinen zu fragen, wie die Schließung einer Funktion unter wiederholter Funktion Anwendung berechnen. Der Schlüssel zu dem Problem besteht darin, einen Weg zu finden, um eine Beendigung sicherzustellen, d. H. Eine Möglichkeit, die maximale Häufigkeit zu bestimmen, mit der die Funktion aufgerufen werden kann. In diesem Fall ist eine einfache obere Grenze List.length l; Ein Element kann nicht mehr transitive Eltern haben als Generationen. Mit dieser Einsicht können wir eine Funktion definieren, die eine Liste von Zahlen nimmt und gibt eine Liste der Zahlen zusammen mit all ihren Eltern, und dann wenden wir diese Funktion List.length l mal an sich selbst, beginnend mit parents von c:

Require Import Coq.Lists.List. Import ListNotations. 
Require Import Coq.Sorting.Mergesort. Import NatSort. 
Scheme Equality for nat. 
Inductive Gen : Set := 
| BGen : nat -> nat -> Gen. 

Definition g1 := BGen 1 2. 
Definition g2 := BGen 2 3. 


Fixpoint parents (l : list Gen) (c : nat) := 
    match l with 
    | [] => [] 
    | (BGen p c') :: l' => if nat_beq c c' 
         then [p] 
         else parents l' c 
    end. 

Fixpoint deduplicate' (ls : list nat) := 
    match ls with 
    | [] => [] 
    | x :: [] => [x] 
    | x :: ((y :: ys) as xs) 
    => if nat_beq x y 
     then deduplicate' xs 
     else x :: deduplicate' xs 
    end. 
Definition deduplicate (ls : list nat) := deduplicate' (sort ls). 

Definition parents_step (l : list Gen) (cs : list nat) := 
    deduplicate (cs ++ List.flat_map (parents l) cs). 

Fixpoint all_parents' (l : list Gen) (cs : list nat) (fuel : nat) := 
    match fuel with 
    | 0 => cs 
    | S fuel' 
    => all_parents' l (parents_step l cs) fuel' 
    end. 
Definition all_parents (l : list Gen) (c : nat) := 
    deduplicate (all_parents' l (parents l c) (List.length l)). 

Definition gs := (g1::g2::nil). 

Compute all_parents gs 3. (* [1; 2] *)