coq - 提示重写无法推断参数

Question

我正在尝试为我编写的矩阵库创建一个提示重写数据库。但是当我写

提示重写 kron_1_r : M_db

我收到以下错误:

无法推断类型为“nat”的kron_1_r 的隐式参数m。

kron_1_r 的类型为 forall {m n : nat} (A : Matrix m n), A ⊗ Id 1 = A，因此 m 和 n 应该基于调用 autorewrite 时的上下文。我不确定为什么它需要一个参数，或者如何告诉它推迟。

Answer 1

您遇到了最大插入隐式参数 和普通隐式参数之间的区别。不同之处在于，当您使用定义而不提供任何参数时，就像您在 Hint Rewrite kron_1_r 中的方式一样。一种解决方案当然是使用 @kron_1_r，它提供没有任何隐式参数的标识符。

不幸的是，在创建定义时没有语法来为其提供非最大插入的隐式参数；你只能使用 {m : nat}。相反，您需要在创建 kron_1_r 后使用 Arguments kron_1_r [m n] _. 来更改前两个参数的隐式行为(如上面 Anton Trunov 所建议的) .

使用 About 通常很有帮助，它报告隐式参数的状态(您也可以通过 Print 获得这些状态，但是打印时通常会得到太多输出定理，因为证明项很大)。