Formalisation of "Axiomatic Set Theory in Type Theory" by Gert Smolka

Version: 16 May 2015
Author: Dominik Kirst, Saarland University
This file covers Sections 2, 6 and 7 of the paper

Global Set Implicit Arguments.
Global Unset Strict Implicit.

Require Export Classical_Pred_Type Classical_Prop.

Ltac indirect :=
  match goal with
    | [ |- ?H ] => destruct (classic H); auto; exfalso
  end.

Well-Orderings in Type Theory

Notation for sub-classes and sub-orderings

Notation "p '<<=' q" := (forall x, p x -> q x) (at level 70).
Notation "p '===' q" := (p <<= q /\ q <<= p) (at level 70).
Notation "R 'o=' S" := (forall x y, R x y -> S x y) (at level 70).
Notation "R 'o=o' S" := (R o = S /\ S o = R) (at level 70).

Lemma sub_trans1 X (p: X -> Prop) q r:
  p <<= q -> q <<= r -> p <<= r.
Proof.
  auto.
Qed.

Lemma sub_trans2 X Y (R: X -> Y -> Prop) S T:
  R o = S -> S o = T -> R o = T.
Proof.
  auto.
Qed.

Definitions for binary relations

Definition inv X Y (U: X -> Y -> Prop) x y :=
  U y x.

Definition dom X Y (U: X -> Y -> Prop) x :=
  exists y, U x y.

Definition functional X Y (U: X -> Y -> Prop) :=
  forall x y y', U x y -> U x y' -> y = y'.

Definition expansion X Y (U: X -> Y -> Prop) a b :=
  fun x y => U x y \/ x = a /\ y = b.

Lemma inv_sub X Y (U: X -> Y -> Prop) (V: X -> Y -> Prop):
  U o = V -> (inv U ) o = (inv V ).
Proof.
  firstorder.
Qed.

Theory of Well-Orderings

Definitions for orderings

Definition reflexive X (R: X -> X -> Prop) :=
  forall x y, R x y -> R x x /\ R y y.

Definition antisym X (R: X -> X -> Prop) :=
  forall x y, R x y -> R y x -> x = y.

Definition transitive X (R: X -> X -> Prop) :=
  forall x y z, R x y -> R y z -> R x z.

Definition linear X (R: X -> X -> Prop) :=
  forall x y, dom R x -> dom R y -> R x y \/ R y x.

Definition porder X (R: X -> X -> Prop) :=
  reflexive R /\ antisym R /\ transitive R.

Definition Least X (R: X -> X -> Prop) p x :=
  p x /\ forall y, p y -> R x y.

Definition Segs X (R: X -> X -> Prop) (p: X -> Prop) :=
  (p <<= dom R ) /\ (forall x y, R x y -> p y -> p x ).

Definition Seg X (R: X -> X -> Prop) x y :=
  R y x /\ x <> y.

Definition res X (R: X -> X -> Prop) p x y :=
  p x /\ p y /\ R x y.

Definition least_inhab X (R: X -> X -> Prop) :=
  forall (p: X -> Prop), ex p -> p <<= dom R -> ex (Least R p).

Definition worder X (R: X -> X -> Prop) :=
  porder R /\ least_inhab R.

Definition res_seg X (R: X -> X -> Prop) a x y :=
  (Seg R a) x /\ (Seg R a) y /\ R x y.

Lemma res_sub1 X (R: X -> X -> Prop) p:
  dom (res R p) <<= dom R.
Proof.
  firstorder.
Qed.

Lemma res_sub2 X (R: X -> X -> Prop) p:
  dom (res R p) <<= p.
Proof.
  firstorder.
Qed.

Lemma res_sub X (R: X -> X -> Prop) (p: X -> Prop) x:
  worder R -> p x -> dom R x -> dom (res R p) x.
Proof.
  firstorder.
Qed.

Lemma seg_segs X (R: X -> X -> Prop) x:
  worder R -> dom R x -> Segs R (Seg R x).
