Coq에서 cumsum에 대한 종단 재귀 표시

Question

a과 b 사이의 누적 합계 계산이 종료되었음을 증명하고 싶습니다.

나는 그것은 모든 하위 목표를 지우고이

Require Import Omega. 

Lemma L1 : forall a b, a<b -> (b-(1+a)) < (b-a). 
    intros; omega. Qed. 

Lemma term_lemma: forall a b, Acc lt (b-a) -> Acc lt (b-(1+a)). 
    intros; inversion H; clear H; constructor; intros; apply H0; omega. 
Defined. 

Fixpoint cumsum a b (H: Acc lt (b-a)) {struct H} : nat. 
refine (
    match lt_dec a b with 
    | left a_lt_b => a + cumsum (1+a) b _ 
    | right a_ge_b => if beq_nat a b then a else 0 
    end 
). 
apply (term_lemma _ _ H). 
Qed. 

처럼 재귀가 감소 함을 표시하려면 Acc lt x 용어를 사용하지만 Qed 문에서 유형 체킹이되지 않습니다.

Recursive definition of cumsum is ill-formed 
Recursive call to cumsum has principal argument equal to 
"term_lemma a b H" instead of a subterm of "H". 

내가 어떻게 든 재귀 호출에 H 용어의 인수가 실제로 작은 것을 보여주기 위해 L1를 사용해야합니다 같아요,하지만 난 어떻게해야합니까 : COQ 불평? 당신이 뭔가 만들기 전에 H을 반전하기 때문에

Answer 1

constructor ; apply H0를 사용하여 다시 비슷한 틱, 당신은 당신이 원하는 것 무엇을하는 것과의 일치 패턴으로 term_lemma를 얻을 수 있지만 Print NAME.를 사용하여 COQ의 종료 검사기 (당신은 용어를 검사 할 수 있습니다 혼란).

lt_dec a b에 대한 사례 분석 덕분에 이미 a < b이라는 사실을 알고 계시다면이 모든 반전 비즈니스를 수행 할 필요가 없습니다.

Require Import Omega. 

Lemma term_lemma: forall a b, a < b -> Acc lt (b-a) -> Acc lt (b-(1+a)). 
intros a b altb [H]; apply H; omega. 
Defined. 

Fixpoint cumsum a b (H: Acc lt (b-a)) {struct H} : nat. 
refine (
    match lt_dec a b with 
    | left a_lt_b => a + cumsum (1+a) b _ 
    | right a_ge_b => if beq_nat a b then a else 0 
    end 
). 
apply (term_lemma _ _ a_lt_b H). 
Defined.