小编Ran*_*d00的帖子

我正在尝试求解形式的等式

A * B * C * D * E = F

其中*一些复杂的左联想操作。

目前，一切是不透明的（包括*和A通过F），并且可以通过由透明autounfold with M_db。

问题是，如果我全局展开公式中的定义，那么简化将永远存在。相反，我想首先展开A * B，应用一些策略将其简化为正常形式X，然后对X * C诸如此类进行。

知道我将如何做到这一点吗？这是我目前的方法，但是in Aor at A无效。另外，我不清楚这是否是正确的结构，还是reduce_m应该返回某些东西。

Ltac reduce_m M :=
  match M with
  | ?A × ?B => reduce_m A;
              reduce_m B;
              simpl;
              autorewrite with C_db
  | ?A      => autounfold with M_db (* in A *);
              simpl; 
              autorewrite with C_db …

我正在尝试编写一个返回值的策略，在此过程中需要检查某些内容是否是 evar。

不幸的是，我无法使用is_evar，因为这样该策略不被视为返回值（而是另一种策略）。下面是一个例子。

有什么建议么？

Ltac reify_wrt values ls :=
  match ls with
  | nil => constr:(@nil nat)
  | ?a :: ?ls' => let i := lookup a values in
                 let idx := reify_wrt values ls' in
                 constr:(i :: idx)
  | ?e :: ?ls' => is_evar e; 
                  let i := constr:(100) in 
                  let idx := reify_wrt values ls' in
                  constr:(i :: idx)
  end.

我正在尝试为我编写的矩阵库创建一个Hint Rewrite数据库.但是当我写的时候

Hint Rewrite kron_1_r : M_db

我收到以下错误:

Cannot infer the implicit parameter m of kron_1_r whose type is "nat".

kron_1_r具有类型forall {m n : nat} (A : Matrix m n), A ? Id 1 = A,因此应根据调用autorewrite时的上下文推断出m和n.我不确定为什么它想要一个参数,或者如何告诉它推迟.