Proof.
  intros [[_[R1 R2]] _] DX. split.
  - intros y [Y _]. now exists x.
  - intros y z YZ [X1 X2]. split.
    + now apply (R2 y z x).
    + intros XY. subst. apply X2. now apply R1.
Qed.

Facts about well-orderings (8)

Lemma least_inhab_linear X (R: X -> X -> Prop):
  least_inhab R -> linear R.
Proof.
  intros H x y XD YD.
  destruct (H (fun z => x = z \/ y = z)) as [z[[Z1|Z1] Z2]]; subst.
  - exists x. now left.
  - intros z [Z|Z]; subst; assumption.
  - left. apply (Z2 y). now right.
  - right. apply (Z2 x). now left.
Qed.

Lemma worder_linear X (R: X -> X -> Prop):
  worder R -> linear R.
Proof.
  intros H. apply least_inhab_linear. apply H.
Qed.

Lemma linear_Segs X (R: X -> X -> Prop) p q:
  linear R -> Segs R p -> Segs R q -> p <<= q \/ q <<= p.
Proof.
  intros RL [P1 P2] [R1 R2]. indirect. apply not_or_and in H as [H1 H2].
  apply not_all_ex_not in H1 as [x H1]. apply imply_to_and in H1.
  apply not_all_ex_not in H2 as [y H2]. apply imply_to_and in H2.
  destruct (RL x y); firstorder.
Qed.

Lemma worder_Segs X (R: X -> X -> Prop) p:
  worder R -> Segs R p -> (p === dom R ) \/ (exists x, dom R x /\ p === Seg R x ).
Proof.
  intros [H1 H2] [H3 H4].
  destruct (classic (p === dom R)) as [H|H]; auto.
  assert (LR: linear R) by now apply least_inhab_linear.
  apply not_and_or in H as [H|H]; try contradiction.
  apply not_all_ex_not in H.
  destruct (H2 (fun x => ~(dom R x -> p x )) H) as [x[X1 X2]].
  - intros x XP. now apply imply_to_and in XP.
  - right. exists x. apply imply_to_and in X1 as [X1 X3].
    split; try assumption. split; intros y Y.
    + split; try (intros I; now subst).
      destruct (LR x y) as [XY|YX]; auto. contradict X3. now apply (H4 x y).
    + indirect. apply Y. apply H1; try apply Y. apply X2.
      intros I. apply H0. apply I. exists y. firstorder.
Qed.

Lemma worder_sub X (R: X -> X -> Prop) p:
  worder R -> worder (res R p).
Proof.
  intros [[H1[H2 H3]]H4]. repeat split;
  try apply (H1 x y); try apply H; try apply H0.
  - firstorder.
  - apply (H3 x y z); firstorder.
  - intros q [x Q] D. destruct (H4 (fun z => q z /\ p z)) as [y Y]; firstorder.
Qed.

Lemma worder_equiv X (R: X -> X -> Prop) (S: X -> X -> Prop):
  worder R -> R o =o S -> worder S.
Proof.
  intros [[R1[R2 R3]] R4] RS. repeat split.
  - apply RS. apply RS in H. now apply (R1 x y).
  - apply RS. apply RS in H. now apply (R1 x y).
  - firstorder.
  - intros x y z XY YZ. apply RS. apply RS in XY.
    apply RS in YZ. now apply (R3 x y z).
  - intros p PI PS. destruct (R4 p PI) as [x XL].
    + intros x PX. destruct (PS x PX) as [y Y]. apply RS in Y. now exists y.
    + exists x. firstorder.
Qed.

Well-founded induction (9)

Inductive W X (R: X -> X -> Prop) x: Prop :=
| WI: Seg R x <<= W R -> W R x.

Definition wfounded X (R: X -> X -> Prop) :=
  dom R <<= W R.

Lemma worder_wfounded X (R: X -> X -> Prop):
  worder R -> wfounded R.
