写一个析取模式的函数绑定相同的变量

Question

我有这种类型

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会接受,但我不能同时使用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,并i在同一时间Coq？

Answer 1

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

在OCaml

比如说,我在OCaml中定义了一个类型either:

type either = Left of int | Right of int

因此,type的值either只是一个用Left或标记的整数Right.

我现在可以编写的一个显而易见的函数是int_of_either,它将type的值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必须出现在此|的两侧 图案

在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.

编译器抱怨

错误:此析取模式的组件必须绑定相同的变量.

这正是你得到的错误.

总而言之,我建议暂时忘记析取模式,并首先尝试使用专用右侧为模式匹配的每个臂定义函数,然后再考虑是否可以用稍微紧凑的形式编写函数.