coq - ssreflect 的依赖 "match"模式中没有隐式

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 将考虑模式中的隐式参数。

ssreflect 没有为 8.6 特定功能重写所有库(这会妨碍与 8.5 的兼容性)，而是选择在加载插件时通过设置 Asymmetry Patterns 选项来恢复到 8.5 行为.

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

Global Unset Asymmetric Patterns.

导入 ssreflect 后在脚本中。