coq - 将 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（即使是仅涉及自动展开和自动重写的简单方法）限制在目标的子表达式中？

谢谢你。

标签： coqltac

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.