如何改善此证明？

Question

我从事Mereology的工作，我想证明给定定理（扩展）遵循我拥有的四个公理。

这是我的代码：

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.

我对我完成了此证明的事实感到满意。但是，我发现它很混乱。而且我不知道如何改进它。 （我唯一想到的是使用模式而不是破坏。）有可能改善此证明吗？如果是这样，请不要使用超级复杂的策略：我想了解您建议的升级。

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 foo as [x [x []]）

2. 使用卷曲括号将中间断言的证据与主要证明分开。

3. 使用一致性策略来自动化一些低级平等推理。粗略地说，这种策略可以通过以平等的方式重写和用矛盾的陈述来修剪子目标来解决目标，例如x＆lt;＆gt;＆gt; X。

4. 使用sossert ...通过tactic condense divial的证明步骤，该步骤不会生成新的子目标。

5. 使用（a＆amp; b＆amp; c）破坏性模式，而不是[a [bc]]，很难阅读。

6. 用x_equiv_y重写，避免执行序列，例如专业... destruct ... destruct ...在h1

   中应用H0

7. 中应用H0，请避免对经典推理的一些不必要的用法。