問題タブ [convoy-pattern]

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

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

私は次の作業をしようとしています:

最後の「_」の代わりに、「f t」が「Some t'」に等しいという証拠が必要です。試合からの入手方法がわかりませんでした。Vnth は次のように定義されます。

次の質問があります。コードを見てください。

f_optここで、常に type の値を返すバージョンを取得したいと思いますA。このようなもの：

しかし、次のエラーが表示されます。

非網羅的なパターン マッチング: pattern の句が見つかりませんNone。

型で何らかの作業を行う必要があることは理解していますが、正確に何をすべきかわかりません。

有限集合の標準定義を使用します。

いくつかあると仮定しましょうP : forall {m : nat} (x y : fin m) : Set(重要なことは、 の両方の引数がP同じ型であるということです)。デモンストレーションのために、P を次のようにします。

ここで、2 つの数値を比較するカスタム関数を作成します。

アイデアは単純明快です: で and 、 for にマッチするxとy、x = F1簡単y = F1に等値を返します。 forx = FS x'では、 andy = FS y'の手続きを再帰的に呼び出します。x'y'

このアイデアを Coq に直接変換すると、明らかに失敗します。

での試合中にx型y情報が失われるため、 に適用できませんP。型等価証明を渡す標準的なトリックは、ここでは役に立ちません。

では、等価性の証明を使用しxて、 と同じ型 をキャストできるのではないでしょyうか?

また、後でキャストを削除できるようにする必要もあります。fcast eq_refl x = xしかし、任意の等価証明で機能させる必要があるため、それだけでは不十分であることに気付き ました。私が必要としているものを正確に実行する UIP と呼ばれるものを見つけました。

これで、定義全体を完了する準備ができました。

通じます！ただし、有用な値には評価されません。たとえば、次の例では、単純な値 (in_rightまたはin_left) ではなく、5 つのネストされた一致を持つ用語が生成されます。問題は、私が使用した UIP 公理にあると思われます。

結局、私が思いついた定義はほとんど役に立ちません。また、2 つの値を同時にマッチングする代わりに、コンボイ パターンを使用してネストされたマッチングを試みましたが、同じ障害にぶつかりPました。他の方法でできますか？