时间戳

首页 > 解决方案 > 如何在 ltac 中使用类型参数？

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

问题描述

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

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'no

标签： coqcoq-tactic

解决方案

您可以进行语法匹配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而不是replaceeg change n'' with n。这不会在证明项中添加任何内容，因此使用起来可能更容易。

推荐阅读