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 기능은 subterm 속성을 보존하지 않기 때문에 다음과 같은 실패

tl과 new_tl의 유일한 차이점은 빈 입력 목록의 경우 tl은 []을 반환하지만 new_tl은 원래 목록을 반환합니다.