Coqに次の形式の関数を書くにはどうすればよいですか？

Question

f x = f (g subtermOfX) 

再帰は、関数へのargが、渡されたargの直接の下位でCoqが実際に終了することがわかるようになっている場合にのみ許可されますか？

Answer 1

機能gが下位の性質を保持する場合、fと書くことは可能です。

いくつかの標準機能にはこのプロパティがあります。 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. 

一方、いくつかの（標準）関数は、このプロパティを持っていないが、この欠陥を是正するために書き換えることができます。例えば。

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

：我々は

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

たちは、所望の特性を回復することができますので、のような尾の機能を再定義する場合

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

をしかし：標準tl機能は部分項のプロパティを保持していないので、次は失敗します

tlとnew_tlの唯一の違いは、空の入力リストの場合tlは[]を返しますが、new_tlは元のリストを返します。