时间戳

首页 > 解决方案 > 有没有像 apply lem in * 这样的东西？

coq - 有没有像 apply lem in * 这样的东西？

问题描述

有什么方法可以调用apply lem in H前提中所有可能的 H，例如rewrite lem in *？

Axiom P Q : nat -> Prop.
Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.
  intros. apply lem in H. apply lem in H0.

标签： coq

解决方案

我找不到任何内置的东西，但可以用 Ltac 编写这样的策略。

首先，特殊情况。

Axiom P Q : nat -> Prop.
Axiom lem : forall (n : nat), P n -> Q n.
Goal P O -> P (S O) -> True.
  intros.
  repeat match goal with
    x : _ |- _ => apply lem in x
  end.
Abort.

现在我们可以概括这个

Ltac apply_in_premises t :=
  repeat match goal with
    x : _ |- _ => apply t in x
  end.

并像这样使用它：

Goal P O -> P (S O) -> True.
  intros.
  apply_in_premises lem.
Abort.

不幸的是，如果应用产生其他可以应用的lem东西，这种做法可能会导致无限循环。lem

Axiom P : nat -> Prop.
Axiom lem : forall (n : nat), P n -> P (S n).
Ltac apply_in_premises t :=
  repeat match goal with
    x : _ |- _ => apply t in x
  end.

Goal P O -> P (S O) -> nat -> True.
  intros.
  apply_in_premises lem. (* infinite loop *)
Abort.

如果您对此感到担忧，您可以使用 Yves 在评论中建议的变体。简单地更改apply t in x为apply t in x; revert x将确保该假设不会再次匹配。但是，最终结果将包含目标中的所有假设，例如P -> G，而不是p: P作为前提和G目标。

为了自动intro减少这些假设，我们可以跟踪假设被推翻的次数，然后再次引入它们。

Ltac intro_n n :=
  match n with
  | 0 => idtac
  | S ?n' => intro; intro_n n'
  end.

Ltac apply_in_premises_n t n :=
  match goal with
  | x : _ |- _ => apply t in x; revert x;
                  apply_in_premises_n t (S n)
  | _ => intro_n n (* now intro all the premises that were reverted *)
  end.

Tactic Notation "apply_in_premises" uconstr(t) := apply_in_premises_n t 0.

Axiom P : nat -> Prop.
Axiom lem : forall (n : nat), P n -> P (S n).

Goal P O -> P (S O) -> nat -> True.
  intros.
  apply_in_premises lem. (* only applies `lem` once in each of the premises *)
Abort.

在这里，策略intro_n n适用于intro n时间。

我一般没有对此进行测试，但在上述情况下效果很好。如果一个假设无法恢复（例如，如果其他假设依赖于它），它可能会失败。它还可以对假设重新排序，因为当重新引入还原的假设时，它会被放在假设列表的末尾。

推荐阅读