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.