没有削减的弱化假设

Question

我经常发现自己处于以下情况，在这种情况下我证明了一个蕴含的引理：

Lemma L1: A -> B

实际上等价性 A <-> B 是可以证明的，但是蕴涵 B -> A 是微不足道的，不是一个非常有趣的结果。然后在设计一些证明的过程中，我最终得到了假设：

H : A

我实际上想使用 B。我可以使用剪切：

cut (B).

并从那里开始，但我确信有一种更快的方法可以正式削弱假设 H，将语句 A 替换为 B。

我最近一直在做的是回到我的引理并证明蕴涵的两面。

Lemma L1 : A <-> B

然后使用简单的rewrite L1 in H。所以这适用于等价物，但当然不是一般的。那么，如何从简单的蕴涵中削弱没有 cut 的假设呢？

Answer 1

事实上，这很常见，一些 Coq 插件如 ssreflect 为其提供特殊支持，称为 "hypothesis view"。恕我直言，重写在您的情况下可能还不错。

Coq 8.5 引入了一项实验性 p%term 功能来对假设执行 "views"，因此您可以：

Variables (A B C : Prop).
Hypothesis U : A -> B.

Lemma L1 : A -> B.
intros h%U.

但请注意，此功能可能会被删除。当然，如果您愿意使用 ssreflect 策略语言视图是一项基本功能，您可以这样做：

Variables (A B C : Prop).
Hypothesis U : A -> B.

Lemma L1 : A -> B.
by move=> /U.

ssreflect 中的视图提供了更多好处，例如，如果您有一个假设 B 和一个引理 U : A -> B -> C，您通常可以应用 /U，等等...请参阅手册了解更多详情。

Answer 2

一个简单的方法是使用 apply L1 in H..

Variables A B : Prop.
Lemma L1 : A -> B. Admitted.

Theorem theorem : A -> 1 = 1.
  intros H.
  apply L1 in H.

最后一行将H : A变为H : B。

Weakening hypothesis without a cut