0

我简化了peirce、classic、excluded_middle、de_morgan_not_and_not和implicit_to_or互等价的证明过程，主要写git@github.com:B-Rich/sf.git如下。

Theorem excluded_middle_irrefutable:  forall (P:Prop), ~ ~ (P \/ ~ P).
Proof.
  intros. unfold not. intros.
  apply H. right. intros. apply H. left. apply H0.
Qed.

Definition peirce                := forall P Q: Prop, ((P->Q)->P)->P.
Definition classic               := forall P :  Prop, ~~P -> P.
Definition excluded_middle       := forall P :  Prop, P \/ ~P.
Definition de_morgan_not_and_not := forall P Q: Prop, ~(~P /\ ~Q) -> P\/Q.
Definition implies_to_or         := forall P Q: Prop, (P->Q) -> (~P\/Q).

Theorem peirce_classic : peirce -> classic.
Proof.
  compute. intros.
  specialize (H P False).
  apply H. intros.
  apply H. contradiction H0.
Qed.

Theorem classic_excluded_middle : classic -> excluded_middle.
Proof.
  compute. intros.
  apply H. intros.
  apply H0.
  right.
  intros.
  assert (P \/ (P->False)) as H2.
    apply (or_introl H1).
  apply (H0 H2).
Qed.

Theorem false_dist_1 : forall {P Q : Prop}, (P \/ Q -> False) -> (P -> False) /\ (Q -> False).
Proof.
  intros.
  split.
  intros.
  apply (H (or_introl H0)).
  intros.
  apply (H (or_intror H0)).
Qed.

Theorem false_dist_2 : forall {P Q : Prop}, (P -> False) /\ (Q -> False) -> (P \/ Q -> False).
Proof.
  intros.
  inversion H.
  inversion H0.
  apply (H1 H3).
  apply (H2 H3).
Qed.

Theorem em_de_morgan : excluded_middle -> de_morgan_not_and_not.
Proof.
  compute. intros.
  specialize (H (P \/ Q)).
  inversion H.
  apply H1.
  apply (False_ind (P \/ Q) (H0 (false_dist_1 H1))).
Qed.

Theorem double_neg : forall P : Prop,
  P -> ((P->False)->False).
Proof.
  (* WORKED IN CLASS *)
  intros P H. intros G. apply G. apply H.  Qed.

Theorem de_morgan_to_or : de_morgan_not_and_not -> implies_to_or.
Proof.
  compute. intros.
  specialize (H (P -> False) Q).
  intuition.
Qed.

Theorem to_or_peirce: implies_to_or -> peirce.
Proof.
  compute. intros.
  specialize (H P P).
  intuition.
Qed.

我成功删除了一些intuition战术，除了最后两个。

我的问题是：

  • 如何在不使用intuition策略的情况下证明 to_or_peirce 和 de_morgan_to_or？
  • 战术有什么作用intuition？
  • 有没有办法提取该策略可能产生的具体程序intuition？
4

1 回答 1

1

（首先，我知道这是Benjamin C. Pierce 的软件基础的一部分。这些用于大学课程，所以我不会为您提供这些练习的解决方案并破坏其他人的乐趣。如果您正在做这些你自己的（就像我做的那样），很抱歉，但我希望你能理解——我不想“奖励”他们将这些材料公开的努力，因为他们需要额外的工作来提出新的练习。）

有没有办法提取该策略可能产生的具体程序intuition？

好吧，对于任何已定义的事物，您都可以做得到Print thing.定义。对于手动定义的东西，通常看起来很像你写的东西。对于战术产生的东西，这可能是严重不可读的（甚至包含不必要的冗长间接）。通过练习，您最终将能够大部分时间阅读和重新构建（以更易读的方式）这些证明。

可能会或可能不会起作用的是info <tactic>，它应该输出应用策略的列表/树 - 但它似乎被破坏了（多年来......），在新版本的 Coq 中可能有专门的策略，如 ,info_trivial，info_auto或者info_eauto可能帮你。

直觉策略有什么作用？

的文档intuition相当神秘，但包含有用的片段

[...] 事实上，tauto只是intuition fail.

[…]

变体：

  1. intuition
    相当于intuition auto with *。

（最后一部分意味着您可以尝试intuition info_auto看看这是否为您提供了任何有用的信息。不幸的是，它只会打印一长串，(* info auto : *) idtac.因为这些定理都是重言式并且auto没有任何作用。）

因此，转到以下文档tauto：

这种策略基于 Roy Dyckhoff [ 54 ]的无收缩连续演算 LJT* 实现了直觉命题演算的决策过程。请注意，tauto在直觉主义重言式命题的任何实例上都成功。tauto展开否定和逻辑等价，但不展开任何其他定义。

现在应该很清楚了吧？正确的？;-)

（那时，您可以尝试查看的定义，tauto但这也不是很清楚。）

将这些部分放在一起并举例说明：

正如文档所说，tauto（因此intuition）“为直觉命题演算实施决策程序”。也就是说，任何在连词/\（\/<->->~

Variables A B C D : Prop.
Lemma foo : (A /\ B) -> A.  tauto.  Qed.            (* solves *)
Lemma bar : (A /\ B) -> A.  auto. (* fails *) auto 9999 with *. (* fails *)
Lemma baz : ((B /\ C) /\ D) -> ((A /\ C) -> (D /\ B /\ (A /\ A))).
            tauto.  Qed.  (* solves *)
Lemma qux : (A \/ B) /\ (C \/ (A -> B)) /\ ~B -> C.  tauto.  Qed. (* solves *)
(* etc. *)

对于所有这些，auto只会tauto（“重言式”）立即解决它们。当基本的拆散和组合完成并且还没有解决所有intuition问题时，只会尝试做更多的事情。tauto

（这有帮助吗？）

如何证明to_or_peirce和de_morgan_to_or不使用该intuition策略？

提示：你H有形式… -> (… \/ …)，你可以destruct或case分析它，就像你对析取所做的那样（但在这个“符号海洋”中，可能很难看出这是可能的）。其余的应该相当容易。

于 2015-04-26T21:20:57.900 回答