如何在 ltac 中使用类型参数？

Question

我正在尝试编写以下函数：

Ltac restore_dims :=
  repeat match goal with
  | [ |- context[@Mmult ?m ?n ?o ?A ?B]] => let Matrix m' n' := type of A in 
                                           let Matrix n'' o' := type of B in 
                                           replace m with m' by easy
         end.

也就是说，我想在我的 Ltac 中使用有关 A 和 B 类型的信息（它们都是具有二维参数的矩阵）。这可能吗？如果可能，怎么做？

（理想情况下，这会将有问题的 m 替换为 m'，对于我目标中的所有矩阵乘积，n 和 o 也是如此。）

Answer 1

您可以在 type of A 上进行语法匹配以提取参数。

Ltac restore_dims :=
  repeat match goal with
  | [ |- context[@Mmult ?m ?n ?o ?A ?B]] =>
        match type of A with
        |  Matrix ?m' ?n' => replace m with m' by easy
        end;
        match type of B with
        |  Matrix ?n'' ?o' => replace n with n'' by easy
          (* or whatever you wanted to do with n'' and o' *)
        end
  end.

如果您认为 m 和 m' 可以转换，而不仅仅是相等，并且您关心有很好的证明条件，请考虑使用策略 change 而不是 replace 例如change n'' with n。这不会向证明项添加任何内容，因此可能更容易使用。

如何在 ltac 中使用类型参数？

How can I use type arguments in an ltac?

coq

coq-tactic