如何在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的类型的信息(它们都是带有2维参数的矩阵)。这是可能的吗?如果可能，是如何实现的？

(理想情况下，这将用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。这不会给证明项增加任何东西，所以它可能更容易使用。