与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,因为它需要一个额外的字段用于cons模式append:

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的兼容性,ssreflect选择Asymmetric Patterns在加载插件时通过设置选项恢复到8.5行为.

你可以回到默认的8.6行为

Global Unset Asymmetric Patterns.

导入ssreflect后在脚本中.