중첩 된 고정을위한 유도 원리를 얻는 방법

Question

나는 값의 범위를 검색하는 함수로 작업 중이다.

Require Import List. 

(* Implementation of ListTest omitted. *) 
Definition ListTest (l : list nat) := false. 

Definition SearchCountList n := 
    (fix f i l := match i with 
    | 0 => ListTest (rev l) 
    | S i1 => 
    (fix g j l1 := match j with 
    | 0 => false 
    | S j1 => 
     if f i1 (j :: l1) 
     then true 
     else g j1 l1 
    end) (n + n) (i :: l) 
    end) n nil 
. 

이 기능에 대해 추론 할 수 있기를 바랍니다.

그러나 coq의 내장 유도 원리 설비를 작동시킬 수 없습니다.

중첩 된 재귀가 아니라 상호 재귀를 처리하기 위해 coq가 설정되어있는 것 같습니다. 이 경우, 본질적으로 루프에 중첩 된 2 개가 있습니다.

Definition SearchCountList_Loop := 
    fix outer n i l {struct i} := 
    match i with 
    | 0 => ListTest (rev l) 
    | S i1 => inner n i1 (n + n) (i :: l) 
    end 
    with inner n i j l {struct j} := 
    match j with 
    | 0 => false 
    | S j1 => 
     if outer n i (j :: l) 
     then true 
     else inner n i j1 l 
    end 
    for outer 
. 

하지만 그 내부에 오류를

재귀 호출을 수확량 동일한 주요 인자를 갖는 "n + n"대신 :

그러나 상호 재귀로 변환하는 것은 하나 쉽기 때문에 "i1".

따라서 직접 정의를 받아들이려면 측정 값을 사용해야 할 것 같습니다. 때때로 j를 재설정하는 것이 혼란 스럽습니다. 그러나, 중첩 된 설정에서, 그것은 감각이 있습니다, 왜냐하면 저는 감소했고, 저는 바깥 고리입니다.

따라서 상호 재귀가 아니라 중첩 된 재귀를 처리하는 표준 방법이 있습니까? 별도의 귀납 이론을 사용하지 않고 사건을 추론하는 더 쉬운 방법이 있습니까? 자동으로 생성하는 방법을 찾지 못했기 때문에 유도 원리를 직접 작성하는 데 어려움을 겪고 있습니다.

Answer 1

이 경우에 상호 재귀를 피하기위한 속임수가 있습니다. f i1을 f 안에 넣고 그 결과를 g으로 전달할 수 있습니다.

Fixpoint g (f_n_i1 : list nat -> bool) (j : nat) (l1 : list nat) : bool := 
    match j with 
    | 0 => false 
    | S j1 => if f_n_i1 (j :: l1) then true else g f_n_i1 j1 l1 
    end. 

Fixpoint f (n i : nat) (l : list nat) : bool := 
    match i with 
    | 0 => ListTest (rev l) 
    | S i1 => g (f n i1) (n + n) (i :: l) 
    end. 

Definition SearchCountList (n : nat) : bool := f n n nil. 

간단한 유도가 원본 코드에서 충분하지 않았습니까? 잘 설립 된 귀납법은 어떨까요?