3

在我看来，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.

当我 import 时它停止工作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.

这是什么原因，有没有办法在模式匹配中仍然隐含？

4

1 回答 1

6

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

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

您可以回到默认的 8.6 行为

Global Unset Asymmetric Patterns.

导入 ssreflect 后在您的脚本中。

于 2017-03-16T22:25:29.970 回答