gpt4 book ai didi

coq - `auto` 如何与条件(if)交互

转载 作者:行者123 更新时间:2023-12-04 19:29:01 30 4
gpt4 key购买 nike

我注意到,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 <-> BA -> 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.
  • 怎么来的apply A_iff_B作品和 auto using A_iff_B才不是?一世
    以为auto n正在对所有内容进行详尽的搜索apply 的可能序列长度 <= n 使用假设
    以及给定数据库中的所有定理。
  • 是否有使用双条件的标准技巧或
    这两个投影函数通常的解决方案?
  • 标准库中有这样的投影函数吗?一世
    找不到他们。
  • 最佳答案

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

    auto一般使用 simple apply而不是 apply而这个受限版本的 apply不处理双条件。

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


    您可以使用 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. Are such projection functions somewhere in the standard library?


    是的,他们被称为: proj1proj2 .您可以通过以下方式找到它们:
    Search (?A /\ ?B -> ?A).

    或者更容易打字,但发现的东西比我们需要的要多一点:
    Search (_ /\ _ -> _).

    关于coq - `auto` 如何与条件(if)交互,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/47435258/

    30 4 0
    Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
    广告合作:1813099741@qq.com 6ren.com