1

pのCoqの[Co-]誘導型に関するチュートリアル。図４７では、再帰関数が定義されており、各再帰ステップは整形式命題を使用して、再帰が終了することを示している。

で呼び出される関数は、 whereでx再帰呼び出しを行うため、終了する必要があります。x-yy<>0

エラーなしでCoqに入力できません。Coq は呼び出しの再帰引数が小さくないことを訴えていますが、チュートリアルではそうであると主張しています。

私は何が欠けていますか？

短くするためにコードを少し書き直しましたが、論文の逐語的な定義も試しました。

まず、x-yが x からアクセスできることを示します。

Require Import Omega.

Definition minus_decrease:
  forall x y, Acc lt x -> x<>0 -> y<>0 -> Acc lt (x-y).
  intros x y H Hx Hy.
  case H; intro Ha; apply Ha.
  omega.
Qed.

次に、関数を定義しようとすると、このように

Definition div_aux :=
  fix div_aux (x y:nat) (H:Acc lt x) {struct H}: nat :=
  match eq_nat_dec x 0 with
    |left _ => 0
    |right _ =>
     match eq_nat_dec y 0 with
       |left _ => 0
       |right v => S (div_aux (x-y) y (minus_decrease x y H _ v))
     end
  end.

それからCoqは拒否し、

div_aux への再帰呼び出しには、"H" の部分項ではなく、"minus_decrease xy H ​​?156 v" に等しい主引数があります。

div_aux x ...を使用して自分自身を再帰的に呼び出す方法に注目し、型の項div_aux (x-y) ...を(minus_decrease ...)返します。Acc lt (x-y)

Accこの関数が実際に終了することを示すにはどうすればよいですか?

4

1 に答える 1

3

The following works のQed.代わりに定義を終了したことがエラーのようです。Defined.

Require Import Omega.

Definition minus_decrease: forall x y, Acc lt x -> x<>0 -> y<>0 -> Acc lt (x-y).
  intros x y H Hx Hy.
  case H; intro Ha; apply Ha.
  omega.
Defined.


Fixpoint div_aux (x y:nat) (H:Acc lt x) {struct H}: nat.
Proof.
  refine (if eq_nat_dec x 0
          then 0
          else if eq_nat_dec y 0
               then y
               else S (div_aux (x-y) y _)).
  apply (minus_decrease _ _ H _H _H0).
Qed.
于 2014-11-26T15:54:46.133 に答える