coq - 如何改进这个证明？

Question

我从事分体学研究，我想证明给定的定理(外延性)可以从我拥有的四个公理中得出。

这是我的代码:

Require Import Classical.
Parameter Entity: Set.
Parameter P : Entity -> Entity -> Prop.

Axiom P_refl : forall x, P x x.

Axiom P_trans : forall x y z,
  P x y -> P y z -> P x z.

Axiom P_antisym : forall x y,
  P x y -> P y x -> x = y.

Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.

Axiom strong_supp : forall x y,
  ~ P y x -> exists z, P z y /\ ~ O z x.

这是我的证明:

Theorem extension : forall x y,
  (exists z, PP z x) -> (forall z, PP z x <-> PP z y) -> x = y.
Proof.
  intros x y [w PPwx] H.
  apply Peirce.
  intros Hcontra.
  destruct (classic (P y x)) as [yesP|notP].
  - pose proof (H y) as [].
    destruct H0.
    split; auto.
    contradiction.
  - pose proof (strong_supp x y notP) as [z []].
    assert (y = z).
    apply Peirce.
    intros Hcontra'.
    pose proof (H z) as [].
    destruct H3.
    split; auto.
    destruct H1.
    exists z.
    split.
    apply P_refl.
    assumption.
    rewrite <- H2 in H1.
    pose proof (H w) as [].
    pose proof (H3 PPwx).
    destruct PPwx.
    destruct H5.
    destruct H1.
    exists w.
    split; assumption.
Qed.

我对完成这个证明感到很高兴。不过，我觉得很乱。而且我不知道如何改进。 (我唯一想到的就是使用模式而不是破坏。)有可能改进这个证明吗？如果是这样，请不要使用 super 复杂的策略:我想了解您将建议的升级。

Answer 1

这是对您的证明的重构:

Require Import Classical.
Parameter Entity: Set.
Parameter P : Entity -> Entity -> Prop.

Axiom P_refl : forall x, P x x.

Axiom P_trans : forall x y z,
  P x y -> P y z -> P x z.

Axiom P_antisym : forall x y,
  P x y -> P y x -> x = y.

Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.

Axiom strong_supp : forall x y,
  ~ P y x -> exists z, P z y /\ ~ O z x.

Theorem extension : forall x y,
  (exists z, PP z x) -> (forall z, PP z x <-> PP z y) -> x = y.
Proof.
  intros x y [w PPwx] x_equiv_y.
  apply NNPP. intros x_ne_y.
  assert (~ P y x) as NPyx.
  { intros Pxy.
    enough (PP y y) as [_ y_ne_y] by congruence.
    rewrite <- x_equiv_y. split; congruence. }
  destruct (strong_supp x y NPyx) as (z & Pzy & NOzx).
  assert (y <> z) as y_ne_z.
  { intros <-. (* Substitute z right away. *)
    assert (PP w y) as [Pwy NEwy] by (rewrite <- x_equiv_y; trivial).
    destruct PPwx as [Pwx NEwx].
    apply NOzx.
    now exists w. }
  assert (PP z x) as [Pzx _].
  { rewrite x_equiv_y. split; congruence. }
  apply NOzx. exists z. split; trivial.
  apply P_refl.
Qed.

主要变化是:

1. 为所有中间假设提供明确且信息丰富的名称(即避免执行 destruct foo as [x []] )

2. 使用花括号将中间断言的证明与主证明分开。

3. 使用 congruence自动化一些低级平等推理的策略。粗略地说，这种策略解决了只需通过等式重写和用x <> x这样的矛盾语句修剪子目标就可以建立的目标。 .

4. 使用 assert ... by tactic 压缩简单的证明步骤，它不会生成新的子目标。

5. 使用 (a & b & c)破坏模式而不是 [a [b c]] ，这更难阅读。

6. 重写为 x_equiv_y以避免执行诸如 specialize... destruct... apply H0 in H1 之类的序列

7. 避免一些不必要的经典推理使用。