我如何实现迭代这些假设的COQ策略？ [英] How can I implement a coq tactic that iterates over the hypotheses?

问题描述

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

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。

推荐答案

我认为您可能正在寻找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).

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

这篇关于我如何实现迭代这些假设的COQ策略？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！