多类型列表的 Coq 表示法答案

【问题标题】：Coq notation for multi type list多类型列表的 Coq 表示法
【发布时间】：2014-11-05 23:09:43
【问题描述】：

这是一个人为的多类型列表：

Inductive Apple : Set :=.
Inductive Pear : Set :=.

Inductive FruitList : Set := 
| Empty 
| Cons_apple (a : Apple) (p : FruitList) 
| Cons_pear (p : Pear) (p: FruitList).

Variable a : Apple.
Variable p : Pear.

Definition a_fruitList := Cons_apple a (Cons_pear p Empty).

有没有办法为此定义一个列表表示法，例如，a_fruitList 可以由[p,a] 定义？

【问题讨论】：

这与您的问题无关，但请注意Inductive Apple: Set :=. 将Apple 定义为空集。因此，当您声明 Variable a: Apple 时，您会在开发中引入不一致的情况。你应该改用Parameter Apple: Set。

标签： coq

【解决方案1】：

问题是您的列表有两个 cons 构造函数，而递归符号的常用符号机制要求您始终使用相同的构造函数。强制转换可以帮助您解决部分问题：

Section ApplesAndPears.

Variable Apple Pear : Set.

Inductive FruitList : Set :=
| Nil
| ConsApple (a : Apple) (l : FruitList)
| ConsPear (p : Pear) (l : FruitList).

Inductive Fruit : Set :=
| IsApple (a : Apple)
| IsPear (p : Pear).

Coercion IsApple : Apple >-> Fruit.
Coercion IsPear : Pear >-> Fruit.

Definition ConsFruit (f : Fruit) (l : FruitList) : FruitList :=
  match f with
  | IsApple a => ConsApple a l
  | IsPear p => ConsPear p l
  end.

Notation "[ ]" := (Nil) (at level 0).
Notation "[ x ; .. ; y ]" := (ConsFruit x .. (ConsFruit y Nil) ..) (at level 0).

Variable a : Apple.
Variable p : Pear.

Definition a_fruitList := [ a ; p ].

End ApplesAndPears.

（顺便说一句，我假设您真的打算写[ a ; p ]，而不是[ p ; a ]。如果您确实打算写[ p ; a ]，那么您只需要使用SnocFruit 函数代替，这会将元素添加到列表的末尾。但是，这会使后面解释的问题变得更糟。）

现在，我们定义了一个新函数来替换构造函数，并且可以通过将 Fruit 的构造函数声明为强制转换来使用该函数。

当然，这个解决方案并不完全令人满意，因为您的符号产生的术语引用了ConsFruit，而理想情况下，根据您给出的论点选择ConsApple 或ConsFruit 会很好.我怀疑没有办法用符号机制做到这一点，但我可能是错的。

这就是为什么我建议您只使用 list 类型并声明另一种类型（例如 Fruit）来保存 Apple 和 Pear 而不是使用两个 con 构造函数的原因之一，除非您有一个很好的理由不这样做。

【讨论】：

【解决方案2】：

正如Arthur Azevedo De Amorim 所提到的，问题是Coq 的Notation 机制没有考虑子表达式的类型来区分Cons_apple 和Cons_pear。但是，您可以使用 Type Classes 来执行此操作：

Class Cons_fruit(A:Set) := {
  CONS: A -> FruitList -> FruitList }.

Instance Cons_fruit_apple: Cons_fruit Apple:= { CONS := Cons_apple }.
Instance Cons_fruit_pear: Cons_fruit Pear := { CONS := Cons_pear }.

Notation " [ x ; .. ; y ] " := (CONS x .. (CONS y Empty) .. ).

Definition test := [a; p; p; a ].

我们在这里定义了一个类型类Cons_fruit，其中包含一个函数和两个实例，一个用于consing apples，一个用于consing pears。然后我们可以在符号中使用模板化的 CONS 函数，Coq 会在需要时选择合适的实例。

请注意，这可能会导致难以理解的错误消息。例如，与

Definition bad:= [ 0; p ].

你会得到

Error: Cannot infer the implicit parameter Cons_fruit of CONS.
Could not find an instance for "Cons_fruit nat".

【讨论】：

谢谢。我注意到在编写策略时，您可以使用type of 对表达式的类型进行模式匹配。我认为在定义符号时这是不可能的？
确实，我认为这是不可能的。据我所知，Notation 是在解析时处理的纯语法糖，因此该机制无法访问类型信息。另一方面，Ltac 可以访问键入的术语和键入环境。

【解决方案3】：

这是 Coq 文档中关于 lists 的摘录

Notation " [ ] " := nil : list_scope.
Notation " [ x ] " := (cons x nil) : list_scope.
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.

我会坚持使用; 而不是,，因为后者经常在 Coq 的语法中使用，正确获得符号优先级可能会很棘手。

最好的，

【讨论】：