1

我想证明计算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.

它清除所有子目标，但不会在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递归调用中术语中的参数实际上更小，但是我该怎么做呢？

4

1 回答 1

2

H因为您在使用 再次构建类似的东西之前进行了反转constructor ; apply H0，所以您会得到一个term_lemma与您想要的模式匹配的 a ，但会混淆 Coq 的终止检查器（您可以使用 来检查一个术语Print NAME.）。

如果您记得a < b由于您对lt_dec a b. 通过让您的引理进行额外的论证，您现在可以使用Accessibility 谓词的严格子项来获得您的见证：

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.
于 2014-12-04T21:33:35.623 回答