自动与双条件（iff）如何相互干扰 [英] How does `auto` interract with biconditional (iff)

问题描述

我注意到， auto 忽略了双条件。这是一个简化的示例：

I noticed, that auto is ignoring biconditionals. Here is a simplified example:

Parameter A B : Prop.
Parameter A_iff_B : A <-> B.

Theorem foo1: A -> B.
Proof.
  intros H. apply A_iff_B. assumption.
Qed.

Theorem bar1: B -> A.
Proof.
  intros H. apply A_iff_B. assumption.
Qed.

Theorem foo2_failing: A -> B.
Proof.
  intros H. auto using A_iff_B.
Abort.

Theorem bar2_failing: B -> A.
Proof.
  intros H. auto using A_iff_B.
Abort.

现在，我知道 A<-> B 是 A->的语法糖。 B / \ B-> A ，所以我写了两个定理来提取一个或另一个：

Now, I know that A <-> B is a syntactic sugar for A -> B /\ B -> A so I wrote two theorems to extract one or the other:

Theorem iff_forward : forall {P Q : Prop},
  (P <-> Q) -> P -> Q.
Proof.
  intros P Q H. apply H.
Qed.

Theorem iff_backward : forall {P Q : Prop},
  (P <-> Q) -> Q -> P.
Proof.
  intros P Q H. apply H.
Qed.

Theorem foo3: A -> B.
Proof.
  intros H.
  auto using (iff_forward A_iff_B).
Qed.

Theorem bar3: B -> A.
Proof.
  intros H.
  auto using (iff_backward A_iff_B).
Qed.

1. 为什么应用A_iff_B 有效，而 auto使用A_iff_B 无效吗？我
   认为 auto n 正在对 apply 的所有
   可能序列进行详尽搜索。使用假设
   和给定数据库中的所有定理确定长度为< = n的长度。

1. How come apply A_iff_B works and auto using A_iff_B does not? I thought that auto n is performing an exhaustive search of all possible sequences of apply of length <= n using the hypotheses and all theorems in a given database.

是否存在处理双条件的标准技巧？
这两个投影函数是通常的解决方案吗？

Is there a standard trick for working with biconditionals or are those two projection functions the usual solution?

这样的投影函数是否在标准库中？我
找不到它们。

Are such projection functions somewhere in the standard library? I could not found them.

推荐答案

1. 应用A_iff_B的工作原理和使用A_iff_B 自动操作的原因如何？

1. How come apply A_iff_B works and auto using A_iff_B does not?

auto 通常使用简单套用而不是套用，并且此套用的受限版本无法处理双条件

auto generally uses simple apply instead of apply and this restricted version of apply does not handle biconditionals.

1. 是否有用于处理双条件的标准技巧或这两个投影函数？

您可以使用 Hint Resolve-> （<-）功能：

Hint Resolve -> A_iff_B.
Hint Resolve <- A_iff_B. (* if you remove this one, then `auto` won't be able to prove the `bar3` theorem *)

Theorem foo3: A -> B.
Proof. info_auto. Qed. (* look at the output *)

1. 这样的投影函数是否在标准库中？

是的，它们被称为： proj1 和 proj2 。您可以通过以下方式找到它们：

Yes, they are called: proj1 and proj2. Here is how you can find them:

Search (?A /\ ?B -> ?A).

或者更容易键入，但是发现的东西比我们需要的多：

Or a bit easier to type, but finds a tad more stuff than we need:

Search (_ /\ _ -> _).

这篇关于自动与双条件（iff）如何相互干扰的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！