将ltac应用于目标的子表达式

Question

下面是我想要做的一个简短的例子。

假设我有一个关系

Inductive divisible: nat -> nat -> Type := 
| one : forall n, divisible n 1.
..etc...

我还有下面的ltac Ltac simplify := autorewrite with blah：

我想定义一个ltac，它确实简化为一个“可分”目标中的第一个术语。就像这样

Ltac simplify_fst :=
  match goal with |- (divisible ?N ?M) =>
autorewrite with subst1 in N
  end.

当我在下面的代码中尝试上面的方法时，

Lemma silly: forall n m, divisible (n + m) 1.
  intros. simplify_fst.

我得到了一个

Error:
Ltac call to "simplify_fst" failed.
Ltac variable N is bound to n + m which cannot be
coerced to a variable.

是否可以将ltacs (即使是只涉及自动折叠和自动重写的简单ltacs)限制为目标的子表达式？

谢谢。

Answer 1

在您的情况下，remember可能会很有用：

Ltac simplify_fst :=
  match goal with |- (divisible ?N ?M) =>
    let x := fresh "x" in
    let Hx := fresh "Hx" in
    remember N as x eqn:Hx;
    autorewrite with subst1 in Hx;
    subst x
  end.