Proof.
  intros [H1 H2]. indirect.
  apply not_all_ex_not in H as [x XL].
  apply imply_to_and in XL as [X1 X2].
  destruct (H2 (fun y => dom R y /\ ~ W R y)) as [y[Y1 Y2]].
  - exists x. now split.
  - tauto.
  - apply Y1. constructor. intros z Z. indirect. apply Z.
    apply H1; try apply Z. apply Y2. split; firstorder.
Qed.

Similarities and Isomorphisms

Definitions of Similarities

Definition simulative X Y (U: X -> Y -> Prop) R S :=
  forall x x' y, U x y -> R x' x -> exists y', U x' y' /\ S y' y.

Definition simulation X Y (U: X -> Y -> Prop) R S :=
  dom U <<= dom R /\ simulative U R S.

Definition similarity X Y (U: X -> Y -> Prop) R S :=
  simulation U R S /\ functional U /\
  simulation (inv U) S R /\ functional (inv U).

Definition isomorphism X Y (U: X -> Y -> Prop) R S :=
  similarity U R S /\ dom R <<= dom U /\ dom S <<= dom (inv U).

Definition simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) :=
  exists U, isomorphism U R S.

Definition maxisim X Y (U: X -> Y -> Prop) R S :=
  similarity U R S /\ (dom R <<= dom U \/ dom S <<= dom (inv U)).

Definition Canon X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) x y :=
  exists U, similarity U R S /\ U x y.

Facts about similarities

Lemma simi_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> similarity (inv U) S R.
Proof.
  firstorder.
Qed.

Lemma iso_inv X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
isomorphism U R S -> isomorphism (inv U) S R.
Proof.
  firstorder.
Qed.

Lemma simi_simu1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative U R S.
Proof.
  firstorder.
Qed.

Lemma simi_simu2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
similarity U R S -> simulative (inv U) S R.
Proof.
  firstorder.
Qed.

Lemma simi_com X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simi R S -> simi S R.
Proof.
  intros [U[U1 U2]]. exists (inv U). split; firstorder.
Qed.

Lemma simulation_dom X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  simulation U R S -> Segs R (dom U).
Proof.
  intros [H1 H2]. split; trivial. intros x' x XX [y H].
  destruct (H2 x x' y H XX) as [y' [I _]]. now exists y'.
Qed.

Lemma simi_eq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> x = x' -> y = y'.
Proof.
  intros SU H1 H2 H. subst x'. firstorder.
Qed.

Lemma simi_eq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> y = y' -> x = x'.
Proof.
  intros SU H1 H2 H. subst y'. firstorder.
Qed.

Lemma simi_neq1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> y <> y' -> x <> x'.
Proof.
  intros SU H1 H2 H3 H4. apply H3. eauto using simi_eq1.
Qed.

Lemma simi_neq2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y x' y':
  similarity U R S -> U x y -> U x' y' -> x <> x' -> y <> y'.
Proof.
  intros SU H1 H2 H3 H4. apply H3. eauto using simi_eq2.
Qed.

