3

Coqでエラトステネスのふるいを書こうとしています。私には機能がありますcrossout : forall {n:nat}, vector bool n -> nat -> vector bool n。ふるいが素数である数値を見つけると、 を使用crossoutして素数ではないすべての数値をマークし、結果のベクトルを再帰します。明らかに、ふるいはベクトル自体に対して構造的に再帰的ではありませんが、ベクトルの長さに対して構造的に再帰的です。私がしたいのは、次のようなことです：

Fixpoint sieve {n:nat} (v:vector bool n) (acc:nat) {struct n} : list nat :=
  match v with
    | [] => Datatypes.nil
    | false :: v' => sieve v' (S acc)
    | true :: v' => Datatypes.cons acc (sieve (crossout v' acc) (S acc))
  end.

しかし、このように書くと、 Coq は の長さが の部分項でv'はないと文句を言いnます。私はそれが正しいことを知っていますが、関数をどのように構成しても、Coq にそれを納得させることはできないようです。誰も私ができる方法を知っていますか?

4

1 に答える 1

4

これは、Coq の依存型に関する最も一般的な落とし穴の 1 つです。直観的に起こっていることは、 でパターンマッチを行うとすぐにv、そのベクトルの長さが実際には であることを Coq が「忘れ」、 の長さと の前身とのn間の接続を失うことです。ここでの解決策は、Adam Chlipala がコンボイ パターンと呼ぶものを適用し、パターン マッチが関数を返すようにすることです。でのパターン マッチングでも可能ですが、 でのパターン マッチングの方が簡単だと思います。v'nvn

Require Import Vector.

Axiom crossout : forall {n}, t bool n -> nat -> t bool n.

Fixpoint sieve {n:nat} : t bool n -> nat -> list nat :=
  match n with
    | 0 => fun _ _ => Datatypes.nil
    | S n' => fun v acc =>
                if hd v then
                  Datatypes.cons acc (sieve (crossout (tl v) acc) (S acc))
                else
                  sieve (tl v) (S acc)
  end.

のヘッダーがsieve少し変更されていることに注意してください。現在、戻り値の型は、実際には Coq の型推論を支援する関数になっています。

詳細については、Adam の本 ( http://adam.chlipala.net/cpdt/html/MoreDep.html ) を参照してください。

于 2013-06-06T13:48:59.677 に答える