我如何实现迭代假设的 coq 策略？

Question

作为我的一般问题的最小示例，假设我们有以下内容：

Parameter C: Prop.

Definition blah := C.

我想实施一种策略，该策略会blah在目标的所有假设中自动展开。

我试过这个：

Ltac my_auto_unfold := repeat match goal with 
  | [ H: ?P |- ?P ] => unfold blah in H
end.


Theorem g: blah -> blah -> blah.
Proof.
intros.
my_auto_unfold.

但只有一个假设已经blah展开。

Answer 1

我想你可能正在寻找progress战术。如果你这样做：

Ltac my_auto_unfold := repeat match goal with 
  | [ H: ?P |- ?P ] => progress unfold blah in H
end.

那么它将blah在两个假设中展开。你甚至可以这样做：

Ltac in_all_hyps tac :=
    repeat match goal with
           | [ H : _ |- _ ] => progress tac H
           end.

概括这种模式。请注意，这可能会多次运行每个假设中的策略。

如果您想按顺序遍历所有假设，这将显着困难（特别是如果您想保留 evar 上下文而不是在证明项中添加愚蠢的东西）。这是做到这一点的快速而肮脏的方法（假设您的策略不会与目标混淆）：

Parameter C: Prop.
Definition blah := C.

Definition BLOCK := True.

Ltac repeat_until_block tac :=
  lazymatch goal with
  | [ |- BLOCK -> _ ] => intros _
  | [ |- _ ] => tac (); repeat_until_block tac
  end.
Ltac on_each_hyp_once tac :=
  generalize (I : BLOCK);
  repeat match goal with
         | [ H : _ |- _ ] => revert H
         end;
  repeat_until_block
    ltac:(fun _
          => intro;
             lazymatch goal with
             | [ H : _ |- _ ] => tac H
             end).

Theorem g: blah -> blah -> fst (id blah, True).
Proof.
  intros.
  on_each_hyp_once ltac:(fun H => unfold blah in H).

这个想法是你插入一个虚拟标识符来标记你在目标中的位置（即标记可以引入多少变量），然后你将所有上下文恢复到目标中，这样你就可以重新引入上下文一次一个假设，对你刚刚引入的每个假设运行策略。