1

私はこのタイプです

Inductive coef :=
| Mycoef_ex2 : matrix -> coef
with matrix :=
| My_matrix : list (list coef) -> matrix.

Inductive my_type :=
| Mytype_ex1 : list my_type  -> my_type
| Mytype_int : Z -> my_type
| Mytype_coef : coef -> my_type.

Ocaml私は書くことができます：

let test_mytype := function
| Mytype_ex1 [Mytype_coef (Mycoef_ex2 (My_matrix m)); Mytype_int i] :: ps -> ...

m私の関数が両方の引数を必要とiするのと同じ関数で引数を使用したいのですCoqが、たとえば、Coq

Definition test_mytype (m: my_type) :=
 match m with
  | Mytype_ex1 (Mytype_coef (Mycoef_ex2 (My_matrix m)))
  | Mytype_int i :: ps => my_function m i
   ...
 end.

エラーが発生しました:

Toplevel input, characters 82-215:
Error: The components of this disjunctive pattern must bind the same variables.

この関数を以下のように書くと、意志は受け入れられますが、両方を同時にCoq使用することはできませんmi

Definition test_mytype (m: my_type) :=
 match m with
  | Mytype_ex1 (Mytype_coef (Mycoef_ex2 (My_matrix m))) :: ps => ...
  | Mytype_ex1 (Mytype_int i) :: ps => ...
    ...
 end.

私はまた、例えばマッチングを使用しようとしました:

Definition test_mytype (m1, m2: my_type) :=
 match m1, m2 with
  | Mytype_ex1 (Mytype_coef (Mycoef_ex2 (My_matrix m))) :: ps, 
  | Mytype_ex1 (Mytype_int i) :: ps => ...
    ...
 end.

しかし、私の問題は両方mでありi、同じに属する必要がありm: my_typeます。

で とを同時にtest_mytype使用できる関数をどのように書けばよいか知っていますか?miCoq

4

2 に答える 2

6

選言パターンとは何かをよく理解していないようですね。

OCamlで

たとえば、OCaml で type を定義したとしeitherます。

type either = Left of int | Right of int

したがって、 type の値は、 または のいずれかeitherでタグ付けされた単なる整数です。LeftRight

私が今書くことができる明白な関数の 1 つはint_of_either、 type の値をeither引数として取り、その結果として整数を生成する です。

let int_of_either = function
  | Left x -> x
  | Right x -> x

Leftここで、との場合のRight右辺が同じであることに注意してください。その場合、選言パターンを使用すると、パターン マッチの 2 つのアームが 1 つの右辺を共有することで、関数をもう少し簡潔にすることができます。

let int_of_either = function
  | Left x
  | Right x -> x

もちろん、これは変数xが両方のパターンでバインドされている場合にのみ機能します。(さらに、バインディングは、 の型に一致する必要があるという意味で一貫性がある必要がありxます。ここでは、両方のケースxが type の値にバインドされるため、一致しますint。)

つまり、たとえば、

let int_of_either = function
  | Left x
  | Right y -> y

yコンパイラは私のプログラムを拒否し、次の場合に発生しないと文句を言いLeftます:

エラー: 変数 y は、この | の両側で発生する必要があります。パターン

インコック

同様に、Coq で型を定義すると、either

Inductive either :=
  | Left : Z -> either
  | Right : Z -> either.

と関数int_of_either

Definition int_of_either (e : either) : Z :=
  match e with
  | Left x => x
  | Right x => x
  end.

次に、選言パターンを使用して書き換えることができint_of_eitherます

Definition int_of_either (e : either) : Z :=
  match e with
  | Left x
  | Right x => x
  end.

しかし、私が書くならば

Definition int_of_either (e : either) : Z :=
  match e with
  | Left x
  | Right y => y
  end.

コンパイラは文句を言います

エラー: この分離パターンのコンポーネントは、同じ変数をバインドする必要があります。

これはまさにあなたが得ているエラーです。

結論として、ここでは選言パターンを忘れることをお勧めします。まず、パターン マッチの各アーム専用の右辺で関数を定義してから、関数をもう少しコンパクトな形式で記述できるかどうかを検討してください。

于 2013-06-13T08:06:41.527 に答える
2 
 match m with
  | Mytype_ex1 (Mytype_coef (Mycoef_ex2 (My_matrix m)))
  | Mytype_int i :: ps
     => my_function m i

間違っていて動作しません。my_type最初の一致が aと 2 番目の aに一致するだけでなくmy_type list、選言パターン (or-pattern) では両側が同じ変数をキャプチャする必要があります。ブランチで定義されます。mi

何をしようとしているのかはわかりませんが、ここでは Coq と OCaml に同じ制限があり、違いはないはずです。

于 2013-06-13T07:54:58.247 に答える