如何在 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。这不会在证明项中添加任何内容，因此使用起来可能更容易。