Lemma simi_rewrite X Y (R: X -> X -> Prop) (S S': Y -> Y -> Prop) U:
  similarity U R S -> S o =o S' -> similarity U R S'.
Proof.
  intros SU SS. repeat split; try apply SU.
  - intros x x' y XY XX. destruct (simi_simu1 SU XY XX) as [y'[Y1 Y2]].
    exists y'. split; trivial. now apply SS.
  - intros x XD. apply SU in XD as [y YD]. exists y. now apply SS.
  - intros x x' y XY XX. apply SS in XX.
    destruct (simi_simu2 SU XY XX) as [y'[Y1 Y2]]. exists y'. split; trivial.
Qed.

Facts about domains and restrictions of similarities (13)

Lemma simi_dom1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  similarity U R S -> Segs R (dom U).
Proof.
  intros [H _]. apply (simulation_dom H).
Qed.

Lemma simi_dom2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  similarity U R S -> Segs S (dom (inv U)).
Proof.
  intros [_[_[H _]]]. apply (simulation_dom H).
Qed.

Lemma similarity_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> similarity U R (res S (dom (inv U))).
Proof.
  intros WOR WOS US. repeat split; try apply US.
  - assert (SU: simulative U R S) by apply US.
    intros x x' y UX RX. destruct (SU x x' y UX RX) as [y'[Y1 Y2]].
    exists y'. split; firstorder.
  - intros x XD. assert (XS: dom S x) by now apply US.
    destruct XS as [y XY]. exists x. repeat split; trivial.
    destruct WOS as [[SR _]_]. now apply (SR x y).
  - assert (SU: simulative (inv U) S R) by apply US.
    intros y y' x UY [_ [_ SY]]. destruct (SU y y' x UY SY) as [x'[X1 X2]].
    exists x'. split; assumption.
Qed.

Lemma simi_res X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> dom U === dom R -> isomorphism U R (res S (dom (inv U))).
Proof.
  intros WOR WOS US H. split; auto using similarity_res.
  split; try apply H. firstorder.
Qed.

Lemma similarity_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> similarity U (res R (dom U)) S.
Proof.
  intros WOR WOS US. repeat split; try apply US.
  - intros x XD. assert (XS: dom R x) by now apply US.
    destruct XS as [y XY]. exists x. repeat split; trivial.
    destruct WOR as [[RR _]_]. now apply (RR x y).
  - assert (SU: simulative U R S) by apply US.
    intros x x' y UX [_ [_ RX]]. destruct (SU x x' y UX RX) as [y'[Y1 Y2]].
    exists y'. split; assumption.
  - assert (SU: simulative (inv U) S R) by apply US.
    intros y y' x UY SY. destruct (SU y y' x UY SY) as [x'[X1 X2]].
    exists x'. split; firstorder.
Qed.

Lemma simi_res' X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S ->
  similarity U R S -> dom (inv U) === dom S -> isomorphism U (res R (dom U)) S.
Proof.
  intros WOR WOS US H. split; auto using similarity_res'.
  split; try apply H. firstorder.
Qed.

Agreement and linearity of similarities (14)

Lemma simi_wfounded X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U x y:
  worder R -> worder S ->
  similarity U R S -> U x y -> W R x.
Proof.
  intros WOR WOS SU XY. apply worder_wfounded; trivial. apply SU. now exists y.
Qed.

Lemma simi_agree X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V x y y':
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> U x y -> V x y' -> y = y'.
Proof.
  intros WOR WOS SU SV XY.
  assert (H: W R x) by apply (simi_wfounded WOR WOS SU XY).
  revert y XY y'. induction H as [x H IH]. intros y XY y' XY'.
  indirect. destruct (@worder_linear Y S WOS y y').
  - apply SU. now exists x.
  - apply SV. now exists x.
  - destruct (simi_simu2 SV XY' H1) as [x'[X1 X2]].
    destruct (simi_simu1 SU XY X2) as [z[Z1 Z2]].
    assert (XX': x <> x') by eauto using simi_neq1.
    assert (ZY': y <> z) by eauto using simi_neq2.
    apply ZY'. symmetry. apply (IH x'); firstorder.
  - destruct (simi_simu2 SU XY H1) as [x'[X1 X2]].
    destruct (simi_simu1 SV XY' X2) as [z[Z1 Z2]].
    assert (XX': x <> x') by eauto using simi_neq1.
    assert (ZY': z <> y') by eauto using simi_neq2.
    apply ZY'. symmetry. apply (IH x'); firstorder.
Qed.

Lemma simi_domain_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> dom U <<= dom V -> U o = V.
Proof.
  intros WOR WOS SU SV UV x y XY. destruct (UV x) as [y' H].
  - now exists y.
  - now rewrite (simi_agree WOR WOS SU SV XY H).
Qed.

Lemma simi_lin X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S ->
  similarity U R S -> similarity V R S -> U o = V \/ V o = U.
Proof.
  intros WOR WOS SU SV. assert (LR: linear R) by now apply worder_linear.
  destruct (linear_Segs LR (simi_dom1 SU) (simi_dom1 SV)) as [H|H].
  - left. now apply (simi_domain_sub WOR WOS).
  - right. now apply (simi_domain_sub WOR WOS).
Qed.

Lemma maxi_sub X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U V:
  worder R -> worder S -> similarity U R S -> maxisim V R S -> U o = V.
Proof.
  intros WOR WOS SU [SV[M|M]].
  - apply (simi_domain_sub WOR WOS); trivial.
    apply (@sub_trans1 X (dom U) (dom R)); trivial. apply SU.
  - apply inv_sub. apply (simi_domain_sub WOS WOR); try now apply simi_inv.
    apply (@sub_trans1 Y (dom (inv U)) (dom S)); trivial. apply SU.
Qed.

Embedding theorem (15)

Lemma canon_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simulative (Canon R S) R S.
Proof.
  intros x x' y [U[SU XY]] XX.
  assert (SS: simulative U R S) by apply SU.
  destruct (SS x x' y XY XX) as [y'[Y1 Y2]].
  exists y'. split; trivial. exists U. now split.
Qed.

Lemma canon_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  simulative (inv (Canon R S)) S R.
Proof.
  intros x x' y [U[SU XY]] XX.
  assert (SS: simulative (inv U) S R) by apply SU.
  destruct (SS x x' y XY XX) as [y'[Y1 Y2]].
  exists y'. split; trivial. exists U. now split.
Qed.

Lemma canon_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S -> similarity (Canon R S) R S.
Proof.
  intros WOR WOS. repeat split.
  - firstorder.
  - apply canon_simulative1.
  - intros x y y' [U[SU XY]] [V[SV XY']].
    apply (simi_agree WOR WOS SU SV XY XY').
  - firstorder.
  - apply canon_simulative2.
  - intros x y y' [U[SU XY]] [V[SV XY']].
    apply simi_inv in SU. apply simi_inv in SV.
    apply (simi_agree WOS WOR SU SV XY XY').
Qed.

Lemma exp_simulative1 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  simulative (expansion U a b) R S.
Proof.
  intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B].
  intros x x' y [XY|[XA YB]] XX; subst.
  - destruct (U2 x x' y XY XX) as [y'[Y1 Y2]]. exists y'. firstorder.
  - destruct (classic (dom U x')) as [[y XY]|H].
    + exists y. split; try now left.
      destruct (worder_linear WS (x:=y) (y:=b)); auto. apply U4. now exists x'.
      assert (US: similarity U R S) by firstorder.
      exfalso. apply UB. destruct (simi_dom2 US) as [_ SU].
      apply (SU b y); trivial. now exists x'.
    + exists b. split; try apply B; auto. right. split; trivial.
      apply WR; trivial. apply A. split; trivial. now exists a.
Qed.

Lemma exp_simulative2 X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  simulative (inv (expansion U a b)) S R.
Proof.
  intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B].
  intros x x' y [XY|[XA YB]] XX; subst.
  - destruct (U5 x x' y XY XX) as [y'[Y1 Y2]]. exists y'. firstorder.
  - destruct (classic (dom (inv U) x')) as [[y XY]|H].
    + exists y. split; try now left.
      destruct (worder_linear WR (x:=y) (y:=a)); auto. apply U1. now exists x'.
      assert (US: similarity U R S) by firstorder.
      exfalso. apply UA. destruct (simi_dom1 US) as [_ SU].
      apply (SU a y); trivial. now exists x'.
    + exists a. split; try apply B; auto. right. split; trivial.
      apply WS; trivial. apply B. split; trivial. now exists b.
Qed.

Lemma exp_simi X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U a b:
  worder R -> worder S -> similarity U R S ->
  Least R (fun c => dom R c /\ ~ dom U c) a ->
  Least S (fun c => dom S c /\ ~ dom (inv U) c) b ->
  similarity (expansion U a b) R S.
Proof.
  intros WR WS [[U1 U2][U3[[U4 U5] U6]]] [[RA UA] A] [[SB UB] B]. repeat split.
  - intros x [y[H|[H1 H2]]]; subst; auto. apply U1. now exists y.
  - apply exp_simulative1; firstorder.
  - intros x y y' [XY|[XA YB]] [XY'|[XA' YB']]; subst; eauto.
    + contradict UA. now exists y.
    + contradict UA. now exists y'.
  - intros x [y[H|[H1 H2]]]; subst; auto. apply U4. now exists y.
  - apply exp_simulative2; firstorder.
  - intros x y y' [XY|[XA YB]] [XY'|[XA' YB']]; subst; eauto.
    + contradict UB. now exists y.
    + contradict UB. now exists y'.
Qed.

Lemma canon_max X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S -> maxisim (Canon R S) R S.
Proof.
  intros WOR WOS. split; try now apply canon_simi.
  indirect. apply not_or_and in H as [H1 H2].
  apply not_all_ex_not in H1 as [a' A]. apply imply_to_and in A as [A1 A2].
  apply not_all_ex_not in H2 as [b' B]. apply imply_to_and in B as [B1 B2].
  assert (RL: least_inhab R) by now apply WOR.
  destruct (RL (fun c => dom R c /\ ~ dom (Canon R S) c)) as [a A].
  exists a'. now split. tauto.
  assert (SL: least_inhab S) by now apply WOS.
  destruct (SL (fun c => dom S c /\ ~ dom (inv (Canon R S)) c)) as [b B].
  exists b'. now split. tauto.
  apply A. exists b. exists (expansion (Canon R S) a b). split.
  - apply exp_simi; auto using canon_simi.
  - now right.
Qed.

Lemma canon_unique X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop) U:
  worder R -> worder S -> maxisim U R S -> U o =o Canon R S.
Proof.
  intros WOR WOS MU. split.
  - apply (maxi_sub WOR WOS); auto using canon_max. apply MU.
  - apply (maxi_sub WOR WOS); auto using canon_simi.
Qed.

Lemma embedding X Y (R: X -> X -> Prop) (S: Y -> Y -> Prop):
  worder R -> worder S ->
  (exists p, Segs R p /\ simi (res R p) S ) \/
  (exists q, Segs S q /\ simi R (res S q)).
Proof.
  intros WOR WOS. destruct (canon_max WOR WOS) as [C1[C2|C2]].
  - right. exists (dom (inv (Canon R S))). split.
    + apply (simi_dom2 C1).
    + exists (Canon R S). apply (simi_res WOR WOS C1). firstorder.
  - left. exists (dom (Canon R S)). split.
    + apply (simi_dom1 C1).
    + exists (Canon R S). apply (simi_res' WOR WOS C1). firstorder.
Qed.

Segments are equivalent iff they are isomorphic (16)

Lemma seg_equal X (R: X -> X -> Prop) x y:
  worder R -> dom R x -> dom R y -> Seg R x === Seg R y -> x = y.
Proof.
  intros WOR DX DY [XY YX]. indirect.
  assert (LR: linear R) by now apply worder_linear.
  destruct (LR x y DX DY) as [I|I].
  - apply (YX x); firstorder.
  - apply (XY y); firstorder.
Qed.

Lemma simi_sub X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p <<= q.
Proof.
  intros WOR SP SQ [U[U1[U2 U3]]]. cut (forall x, dom (res R p) x -> U x x).
  - intros H x PX. assert (UX: dom U x).
    + apply U2. apply res_sub; firstorder.
    + apply (res_sub2 (R:=R)). apply U1. exists x. apply H. now apply U1.
  - assert (WR: wfounded R) by now apply worder_wfounded.
    intros x DX. assert (XR: dom R x) by now apply (res_sub1 (p:=p)).
    specialize (WR x XR). induction WR as [x H IH].
    destruct (U2 x DX) as [y Y]. cut (x = y); try congruence.
    destruct U1 as [[H1 H2][H3[[H4 H5]H6]]]. apply (seg_equal WOR); auto.
    + apply (res_sub1 (p:=q)). apply H4. now exists x.
    + split; intros z Z.
      * assert (ZX: res R p z x) by firstorder.
        destruct (H2 x z y Y) as [z'[Z1' Z2']]; trivial.
        assert (ZD1: dom (res R p) z) by now exists x.
        assert (ZD2: dom R z) by (exists x; apply Z).
        specialize (IH z Z ZD1 ZD2). rewrite (H3 z z z' IH Z1').
        split; try apply Z2'. intros YZ. subst.
        apply Z. now apply (H6 z').
      * assert (DY: dom (inv U) y) by now exists x.
        assert (QY: q y) by apply (res_sub2 (H4 y DY)).
        assert (ZX: res R q z y) by firstorder.
        destruct (H5 y z x Y) as [z'[Z1' Z2']]; trivial.
        assert (ZD1: dom (res R p) z') by now exists x.
        assert (ZD2: dom R z') by (exists x; apply Z2').
        assert (Z': Seg R x z'). { split. apply Z2'. intros J. subst.
        apply Z. now apply (H3 z' y z). }
        specialize (IH z' Z' ZD1 ZD2). rewrite (H3 z' z z' Z1' IH).
        split; try apply Z2'. intros YZ. subst. now apply Z'.
Qed.

Lemma simi_equiv X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> simi (res R p) (res R q) -> p === q.
Proof.
  intros WOR SP SQ PQ. split.
  - now apply (simi_sub WOR).
  - apply (simi_sub WOR); auto using simi_com.
Qed.

Lemma equiv_simi X (R: X -> X -> Prop) p q:
  worder R -> Segs R p -> Segs R q -> p === q -> simi (res R p) (res R q).
Proof.
  intros WOR SP SQ PQ. exists (fun x y => p x /\ x = y). repeat split.
  - intros x [y[H1 H2]]. subst y. exists x. repeat split; firstorder.
  - intros x x' y [X1 X2] XY. subst y. exists x'. repeat split; firstorder.
  - intros x y y' [_ XY] [_ XY']. congruence.
  - intros x [y[H1 H2]]. subst y. exists x. repeat split; firstorder.
  - intros x x' y [X1 X2] XY. subst y. exists x'. repeat split; firstorder.
  - intros x y y' [_ XY] [_ XY']. congruence.
  - intros x [y[H1 H2]]. exists x. now split.
  - intros x [y[H1 H2]]. exists x. apply PQ in H1. now split.
Qed.

Lemma simi_trans X (R: X -> X -> Prop) (S1: X -> X -> Prop) (S2: X -> X -> Prop):
  simi R S1 -> simi R S2 -> simi S1 S2.
Proof.
  intros [U[[[H1 H2][H3[[H4 H5] H6]]][H7 H8]]].
  intros [V[[[I1 I2][I3[[I4 I5] I6]]][I7 I8]]].
  pose (W := fun x z => exists y, U y x /\ V y z).
  exists W. repeat split.
  - firstorder.
  - intros x x' y [z[Z1 Z2]] XX. destruct (H5 x x' z Z1 XX) as [z'[Z3 Z4]].
    destruct (I2 z z' y Z2 Z4) as [y'[Y1 Y2]]. exists y'. firstorder.
  - intros x y y' [z[Z1 Z2]] [z'[Z3 Z4]]. apply (I3 z y y'); trivial.
    cutrewrite (z = z'); trivial. now apply (H6 x z z').
  - firstorder.
  - intros x x' y [z[Z1 Z2]] XX. destruct (I5 x x' z Z2 XX) as [z'[Z3 Z4]].
    destruct (H2 z z' y Z1 Z4) as [y'[Y1 Y2]]. exists y'. firstorder.
  - intros x y y' [z[Z1 Z2]] [z'[Z3 Z4]]. apply (H3 z y y'); trivial.
    cutrewrite (z = z'); trivial. now apply (I6 x z z').
  - intros x XD. destruct (H8 x XD) as [z Z]. assert (H: dom U z) by now exists x.
    destruct (I7 z (H1 z H)) as [y Y]. exists y. exists z. split; assumption.
  - intros x XD. destruct (I8 x XD) as [z Z]. assert (H: dom V z) by now exists x.
    destruct (H7 z (I1 z H)) as [y Y]. exists y. exists z. split; assumption.
Qed.