Wie kann ich eine Funktion des folgenden Formulars in Coq schreiben?

Question

Ist Rekursion nur zulässig, wenn das Argument arg zu der Funktion ein direkter Unterbegriff des übergebenen Arguments ist, so dass Coq sehen kann, dass es tatsächlich endet?

Answer 1

Es ist möglich, eine solche Funktion f zu schreiben, wenn die Funktion g die Eigenschaft eines Unterbegriffs beibehält.

Einige der Standardfunktionen haben diese Eigenschaft, z.B. pred, sub:

From Coq Require Import Arith List. 
Import ListNotations. 

Fixpoint foo (x : nat) : nat := 
    match x with 
    | O => 42 
    | S x' => foo (pred x'). (* foo (x' - 1) works too *) 
    end. 

Auf der anderen Seite einige (Standard) Funktionen, diese Eigenschaft nicht haben, aber umgeschrieben werden kann, diesem Mangel abzuhelfen. Z.B. die Standard-tl Funktion erhalten nicht die Subterm Eigenschaft, so dass die folgenden nicht:

Fail Fixpoint bar (xs : list nat) : list nat := 
    match xs with 
    | [] => [] 
    | x :: xs' => bar (tl xs') 
    end. 

aber wenn wir den Schwanz Funktion wie neu definieren so

Fixpoint new_tl {A : Type} (xs : list A) := 
    match xs with 
    | [] => xs   (* `tl` returns `[]` here *) 
    | _ :: xs' => xs' 
    end. 

wir die gewünschte Eigenschaft erholen:

Fixpoint bar (xs : list nat) : list nat := 
    match xs with 
    | [] => [] 
    | x :: xs' => bar (new_tl xs') 
    end. 

Der einzige Unterschied zwischen tl und new_tl ist, dass bei leerer Eingabeliste tl gibt [] zurück, aber new_tl gibt die ursprüngliche Liste zurück.