8

私はCoqが初めてです。

挿入ソートの汎用バージョンを実装しようとしています。私が実装しているのは、 Comparator をパラメーターとして受け取るモジュールです。この Comparator は、比較演算子 (is_eq、is_le、is_neq など) を実装します。

挿入ソートでは、挿入するために、入力リスト内の 2 つの要素を比較し、比較の結果に基づいて、要素を正しい位置に挿入する必要があります。

私の問題は、比較演算子の実装がそうでtype -> type -> propあることです(他のタイプ/プルーフの実装には、このようにする必要があります)。type -> type -> bool回避できる場合は、オペレーターのバージョンを作成したくありません。

節True | Falseで使用するために prop を bool に変換する方法はありますか?if ... then ... else

コンパレータモジュールのタイプ:

Module Type ComparatorSig.

  Parameter X: Set.
  Parameter is_eq : X -> X -> Prop.
  Parameter is_le : X -> X -> Prop.
  Parameter is_neq :  X -> X -> Prop.

  Infix "=" := is_eq (at level 70).
  Infix "<>" := (~ is_eq) (at level 70).
  Infix "<=" := is_le (at level 70).

  Parameter eqDec : forall x y : X, { x = y } + { x <> y }.

  Axiom is_le_trans : forall (x y z:X), is_le x y -> is_le y z -> is_le x z.

End ComparatorSig.

自然数の実装:

Module IntComparator <: Comparator.ComparatorSig.
  Definition X := nat.
  Definition is_le x y := x <= y.
  Definition is_eq x y := eq_nat x y.
  Definition is_neq x y:= ~ is_eq  x y.

  Definition eqDec := eq_nat_dec.

  Definition is_le_trans := le_trans.
End IntComparator.

挿入ソートの挿入部分:

  Fixpoint insert (x : IntComparator .X) (l : list IntComparator .X) :=
    match l with
      | nil => x :: nil
      | h :: tl => if IntComparator.is_le x h then x :: h :: tl else h :: (insert x tl)
    end.

(明らかに、is_le は bool ではなく Prop を返すため、insert fixpoint は機能しません)。

どんな助けでも大歓迎です。

4

1 に答える 1

12

あなたはプロップについて少し混乱しているようです。

is_le x yは Prop タイプで、ステートメントx is less or equal to yです。この記述が正しいことを証明するものではありません。この陳述が正しいという証拠はp : is_le x y、そのタイプの住民 (つまり、その陳述の真実の証人) になります。

これが、 でのパターン マッチがあまり意味をなさない理由IntComparator.is_le x hです。

より良いインターフェースは次のようになります。

Module Type ComparatorSig.

  Parameter X: Set.
  Parameter is_le : X -> X -> Prop.
  Parameter is_le_dec : forall x y, { is_le x y } + { ~ is_le x y }.

特に、 のタイプはis_le_decプロパティ の決定手続きのタイプです。つまり、 の証明または の証明is_leのいずれかを返します。これは 2 つのコンストラクターを持つ型であるため、シュガーを活用できます。x <= y~ (x <= y)if

... (if IntComparator.is_le_dec x h then ... else ...) ...

これは、ある意味で、bool決定しようとしているものの証人を返す拡張された です。問題の型が呼び出されsumbool、ここでそれについて学ぶことができます: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool

一般に、コードについて話しTrueたりFalse、コードを実行したりすることは意味がありません。

まず、これらはPropに存在するため、消去されるため、計算上関連性がありません。

第二に、彼らは唯一の住民ではないからですProp。trueとfalseは type の唯一の値であり、boolこれはパターン マッチが可能であることを意味しますが、型Propには無限の数の要素 (想像できるすべてのステートメント) が含まれているため、 type の要素でパターン マッチを試行しても意味がありません。Prop.

于 2013-01-07T18:19:37.313 に答える