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

Question

这是我正在尝试做的一个简短示例。

假设我有一个关系

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

我还有以下ltac Ltac simplify := autorewrite with blah

我想定义一个 ltac，它只简化了 'divisible' 目标中的第一项。像

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（即使是仅涉及自动展开和自动重写的简单应用程序）限制为目标的子表达式？

谢谢。

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.

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

apply ltac to subexpression of a goal

coq

ltac