Показаны завершающие рекурсии для cumsum в Coq

Question

Я хочу доказать, что вычисление суммарной суммы между a и b завершается.

Я использую Acc lt x термин, чтобы показать, что рекурсии уменьшается, как этот

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. 

Он очищает все подцели, но он не будет typecheck в Qed заявлении. Coq жалуется:

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". 

Я думаю, я должен каким-то образом использовать L1, чтобы показать, что аргумент в H срок в рекурсивном вызове на самом деле меньше, но как я могу это сделать?

Answer 1

Поскольку вы меняете H, прежде чем строить что-то подобное-иш снова с помощью constructor ; apply H0, вы получите term_lemma с шаблоном соответствия, что эквивалентно тому, что вы хотите, но путает окончания проверки Coq в (Вы можете проверить срок с помощью Print NAME.).

Вам не нужно делать все это дело инверсии, если вы помните, что уже знаете, что a < b благодаря анализу вашего дела на lt_dec a b. Позволяя вашу лемму взять дополнительный аргумент, теперь вы можете использовать строгие подтермы в Acc essibility предиката получить свидетельство:

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.