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_lemmaCoq の終了チェッカーは混乱します ( を使用して項を調べることができます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 に答える