1

Coq で弱く指定された型で関数を定義しようとしています。具体的には、一連の再帰コンストラクターによって帰納的に定義された型があり、これらのサブセットを使用して引数が構築された場合にのみ定義される関数を定義したいと考えています。

より具体的には、次の型定義があります。

Inductive Example : Set :=
  | Example_cons0 : nat -> Example
  | Example_cons1 : Example -> Example
  .

これで、グラウンド ケースにのみ適用される関数ができました。(次の定義は明らかに機能しませんが、私の意図を示唆するものです。)

Definition example (x:Example) : nat :=
  match x with
    | Example_cons0 n => n
  end.

理想的には、引数 x が汎用型コンストラクターのサブセット (この場合は Example_cons0) を使用して構築されていることを伝えたいと思います。この事実を述べる述語を定義し、述語の証明を引数として渡すことで、これができると考えました。例えば：

Definition example_pred (x:Example) : Prop :=
  match x with
    | Example_cons0 _ => True
    | _ => False
  end.

そして (Robin Green の推奨に従って) 次のようにします。

Definition example2 (x:Example) : example_pred x -> nat :=
  (use proof to define example2?)

残念ながら、これをどのように行うかはわかりません。これが、弱く指定された型で制限された関数を定義する正しい方法であるかどうかさえわかりません。

ガイダンス、ヒント、または提案をいただければ幸いです。- リー

アップデート：

jozefg による推奨に従って、関数の例を次のように定義できます。

Definition example (x:Example) : example_pred x -> nat :=
  match x with
    | Example_cons0 n => fun _ => n
    | _               => fun proof => match proof with end 
  end.

詳細については、彼のコメントを参照してください。この関数は、次の構文を使用して評価できます。これは、証明項が Coq でどのように表現されるかを示しています。

Coq < Eval compute in Example.example (Example.Example_cons0 0) (I : Example.example_pred (Example.Example_cons0 0)).
    = 0
    : nat
4

2 に答える 2

2

簡単な例としてこれを書く方法は次のとおりです

単純なデータ型を検討する

Inductive Foo :=
| Bar : nat -> Foo
| Baz.

そして今、役に立つ関数を定義します

Definition bar f :=
  match f with
    | Bar _ => True
    | Baz   => False
  end.

そして最後に書きたいこと：

Definition example f :=
  match f return bar f -> nat with
    | Bar n => fun _ => n
    | Baz   => fun p => match p with end
  end.

これは型を持っていforall f : Foo, bar f -> natます。これは、exampleが提供されなかった場合Bar、ユーザーが false (不可能) の証明を提供する必要があることを確認することによって機能します。

これは次のように呼び出すことができます

example (Bar n) I

しかし問題は、いくつかの項が によって構成されていることを手動で証明しBarなければならない場合があることです。

于 2013-12-10T22:28:48.807 に答える
1

はい、あなたは正しい線にいます。あなたがしたい：

Definition example2 (x:Example) (example_pred x) : nat :=

さらに先に進む方法は、何を証明したいかによって異なります。

Curry-Howard対応を使用して、戦術で証明することによって定義を作成すると役立つ場合があります。

Definition example2 (x:Example) (example_pred x) : nat.
Proof.
  some proof
Defined.

sigまた、 andsigT型は、「弱く指定された型」を述語と組み合わせて制約するためによく使用されることを指摘したいと思います。

于 2013-12-10T21:53:04.973 に答える