How to improve this proof?

Question

I work on mereology and I wanted to prove that a given theorem (Extensionality) follows from the four axioms I had.

This is my code:

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.

And this is my proof:

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

I'm happy with the fact that I completed this proof. However, I find it quite messy. And I don't know how to improve it. (The only thing I think of is to use patterns instead of destruct.) It is possible to improve this proof? If so, please do not use super complex tactics: I would like to understand the upgrades you will propose.

Answer

Here is a refactoring of your proof:

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

The main changes are:

1. Give explicit and informative names to all the intermediate hypotheses (i.e., avoid doing destruct foo as [x []])

2. Use curly braces to separate the proofs of the intermediate assertions from the main proof.

3. Use the congruence tactic to automate some of the low-level equality reasoning. Roughly speaking, this tactic solves goals that can be established just by rewriting with equalities and pruning subgoals with contradictory statements like x <> x.

4. Condense trivial proof steps using the assert ... by tactic, which does not generate new subgoals.

5. Use the (a & b & c) destruct patterns rather than [a [b c]], which are harder to read.

6. Rewrite with x_equiv_y to avoid doing sequences such as specialize... destruct... apply H0 in H1

7. Avoid some unnecessary uses of classical reasoning.

Q: Is destruct (strong_supp x y NPyx) as (z & Pzy & NOzx). equivalent to pose proof (strong_supp x y NPyx) as (z & Pzy & NOzx).? I tried and its the same result. Is there a difference?

A: In this particular case, yes, they are equivalent.

A: Classical reasoning can be replaced with an extra assumption that equality of Entity is decidable.