在依赖的“匹配”模式中没有隐含的ssreflect

Question

在我看来，在ssreflect中，当我们进行依赖模式匹配时，隐式构造函数字段会变成显式字段，而设置各种隐式选项并不会影响这种行为。

以下代码适用于Coq 8.6：

Require Import Coq.Unicode.Utf8.
Set Implicit Arguments.
Set Contextual Implicit.

Inductive Vec (A : Type) : nat → Type :=
  nil  : Vec A 0
| cons : ∀ {n}, A → Vec A n → Vec A (S n).

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons x xs => cons x (append xs ys)
  end.

当我导入ssreflect时，它停止工作，因为它需要一个额外的字段用于append中的cons模式

From mathcomp Require ssreflect.

Fixpoint append {A n m}(xs : Vec A n)(ys : Vec A m) : Vec A (n + m) :=
  match xs with
    nil => ys
  | cons _ x xs => cons x (append xs ys)
  end.

这么做的原因是什么，有没有办法在模式匹配中保留隐含的含义？

Answer 1

Coq 8.5和Coq 8.6之间的模式行为发生了变化，基本上破坏了现有的所有Coq脚本，因为8.6将考虑模式中的隐含参数，如您所注意到的。

而不是为8.6版的特定功能重写所有的库，这会阻止与8.5的兼容性，而是通过在加载插件时设置Asymmetric Patterns选项来恢复到8.5的行为。

您可以返回到默认的8.6行为

Global Unset Asymmetric Patterns.

在您导入ssreflect之后，在您的脚本中。