# Library Equivalence

## Equivalence

We reformulate some simple properties of the orderings.
They are already given in the respective developments and only need
some minor refactoring.

Lemma W1_irref a: ~ W1 a a.

Proof.

destruct X_wo as [[I _] _].

destruct (I a a) as [_ J]; unfold X'; trivial.

now apply J.

Qed.

Lemma W1_asym a b: W1 a b -> ~ W1 b a.

Proof.

destruct X_wo as [[I _] _].

destruct (I a b) as [J _]; unfold X'; trivial.

now apply J.

Qed.

Lemma W2_asym a b: W2 a b -> ~ W2 b a.

Proof.

intros I1 I2. apply (lt_irref (a:=a)). now apply (lt_tra (b:=b)).

Qed.

This lemma induces our strategy: to prove the orderings equivalent,
it suffices to prove one implication. The other is a consequence.

Lemma impl_equi: (forall a b, W2 a b -> W1 a b) -> (forall a b, W1 a b -> W2 a b).

Proof.

intros I a b J. destruct (lt_trich a b) as [H|[H|H]]; trivial.

- subst b. contradiction (W1_irref J).

- specialize (I b a H). contradiction (W1_asym J).

Qed.

We need one characterisation of W1 a b.
It is a sufficient criterion if we find a gamma-set G,
such that a is in G, but b is not.

Lemma char a b: (exists G W, GS G W /\ G a /\ ~ G b) -> W1 a b.

Proof.

intros [G[W[I1[I2 I3]]]]. exists G, W. split; trivial. split; trivial.

intros Mb Rb J1 J2. destruct (IS_compare' I1 J1) as [H|H]; trivial.

- intros H. apply iseg_sub in H. apply I3. now apply H.

- subst Mb. contradiction.

Qed.

We proof that W2 is a well-ordering for all subsets of X.
The term wellOrdered is specified in the 1904 implementation
and we need some technical refactoring to meet the actual requirements.

Lemma W2_WO U: wellOrdered U W2.

Proof.

split.

- split.

+ intros x y _ _. split; split; intros I.

* split; eauto using W2_asym. apply I.

* destruct I as [I1 I2]. destruct (lt_trich x y) as [H|[H|H]]; tauto.

* subst x. split; apply lt_irref.

* destruct I as [I1 I2]. destruct (lt_trich x y) as [H|[H|H]]; tauto.

+ intros x y z _ _ _. apply lt_tra.

- intros V I1 I2. destruct (lt_wo (p:=V)) as [x[X1 X2]].

+ assumption.

+ exists x. split; trivial. intros y Y1 Y2. apply (lt_irref (a:=y)).

apply (lt_tra Y2). apply X2. split; trivial. apply Y2.

Qed.

In the following, the sets of the form "R a" denote the specific element of T,
the intersection of all theta-chains, which is the construction used in 1908.
We first proof them linear, in the sense that a is in the rest of b,
whenever b is not in the rest of a.

Now we can prove, that the complements of the sets "R a" are gamma-sets.
By definition, we have to justify, the two properties of gamma-sets.
We use W2 and find that the complements are well-ordered.
It remains to show that the respective initial segments agrre with the
choice function Eps, which is a consequence of the lemma clos_Eps,
which states that Eps(R a) = a.

Lemma W2_GS a: GS (fun c => ~ R a c) W2.

Proof.

split; eauto using W2_WO.

intros b B. apply R_lin' in B.

assert (J: IS (fun c => ~ R a c) b W2 = IS X' b W2).

{ apply pe. intros d. split; intros [I1 I2]; split; unfold X'; trivial.

destruct I2 as [I2 I3]. intros HH. apply I3.

apply R_antisym; trivial. now apply R_tra with (b:=a). }

assert (I: X' -- IS (fun c => ~ R a c) b W2 = R b).

{ rewrite J. apply pe. intros d. split; intros I.

- destruct (xm (d=b)) as [Y|N].

+ subst d. apply R_ref.

+ destruct I as [I1 I2]. apply R_lin'. intros DB. apply I2. repeat split; trivial.

- split; unfold X'; auto. intros [I1 I2]. destruct I2 as [I2 I3].

apply I3. now apply R_antisym. }

rewrite I. symmetry. apply R_Eps.

Qed.

Now it is easy to conclude the implication we want to prove:
By the characterisation, it suffices to find the special gamma-set.
The statement above shows that the complement of R a is a gamma-set,
the two membership properties come from the definition of W2.

Lemma impl a b: W2 a b -> W1 a b.

Proof.

intros I. apply char. pose (RC := fun c => ~ R b c).

exists RC, W2. split; eauto using W2_GS. split.

- intros J. destruct I as [I1 I2]. apply I2. now apply R_antisym.

- intros J. apply J. apply R_ref.

Qed.

We conclude the equivalence of the two orderings.
Note that stronger propositional extensionality implies equality.