“自动”如何与双相关联(当且仅当)

Question

我注意到，auto忽略了二分词。下面是一个简化的示例：

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的一种语法糖，所以我写了两个定理来提取其中一个定理：

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. 为什么apply A_iff_B工作，而auto using A_iff_B不工作？我认为auto n是在使用给定数据库中的假设和所有定理对长度为<= n的所有可能序列进行详尽的搜索。
2. 这两个投影函数是否有一个标准的技巧来处理双数，或者这两个投影函数是通常的解？
3. 这样的投影函数是否在标准库的某个地方？我找不到他们。

Answer 1

1. 为什么apply A_iff_B works和auto using A_iff_B没有呢？

auto通常使用simple apply而不是apply，并且这个受限制的apply版本不处理二叉树。

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。下面是你如何找到它们的方法：

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

或者更容易打字，但发现的东西比我们需要的要多一些：

Search (_ /\ _ -> _).