6

私はCoqで遊んでいて、ソートされたリストを作成しようとしています。リスト[1,2,3,2,4]を取得して、次のような関数を返す関数が必要Sorted [1,2,3,4]でした。つまり、不良部分を削除しますが、実際にはリスト全体を並べ替えることはありません。

lesseqタイプの関数を定義することから始めようと思ったのですが(m n : nat) -> option (m <= n)、それからパターンマッチングをかなり簡単に行うことができました。多分それは悪い考えです。

私が今抱えている問題の核心はそれです（スニペット、下部の関数全体）

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
        | 0 => match n with
            | 0 => Some (le_n 0)
            ...

タイプチェックではありません。を期待していると書いてありますoption (m <= n)が、Some (le_n 0)タイプはoption (0 <= 0)です。mその文脈では明らかに両方とnがゼロであるため、私にはわかりませんが、 Coqにそのことを伝える方法がわかりません。

全体の機能は次のとおりです。

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
    | 0 => match n with
        | 0 => Some (le_n 0)
        | S n_  => None
        end
    | S m_  => match n with
        | 0 => None
        | S _   => match lesseq m_ n with
                | Some x=> le_S m n x
                | None  => None
                end
            end
    end.

おそらく私は自分より進んでいて、これに取り組む前に読み続ける必要があります。

4

2 に答える 2

7

次の関数を定義することをお勧めします（適切に注釈を付けたとしても、[le_S mnx]には必要なタイプがありません）：

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n with
     | 0 =>
         match m with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

しかし、お気づきのように、結果の型に表示される変数を破棄するときに、型チェッカーは新しいコンテキストを推測するのに十分賢くありません。次の方法で一致に注釈を付ける必要があります。

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n return (option (m <= n)) with
     | 0 =>
         match m return (option (m <= 0)) with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

パターンマッチングが依存型でどのように機能するかを本当に理解したい場合は、リファレンスマニュアルを参照してください。そのための勇気が足りない場合は、戦術メカニズムを使用して証明を作成することをお勧めします（「洗練された」戦術はそのための優れたツールです）。

     Definition lesseq m n : option (m <= n).
     refine (fix lesseq (m : nat) (n : nat) {struct n} := _).

     destruct n.
     destruct m.
     apply Some; apply le_n.
     apply None.

     destruct (lesseq m n).
     apply Some.
     apply le_S.
     assumption.
     apply None.
     Defined.

ちなみに、次の補題を証明する必要があるため、関数が実際に役立つとは思いません（たとえそれが良いアイデアであっても）：Lemma lesseq_complete：forall mn、lesseqmn<>なし->m> n。

これが、人々がCoq.Arith.Compare_decを使用する理由です。楽しむ。

于 2011-05-23T14:29:23.073 に答える
6

この関数を演習として作成しますか、それともより大きな目標を達成するためだけに作成しますか？後者の場合、ここで仕事をする決定関数でいっぱいの標準ライブラリ、Coq.Arith.Compare_decを見る必要があります。たとえばを参照してくださいle_gt_dec。

また、提案する関数は、かどうかの情報のみを提供することに注意してくださいm <= n。パターンマッチングの場合、合計タイプの{ ... } + { ... }方がはるかに便利で、2つの可能なケースを処理できます。

于 2011-05-23T14:09:31.030 に答える