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我不能这样做，例如，如果我写iCoqCoq

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将被接受，但我不能同时m使用i两者

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可以同时使用和m的函数吗？iCoq

4

2 回答 2

6

您似乎没有很好地理解析取模式的含义。

在 OCaml 中

例如，假设我在 OCaml 中定义了一个类型either：

type either = Left of int | Right of int

因此，类型的值either只是一个用Leftor标记的整数Right。

我现在可以编写的一个明显的函数是int_of_either，它接受一个类型的值either作为它的参数并产生一个整数作为它的结果：

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

现在，请注意 和 的情况Left具有Right相同的右侧。在这种情况下，析取模式允许我通过让模式匹配的两个臂共享一个右侧来使我的函数更加简洁：

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

当然，这只有在变量x在两种模式中都绑定时才有效。（此外，绑定应该是一致的，因为它们应该就 的类型达成一致x。在这里，它们都这样做，因为两种情况都绑定x到类型的值int。）

也就是说，如果我写，例如

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

编译器将拒绝我的程序并抱怨y在以下情况下没有发生Left：

错误：变量 y 必须出现在 this 的两边 | 图案

在 Coq 中

以类似的方式，如果在 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

错了，不能工作。不仅第一个匹配 amy_type和第二个 a ，而且在分离模式（或模式）中双方都必须捕获相同的变量：在一个案例中定义，在另一个案例中定义并期望两者my_type list都没有意义在分支中定义。mi

所以我不知道你想做什么，但是 Coq 和 OCaml 在这里有相同的限制，应该没有区别。

于 2013-06-13T07:54:58.247 回答