2

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

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。

4

2 回答 2

5

我想你可能正在寻找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).

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

于 2017-10-03T03:51:35.727 回答
3

您的代码段的问题是[ H: ?P |- ?P ]在这种情况下始终匹配。第一次匹配H : blah，第二次匹配H : C——因为 C 和 blah 在 Coq 中是可转换的——展开不会改变任何东西，因此中止repeat.

我会写

Ltac my_auto_unfold nam := repeat lazymatch goal with 
  | [ H : nam |- _ ] => unfold nam in H
end.

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

你甚至可以写

Theorem g: blah -> blah -> blah.
Proof.
  intros.
  match goal with
  | [ |- ?p] => my_auto_unfold p
  end.
  auto. Qed.

如果你愿意的话。

于 2017-04-05T16:35:00.643 回答