Library schutte.Ordering_Functions
Add LoadPath "../hilbert".
Add LoadPath "../prelude".
Add LoadPath "../denumerable".
Require Import Epsilon.
Require Import Schutte.
Require Import Ensembles.
Require Import Well_Orders.
Require Import Denumerable.
Require Import PartialFun.
Require Import Classical.
Set Implicit Arguments.
Lemma inh_Ordinal_sets : Ensemble OT.
Proof.
exact (fun (o:OT) => False); auto.
Qed.
Lemma inh_OT_OT : (OT -> OT).
exact (fun (alpha:OT) => alpha).
Qed.
Hint Resolve inh_OT_OT inh_Ordinal_sets : schutte.
Definition O_segment (A: Ensemble OT) :=
Included A ordinal /\
forall a b, A a -> b < a -> A b.
Definition proper_O_segment (A:OT->Prop) := O_segment A /\
~ (Same_set A ordinal).
Lemma ordinal_O_segment : O_segment ordinal.
Proof.
split;auto.
eauto with schutte.
Qed.
Lemma members_proper : forall a, ordinal a ->
proper_O_segment (members a).
Proof.
split.
split.
red; destruct 1;auto.
destruct 1.
split;auto.
unfold In.
eauto with schutte.
red.
eauto with schutte.
unfold Same_set.
red;destruct 1.
absurd (succ a < a).
intro;
case (le_not_gt (a:=a) (b:=succ a)); auto with schutte.
case (H1 (succ a)).
unfold In;auto with schutte.
auto.
Qed.
Lemma proper_members : forall A, proper_O_segment A -> exists a,
ordinal a /\
Same_set A (members a).
destruct 1.
unfold O_segment in H.
case (not_all_not_ex _ (fun b => ordinal b /\ ~ A b)).
red; intro.
unfold Same_set in H0.
apply H0;split.
unfold Included; case H;auto.
red; intros.
unfold In.
apply NNPP.
red; intro.
apply (H1 x).
split;auto.
intros.
case (well_order ON (fun x => ordinal x /\ ~ A x) x).
case H1;auto.
auto.
intros y Hy.
case Hy;intros H2 ((H3,H4),H5).
exists y;split.
auto.
red; unfold In; split. intros a H6.
tricho a y T.
case H;auto.
intros.
apply H7;auto.
split;auto.
unfold In.
case H;auto.
intros.
apply H7;auto.
subst y.
case H4;auto.
case H4.
case H;intros.
apply (H8 a);auto.
red; unfold In;intros.
apply NNPP.
case Hy.
intros _ ((H7,H8),H9).
red; intro H10.
case (H9 x0 ).
case H6.
auto.
split;auto.
case H6;auto.
intro;subst y.
inversion H6.
case (lt_irr x0);auto.
intro.
case (lt_irr x0).
apply lt_trans with y.
case H6;eauto with schutte.
auto.
Qed.
Lemma denumerable_segment_proper : forall A : Ensemble OT,
O_segment A -> denumerable A -> proper_O_segment A.
Proof.
intros.
red.
split;[auto|idtac].
red;intro H1.
generalize (Extensionality_Ensembles _ _ _ H1).
intros; subst A.
case Non_denum.
auto.
Qed.
Definition ordering_function (f : OT -> OT)(A B : Ensemble OT) :=
O_segment A /\
(Included B ordinal) /\
(forall a, In A a -> In B (f a)) /\
(forall b, B b -> exists a, In A a /\ f a = b)/\
forall a b , In A a -> In A b -> a < b -> f a < f b.
Definition ordering_function_segment (A B : Ensemble OT) :=
exists f : OT -> OT, ordering_function f A B.
Definition ordering_segment_2_fun (A B : Ensemble OT) :=
epsilon inh_OT_OT (fun f => ordering_function f A B).
Lemma ordering_segment_2_fun_ok :
forall A B, ordering_function_segment A B ->
ordering_function (ordering_segment_2_fun A B) A B.
Proof.
intros A B H.
pattern (ordering_segment_2_fun A B).
unfold ordering_segment_2_fun.
pattern (epsilon inh_OT_OT (fun f : OT -> OT => ordering_function f A B)).
apply epsilon_ind.
case H.
intros;exists x;auto.
auto.
Qed.
Lemma ordering_function_ordA : forall f A B, ordering_function f A B ->
Included A ordinal.
destruct 1.
case H;auto.
Qed.
Hint Resolve ordering_function_ordA : schutte.
Lemma ordering_function_ordB : forall f A B, ordering_function f A B ->
Included B ordinal.
destruct 1.
tauto.
Qed.
Hint Resolve ordering_function_ordB : schutte.
Lemma Inc_elim : forall (U:Type) (A B: Ensemble U), Included A B -> forall a, In A a ->In B a.
Proof.
eauto.
Qed.
Hint Resolve Inc_elim: schutte.
Lemma ordering_function_mono : forall f A B, ordering_function f A B ->
forall a b, In A a -> In A b -> a <b -> f a < f b.
Proof.
destruct 1.
tauto.
Qed.
Hint Resolve ordering_function_mono.
Lemma ordering_function_mono_weak :
forall f A B, ordering_function f A B ->
forall a b, In A a -> In A b -> a <= b -> f a <= f b.
Proof.
destruct 1.
decompose [and] H0; clear H0.
destruct 3.
case H6;intros; subst b.
left;
auto with schutte.
right;apply H5;auto.
Qed.
Hint Resolve ordering_function_mono_weak.
Lemma ordering_function_monoR : forall f A B, ordering_function f A B ->
forall a b, In A a -> In A b -> f a < f b -> a < b.
Proof.
intros.
case H;
intros.
decompose [and] H4.
clear H4.
tricho a b H4.
eapply (ordering_function_ordA H a H0 ).
eapply (ordering_function_ordA H b H1 ).
auto.
subst b.
case (lt_irr (f a)).
auto.
case (lt_irr (f a)).
apply lt_trans with (f b);auto.
Qed.
Hint Resolve ordering_function_monoR.
Lemma Ordering_bijection : forall f A B, ordering_function f A B ->
fun_bijection A B f.
Proof.
destruct 1.
decompose [and] H0; clear H0.
split;red;auto.
intros.
tricho a a' H7.
case H;intros H7 _; apply H7;auto.
case H;intros H7 _; apply H7;auto.
generalize (H5 _ _ H0 H4 ).
rewrite H6; intro H8. case (lt_irr _ (H8 H7));auto.
auto.
generalize (H5 _ _ H4 H0 H7).
rewrite H6; intro H8. case (lt_irr _ H8);auto.
Qed.
Lemma ordering_function_mono_weakR :
forall f A B, ordering_function f A B ->
forall a b, In A a -> In A b -> f a <= f b -> a <= b.
Proof.
intros.
case H.
intros. decompose [and] H4; clear H4.
case H2;intros.
case H4;intros.
case (Ordering_bijection H).
intros.
case (H13 a b H0 H1 H10).
left;split;auto with schutte.
fold ordinal;eauto with schutte.
right;auto.
eapply ordering_function_monoR; eauto.
Qed.
Hint Resolve ordering_function_mono_weakR.
Lemma ordering_function_seg : forall A B, ordering_function_segment A B ->
O_segment A.
Proof.
destruct 1 as [ f Hf].
case Hf;auto.
Qed.
Definition fun_eq (f g : OT -> OT )(A : OT -> Prop) :=
forall a, In A a -> f a = g a.
Definition fun_eq_gen (f g : OT -> OT)(A B : OT -> Prop) :=
Same_set A B /\ forall a, In A a -> f a = g a.
Lemma fun_eq_refl : forall (f : OT -> OT)(A : Ensemble OT),
fun_eq_gen f f A A.
Proof.
split; auto.
split;auto.
Qed.
Definition fun_restrict (f g : OT -> OT)(A B : OT -> Prop) :=
Included A B /\ forall a, In A a -> f a = g a.
Lemma empty_ordering : forall B, (forall b, ~ B b) ->
ordering_function (fun o => o)
(members zero)
B.
Proof.
intros.
split.
intros.
split.
red.
destruct 1.
red in H1.
case (not_lt_zero x);auto.
destruct 1.
case (not_lt_zero x);auto.
repeat split.
red;intro b.
intro;case (H b);auto.
destruct 1.
case (not_lt_zero x);auto.
intros b Hb;case (H b);auto.
intros a b Hb; case (not_lt_zero a).
case Hb;auto.
Qed.
Lemma O_segment_ordinal : forall A a, O_segment A -> A a -> ordinal a.
Proof.
intros.
case H.
intros.
apply H1;auto.
Qed.
Lemma O_segment_lt : forall A a b, O_segment A -> A a -> b < a -> A b.
Proof.
intros.
case H;intros.
apply H3 with a;auto.
Qed.
Hint Resolve O_segment_ordinal.
Theorem ordering_le : forall f A B, ordering_function f A B ->
forall a, A a -> a <= f a.
Proof.
intros.
generalize H0; pattern a; apply Induction.
2: case H; intuition.
2: case H1.
2:eauto with schutte.
unfold ordering_function in H; decompose [and] H.
clear H.
unfold progressive.
intros.
tricho a0 (f a0) H'; auto with schutte.
apply H3.
auto.
assert (f (f a0) < f a0).
apply H6.
eapply O_segment_lt;eauto with schutte.
unfold In;auto.
unfold In;auto.
auto.
case (le_not_gt (a:= f a0)(b:=f (f a0)));auto.
apply H5; eauto with schutte.
eapply O_segment_lt;eauto with schutte.
Qed.
Section ordering_function_unicity.
Variables B A1 A2 : Ensemble OT.
Variables f1 f2 : OT -> OT.
Hypothesis O1 : ordering_function f1 A1 B.
Hypothesis O2 : ordering_function f2 A2 B.
Remark ord_B : Included B ordinal.
Proof.
case O1; intuition.
Qed.
Remark SA1 : O_segment A1.
Proof.
case O1;intuition.
Qed.
Remark SA2 : O_segment A2.
Proof.
case O2;intuition.
Qed.
Hint Resolve SA2 SA1 ord_B.
Lemma A1_A2 :forall a, In A1 a -> A2 a /\ f1 a = f2 a.
Proof.
intros a Ha.
generalize Ha;pattern a; apply Induction.
2:apply O_segment_ordinal with A1;auto.
clear a Ha.
unfold progressive;intros.
assert (A2 a).
assert (forall khi, khi < a -> A2 khi /\ f1 khi = f2 khi).
intros.
apply H0.
eauto with schutte.
auto.
apply O_segment_lt with a;auto.
apply NNPP.
red; intro.
assert (forall y, A2 y -> y < a).
intros.
tricho y a H4.
eauto with schutte.
auto.
subst y; case H2;auto.
case H2.
apply O_segment_lt with y;auto.
assert (forall y, A2 y -> f1 y < f1 a).
intros.
case O1;intros.
decompose [and] H6.
apply H11;auto with schutte.
case (H1 y).
apply H3;auto.
intros.
apply O_segment_lt with a;auto.
case O2;intros.
decompose [and] H6.
clear H6.
case (H8 (f1 a)).
case O1;intros.
decompose [and] H10;clear H10.
apply H14.
auto.
intro.
destruct 1.
generalize (H4 x H6).
intro.
case (H0 x).
eauto with schutte.
eauto with schutte.
apply O_segment_lt with a;auto.
intros.
rewrite H14 in H12.
rewrite H10 in H12.
case (lt_irr (f1 a));auto.
split.
auto.
assert (is_least_member (ordinal) lt (fun x => B x /\
forall y, y < a ->
f1 y <> x)
(f1 a)).
split.
case O1;intros.
unfold In; intuition.
apply H4.
auto.
split.
split.
case O1;intros.
intuition.
apply H3;auto.
intros.
red;intro.
case (lt_irr (f1 a)).
pattern (f1 a) at 1; rewrite <- H3.
case O1;intros.
decompose [and] H5.
apply H10;auto with schutte.
apply O_segment_lt with a;auto with schutte.
destruct 2.
case O1;intros.
decompose [and] H6.
case (H8 x H3).
intros c (Hc,H'c).
subst x.
tricho (f1 c) (f1 a) H12.
apply H7.
auto.
tricho c a H13.
eauto with schutte.
case (H4 c H13).
auto.
subst a;auto.
right;apply H11;eauto with schutte.
auto.
auto.
assert (is_least_member (ordinal) lt (fun x => B x /\ forall y, y < a ->
f2 y <> x)
(f2 a)).
split.
case O2;intros.
case H4;auto.
unfold In, Included;intuition.
apply H7.
auto.
split.
split.
case O2;intros.
intuition.
apply H4;auto.
intros.
red;intro.
case (lt_irr (f2 a)).
pattern (f2 a) at 1; rewrite <- H4.
case O2;intros.
decompose [and] H6.
apply H11;auto with schutte.
apply O_segment_lt with a;auto with schutte.
destruct 2.
case O2;intros.
decompose [and] H7.
case (H9 x H4).
intros c (Hc,H'c).
subst x.
tricho (f2 c) (f2 a) H13.
apply H8.
auto.
tricho c a H14.
eauto with schutte.
case (H5 c H14).
auto.
subst a;auto.
right;apply H12;eauto with schutte.
auto.
auto.
eapply (least_member_unicity ON);eauto.
generalize (least_member_of_eq ON
(X:=fun x : M ON => B x /\
(forall y : M ON, y < a -> f2 y <> x))
(Y:=fun x : M ON => B x /\ (forall y : M ON, y < a -> f1 y <> x)) ).
intros.
generalize (H4 (f2 a) (f1 a)).
clear H4;intros.
rewrite H4.
auto.
intros x (H5,H6).
split;auto.
intros.
replace (f1 y) with (f2 y).
auto.
case (H0 y).
eauto with schutte.
auto.
eapply O_segment_lt with a;auto.
auto.
intros x (H5,H6).
split;auto.
intros.
replace (f2 y) with (f1 y).
auto.
case (H0 y).
eauto with schutte.
auto.
eapply O_segment_lt with a;auto.
auto.
auto.
auto.
Qed.
Lemma A2_A1 :forall a, A2 a -> A1 a /\ f2 a = f1 a.
Proof.
intros a Ha.
generalize Ha;pattern a; apply Induction.
2:apply O_segment_ordinal with A2;auto.
clear a Ha.
unfold progressive;intros.
assert (A1 a).
assert (forall khi, khi < a -> A1 khi /\ f2 khi = f1 khi).
intros.
apply H0.
eauto with schutte.
auto.
apply O_segment_lt with a;auto.
apply NNPP.
red; intro.
assert (forall y, A1 y -> y < a).
intros.
tricho y a H4.
eauto with schutte.
auto.
subst y; case H2;auto.
case H2.
apply O_segment_lt with y;auto.
assert (forall y, A1 y -> f2 y < f2 a).
intros.
case O2;intros.
decompose [and] H6.
apply H11;auto with schutte.
case (H1 y).
apply H3;auto.
intros.
apply O_segment_lt with a;auto.
case O1;intros.
decompose [and] H6.
clear H6.
case (H8 (f2 a)).
case O2;intros.
decompose [and] H10;clear H10.
apply H14.
auto.
intro.
destruct 1.
generalize (H4 x H6).
intro.
case (H0 x).
eauto with schutte.
eauto with schutte.
apply O_segment_lt with a;auto.
intros.
rewrite H14 in H12.
rewrite H10 in H12.
case (lt_irr (f2 a));auto.
split.
auto.
assert (is_least_member (ordinal) lt
(fun x => B x /\ forall y, y < a ->
f2 y <> x)
(f2 a)).
split.
case O2;intros.
unfold In; intuition.
apply H4.
auto.
split.
split.
case O2;intros.
intuition.
apply H3;auto.
intros.
red;intro.
case (lt_irr (f2 a)).
pattern (f2 a) at 1; rewrite <- H3.
case O2;intros.
decompose [and] H5.
apply H10;auto with schutte.
apply O_segment_lt with a;auto with schutte.
destruct 2.
case O2;intros.
decompose [and] H6.
case (H8 x H3).
intros c (Hc,H'c).
subst x.
tricho (f2 c) (f2 a) H12.
apply H7.
auto.
tricho c a H13.
eauto with schutte.
case (H4 c H13).
auto.
subst a;auto.
right;apply H11;eauto with schutte.
auto.
auto.
assert (is_least_member (ordinal) lt
(fun x => B x /\ forall y, y < a ->
f1 y <> x)
(f1 a)).
split.
case O1;intros.
case H4;auto.
unfold In, Included;intuition.
apply H7.
auto.
split.
split.
case O1;intros.
intuition.
apply H4;auto.
intros.
red;intro.
case (lt_irr (f1 a)).
pattern (f1 a) at 1; rewrite <- H4.
case O1;intros.
decompose [and] H6.
apply H11;auto with schutte.
apply O_segment_lt with a;auto with schutte.
destruct 2.
case O1;intros.
decompose [and] H7.
case (H9 x H4).
intros c (Hc,H'c).
subst x.
tricho (f1 c) (f1 a) H13.
apply H8.
auto.
tricho c a H14.
eauto with schutte.
case (H5 c H14).
auto.
subst a;auto.
right;apply H12;eauto with schutte.
auto.
auto.
eapply (least_member_unicity ON);eauto.
generalize (least_member_of_eq ON
(X:=fun x : M ON => B x /\
(forall y : M ON, y < a -> f1 y <> x))
(Y:=fun x : M ON => B x /\ (forall y : M ON, y < a -> f2 y <> x)) ).
intros.
generalize (H4 (f1 a) (f2 a)).
clear H4;intros.
rewrite H4.
auto.
intros x (H5,H6).
split;auto.
intros.
replace (f2 y) with (f1 y).
auto.
case (H0 y).
eauto with schutte.
auto.
eapply O_segment_lt with a;auto.
auto.
intros x (H5,H6).
split;auto.
intros.
replace (f1 y) with (f2 y).
auto.
case (H0 y).
eauto with schutte.
auto.
eapply O_segment_lt with a;auto.
auto.
auto.
auto.
Qed.
Theorem ordering_function_unicity : fun_eq_gen f1 f2 A1 A2.
Proof.
intros.
split.
split.
intro.
intro.
case (A1_A2 H);auto.
intros x0 H0;case (A2_A1 H0);auto.
intros.
case (A1_A2 H);auto.
Qed.
End ordering_function_unicity.
Lemma ordering_function_seg_unicity : forall A1 A2 B,
ordering_function_segment A1 B ->
ordering_function_segment A2 B -> A1 = A2.
Proof.
destruct 1 as [f1 Hf1].
destruct 1 as [f2 Hf2].
apply Extensionality_Ensembles.
assert (fun_eq_gen f1 f2 A1 A2).
eapply ordering_function_unicity;eauto.
case H;auto.
Qed.
Definition proper_segment_of (B : Ensemble OT)(beta : OT): Ensemble OT :=
fun alpha => B alpha /\ alpha < beta /\ B beta.
Lemma proper_segment_ordinals : forall (B : OT -> Prop),
(Included B ordinal) ->
forall beta, In B beta -> Included (proper_segment_of B beta) ordinal.
Proof.
intros B H beta Hbeta alpha Halpha.
case Halpha.
intros; apply H.
auto.
Qed.
Section ordering_function_ex_recur.
Variable B : Ensemble OT.
Hypothesis OrdB : Included B ordinal.
Variable recur : forall beta, In B beta ->
exists A : Ensemble OT,
ordering_function_segment A
(proper_segment_of B beta).
Section beta_fixed.
Variable beta : OT.
Hypothesis beta_B : In B beta.
Remark O_beta : ordinal beta.
Proof.
apply OrdB;auto.
Qed.
let us build an ordering function for (proper_segment_of B beta)
Definition _A := iota inh_Ordinal_sets (fun E => ordering_function_segment E
(proper_segment_of B beta)).
Definition f_beta := epsilon inh_OT_OT
(fun f =>
ordering_function f _A
(proper_segment_of B beta)).
Lemma of_beta' : ordering_function f_beta _A (proper_segment_of B beta).
pattern f_beta.
hilbert_e.
pattern _A.
hilbert_e.
case (recur beta_B).
intros.
exists x;split;auto.
intros;eapply ordering_function_seg_unicity;eauto.
Qed.
Remark Bbeta_denum : denumerable (proper_segment_of B beta).
Proof.
apply AX2.
apply proper_segment_ordinals;auto.
exists beta.
split;auto.
apply OrdB;auto.
destruct 1;auto.
destruct H0;auto.
Qed.
Hint Resolve of_beta': schutte.
Remark A_denum : denumerable _A.
Proof.
eapply denumerable_bij_funR.
eapply Ordering_bijection.
eauto with schutte.
apply Bbeta_denum;eauto.
Qed.
Lemma Proper_A : proper_O_segment _A.
apply denumerable_segment_proper.
eapply SA1.
eauto with schutte.
eapply A_denum.
Qed.
Lemma g_def1 : exists g_beta, ordinal g_beta /\ _A = members g_beta.
generalize (proper_members Proper_A).
intros (a,Ha);exists a;split.
case Ha;auto.
eapply Extensionality_Ensembles.
auto.
case Ha;auto.
Qed.
Lemma g_unic : forall g_beta g_beta', ordinal g_beta ->
ordinal g_beta' ->
_A = members g_beta ->
_A = members g_beta' ->
g_beta = g_beta'.
Proof.
intros.
rewrite H2 in H1;clear H2.
assert (Same_set (members g_beta') (members g_beta)).
rewrite H1;auto.
split;auto.
case H2.
unfold Included, members; intros.
apply le_antisym.
apply not_gt_le; auto with schutte.
red.
intro.
generalize (H4 g_beta').
intros.
unfold In in H6.
case (lt_irr g_beta').
assert (Intersection OT ordinal (fun b : OT => b < g_beta) g_beta').
split;auto.
generalize (H6 H7).
intro.
inversion H8.
auto.
apply not_gt_le; auto with schutte.
red.
intro.
generalize (H3 g_beta).
intros.
unfold In in H6.
case (lt_irr g_beta).
assert (Intersection OT ordinal (fun b : OT => b < g_beta') g_beta).
split;auto.
generalize (H6 H7).
intro.
inversion H8.
auto.
Qed.
Definition g := iota inh_OT (fun o => ordinal o /\ _A = members o).
End beta_fixed.
Lemma g_def : forall beta, In B beta -> _A beta = members (g beta ).
Proof.
intros.
pattern (g beta).
hilbert_e.
case (g_def1 H).
intros x (Hx,H'x).
exists x.
split;auto.
intros a' (Ha',Ha'').
eapply g_unic;eauto.
tauto.
Qed.
Lemma g_ord : forall beta, In B beta -> ordinal (g beta).
Proof.
intros.
pattern (g beta).
hilbert_e.
case (g_def1 H).
intros x (Hx,H'x).
exists x;split;auto.
intros a' (Ha',Ha'').
eapply g_unic;eauto.
tauto.
Qed.
Lemma g_domains : fun_codomain B ordinal g.
Proof.
red.
exact g_ord.
Qed.
Lemma g_lemma :
forall beta, In B beta ->
ordering_function (f_beta beta) (members (g beta))
(proper_segment_of B beta).
Proof.
intros.
rewrite <- g_def.
apply of_beta'.
auto.
auto.
Qed.
Lemma g_mono : forall beta1 beta2, In B beta1 -> In B beta2 ->
beta1 < beta2 ->
g beta1 < g beta2.
intros.
assert( B2 : fun_bijection (members (g beta2)) (proper_segment_of B beta2) (f_beta beta2)) .
apply Ordering_bijection.
apply g_lemma; auto.
assert (B3 : In (proper_segment_of B beta2) beta1).
red;red.
split; auto.
assert (B4 : exists alpha, ordinal alpha /\ alpha < g beta2 /\ f_beta beta2 alpha= beta1).
case B2.
intros.
case (H3 beta1).
auto.
intros alpha (H5,H6).
exists alpha.
split;auto.
case H5;auto.
split;auto.
case H5;auto.
case B4; intros alpha (Ha1,(Ha2,Ha3)).
assert (B5 : ordering_function (f_beta beta2) (members alpha)
(proper_segment_of B beta1)).
repeat split;auto with schutte.
red;destruct 1;auto.
cbv beta delta[In].
eauto with schutte.
red;apply lt_trans with a;eauto.
case H2;auto.
red.
destruct 1;auto.
case B2;intros.
clear H4 H5.
red in H3.
generalize (H3 a).
intros.
clear H3.
case H4.
2:auto.
split.
case H2;auto.
red.
apply lt_trans with alpha.
case H2;auto.
auto.
case (g_lemma H0).
intros.
decompose [and] H4.
clear H4.
replace beta1 with (f_beta beta2 alpha).
apply H9;auto.
split.
case H2;auto.
red.
apply lt_trans with alpha;auto.
case H2;auto.
split;auto.
case H2;auto.
destruct 1.
case (g_lemma H0).
intros.
decompose [and] H4.
clear H4.
decompose [and] H5.
clear H9.
clear H7.
clear H5.
case (H6 b).
split;auto.
split;auto.
eapply lt_trans;eauto.
case H3;auto.
intros a (Ha,Ha');exists a;split;auto.
split.
case Ha;auto.
red.
tricho a alpha X.
case Ha;auto.
auto.
subst a.
rewrite Ha3 in Ha'.
subst b.
case H3;intros H33 _.
case (lt_irr _ H33).
clear H6.
assert (beta1 < b).
rewrite <- Ha3; rewrite <- Ha'.
case (g_lemma H0).
destruct 1.
intros.
decompose [and] H7.
apply H12;auto.
split;auto.
case (lt_irr beta1).
apply lt_trans with b;auto.
case H3;auto.
intros.
case (g_lemma H0).
destruct 1.
intros.
decompose [and] H7.
apply H12;auto.
clear H10 H9 H12 H7.
split;auto.
case H2;auto.
red.
apply lt_trans with alpha;auto.
case H2;auto.
split;auto.
case H3;auto.
red.
apply lt_trans with alpha;auto.
case H3;auto.
generalize (g_lemma H);intro.
generalize (ordering_function_unicity B5 H2).
destruct 1.
generalize (Extensionality_Ensembles _ _ _ H3).
intros.
generalize (members_eq Ha1 (g_ord H) H5).
intro; subst alpha;auto.
Qed.
Lemma L3a : O_segment (image B g).
Proof.
split.
red.
intro a;destruct 1.
case H.
intros; subst a.
red;apply g_ord;auto.
intros gbeta alpha (beta,(H1,H2)) H3.
assert (Halpha : ordinal alpha) . ordi.
subst gbeta.
red.
generalize (g_lemma H1);intro.
case H; intros.
decompose [and] H2;clear H2.
assert (exists beta0, In (proper_segment_of B beta) beta0
/\ f_beta beta alpha=beta0).
exists (f_beta beta alpha).
split;auto.
apply H6.
split;auto.
case H2;intros beta0 (H9,H10).
clear H2.
assert (B5 : ordering_function (f_beta beta) (members alpha)
(proper_segment_of B beta0)).
repeat split;auto with schutte.
red; destruct 1;auto.
cbv beta delta[In].
eauto with schutte.
red;
apply lt_trans with a;eauto.
case H2;auto.
red.
destruct 1;auto.
assert( B2 : fun_bijection (members (g beta)) (proper_segment_of B beta) (f_beta beta)) .
apply Ordering_bijection.
apply g_lemma; auto.
case B2;intros.
red in H7.
generalize (H7 a).
intros.
clear H7.
case H13.
2:auto.
split.
case H2;auto.
red.
apply lt_trans with alpha.
case H2;auto.
auto.
case (g_lemma H1).
intros.
decompose [and] H11.
clear H11.
replace beta0 with (f_beta beta alpha).
apply H16;auto.
split.
case H2;auto.
red.
apply lt_trans with alpha;auto.
case H2;auto.
split;auto.
case H2;auto.
case H9.
auto.
destruct 1.
case (g_lemma H1).
intros.
decompose [and] H11.
clear H11.
decompose [and] H12.
case (H13 b).
split;auto.
split;auto.
apply lt_trans with beta0;auto.
case H7;auto.
case H9;auto.
destruct 2; auto.
intros a (Ha,Ha');exists a;split;auto.
split.
case Ha;auto.
red.
tricho a alpha X.
case Ha;auto.
auto.
subst a.
rewrite H10 in Ha'.
subst b;case H7; intros H77 _.
case (lt_irr _ H77).
assert (beta0 < b).
rewrite <- H10; rewrite <- Ha'.
case (g_lemma H1).
destruct 1.
intros.
decompose [and] H18.
apply H23;auto.
split;auto.
case (lt_irr beta0).
apply lt_trans with b;auto.
case H7;auto.
intros.
case (g_lemma H1).
destruct 1.
intros.
decompose [and] H14.
apply H19;auto.
split;auto.
case H2;auto.
red.
apply lt_trans with alpha;auto.
case H2;auto.
split;auto.
case H7;auto.
red.
apply lt_trans with alpha;auto.
case H7;auto.
generalize (g_lemma (beta:=beta0));intros.
case H9;intros.
generalize (H2 H7).
intros.
generalize (ordering_function_unicity B5 H12).
destruct 1.
generalize (Extensionality_Ensembles _ _ _ H13).
intros.
generalize (members_eq (a:=alpha)(b:=g beta0) Halpha (g_ord H7) H15 ).
intro.
exists beta0.
split;auto.
Qed.
Lemma g_bij : fun_bijection B (image B g) g.
split.
red.
intros.
red;red.
exists a;split;auto.
red.
destruct 1.
exists x;split;auto.
case H;auto.
case H;auto.
red;intros.
tricho a a' XXX.
apply OrdB;auto.
apply OrdB;auto.
generalize (g_mono H H0 XXX).
intro.
rewrite H1 in H2.
case (lt_irr _ H2).
auto.
generalize (g_mono H0 H XXX).
intro.
rewrite H1 in H2.
case (lt_irr _ H2).
Qed.
Hint Resolve g_bij : schutte.
Let g_1 := inv_fun inh_OT B (image B g) g.
Lemma g_1_bij : fun_bijection (image B g) B g_1.
Proof.
unfold g_1.
apply inv_fun_bij; auto with schutte.
Qed.
Hint Resolve g_1_bij : schutte.
Lemma g_1_of : ordering_function g_1 (image B g) B.
split.
apply L3a.
repeat split.
auto.
destruct 1.
case H.
intros.
rewrite <- H1.
replace (g_1 (g x)) with x.
auto.
symmetry;unfold g_1;eapply inv_compose;eauto.
auto with schutte.
auto with schutte.
intros.
exists (g b).
split;auto.
exists b.
split;auto.
unfold g_1;eapply inv_compose;eauto.
auto with schutte.
auto with schutte.
intros.
tricho (g_1 a) (g_1 b) XXX; auto with schutte.
case g_1_bij; intros.
generalize (H2 a H).
intros;apply OrdB;auto.
case g_1_bij; intros.
generalize (H2 b H0).
intros;apply OrdB;auto.
replace a with (g (g_1 a)) in H1.
replace b with (g (g_1 b)) in H1.
rewrite XXX in H1.
case (lt_irr _ H1).
unfold g_1;
apply inv_composeR;
auto with schutte.
unfold g_1;
apply inv_composeR;
auto with schutte.
case (le_not_gt (a:=a)(b:= b)).
auto with schutte.
replace a with (g (g_1 a));
replace b with (g (g_1 b)) .
apply g_mono;auto with schutte.
case g_1_bij;auto with schutte.
case g_1_bij;auto with schutte.
unfold g_1;
apply inv_composeR;
auto with schutte.
unfold g_1;
apply inv_composeR;
auto with schutte.
unfold g_1;
apply inv_composeR;
auto with schutte.
Qed.
Lemma L3 : exists AB, ordering_function_segment AB B.
exists (image B g).
exists g_1.
apply g_1_of.
Qed.
Lemma L3' : exists AB, exists f, ordering_function f AB B.
exists (image B g).
exists g_1.
apply g_1_of.
Qed.
End ordering_function_ex_recur.
Section ofB.
Variable B : Ensemble OT.
Hypothesis OB : Included B ordinal.
Theorem B_of : exists AB, ordering_function_segment AB B.
apply L3.
auto.
intros beta Hbeta; pattern beta; apply Induction.
red.
intros.
apply L3.
red; destruct 1;auto.
intros.
case H1;intros H2 (H3,H4).
replace (proper_segment_of (proper_segment_of B a) beta0)
with (proper_segment_of B beta0).
apply H0.
apply OB;eauto.
auto.
apply Extensionality_Ensembles; split.
red; destruct 1; auto.
red.
red.
case H6;intros;repeat split;auto.
eapply lt_trans;eauto.
red; destruct 1;auto.
red.
case H6;intros;repeat split;auto.
case H5;auto.
apply OB;auto.
Qed.
Theorem B_of' : exists AB, exists f, ordering_function f AB B.
Proof.
case B_of;intros AB (f,pi).
eauto.
Qed.
Definition the_ordering_segment := epsilon inh_Ordinal_sets
(fun x => ordering_function_segment x B).
Definition the_ordering_function :=
epsilon inh_OT_OT
(fun f => ordering_function f the_ordering_segment B).
Lemma the_ordering_function_ok :
ordering_function the_ordering_function the_ordering_segment B.
Proof.
pattern the_ordering_function.
hilbert_e.
pattern the_ordering_segment.
hilbert_e.
case B_of.
intros.
exists x.
auto.
Qed.
Lemma the_ordering_function_eq : forall A f,
ordering_function f A B -> fun_eq_gen f the_ordering_function
A the_ordering_segment.
Proof.
intros;eapply ordering_function_unicity.
eauto.
apply the_ordering_function_ok.
Qed.
End ofB.
Lemma ordering_function_ordinal_B : forall A B f,
ordering_function f A B -> forall a, In A a -> ordinal (f a).
Proof.
intros.
case H.
destruct 2.
decompose [and] H3.
generalize (H2 _ (H4 a H0)).
auto.
Qed.
Lemma of_image : forall f A B, ordering_function f A B ->
ordering_function f A (image A f).
Proof.
intros f A B O; case O; intros.
decompose [and] H0.
repeat split;auto.
case H;auto.
case H;auto.
red.
destruct 1.
apply H1.
decompose [and] H4.
subst x;apply H3.
auto.
intros; exists a;auto.
Qed.
Section Th13_5.
Variables (A B : Ensemble OT).
Variable f : OT -> OT.
Hypothesis f_ord : ordering_function f A B.
Section recto.
Hypothesis f_cont : continuous f A B.
Section M_fixed.
Variable M : Ensemble OT.
Hypothesis inc : Included M B.
Hypothesis ne : Inhabited _ M.
Hypothesis den : denumerable M.
Let U := fun u => In A u /\ In M ( f u).
Remark fbij : fun_bijection A B f.
apply Ordering_bijection.
auto.
Qed.
Remark restrict : fun_bijection U M f.
Proof.
split.
red.
destruct 1;auto.
red.
case fbij.
intros.
case (H0 b).
apply inc;auto.
intros x (Hx,H'x).
exists x;split;auto.
red;unfold U.
split;auto.
subst b;auto.
red.
destruct 1.
destruct 1.
intros.
case fbij;intros.
apply H6;auto.
Qed.
Remark Inc_U_A : Included U A.
red.
destruct 1.
auto.
Qed.
Remark den_U : denumerable U.
eapply denumerable_bij_funR with OT M f;auto.
apply restrict.
Qed.
Remark inh_U : Inhabited _ U.
case ne;intros.
exists (inv_fun inh_OT A B f x).
red; unfold U.
rewrite inv_composeR.
split;auto.
generalize (Ordering_bijection f_ord).
intros.
generalize (inv_fun_bij inh_OT H0).
intros.
case (H1 H0).
intros.
apply H2.
apply inc;auto.
apply Ordering_bijection; auto.
apply inc;auto.
Qed.
Remark im_U_f : (image U f : Ensemble OT) = M.
eapply Extensionality_Ensembles.
split.
red;destruct 1.
unfold U in H.
case H.
intros.
red in H0.
case H0;intros.
subst x;auto.
red.
intros.
red.
red.
exists (inv_fun inh_OT A B f x).
split.
red;red.
generalize (Ordering_bijection f_ord).
intros.
split.
case (inv_fun_bij inh_OT H0).
auto.
intros.
apply H1.
apply inc;auto.
rewrite inv_composeR; auto with schutte.
apply inc;auto.
rewrite inv_composeR; auto with schutte.
apply Ordering_bijection;auto with schutte.
apply inc;auto with schutte.
Qed.
Lemma sup_M_in_B : In B (sup M).
Proof.
rewrite <- im_U_f.
case f_cont.
intros.
rewrite H1; auto.
apply H.
case H0; intros.
apply H3;auto.
apply Inc_U_A.
apply inh_U.
apply den_U.
apply Inc_U_A.
apply inh_U.
apply den_U.
Qed.
End M_fixed.
Lemma Th_13_5_1 : closed B.
split.
eauto with schutte.
apply sup_M_in_B.
Qed.
End recto.
Section verso.
Hypothesis B_closed : closed B.
Section U_fixed.
Variable U : Ensemble OT.
Hypothesis U_non_empty : Inhabited _ U.
Hypothesis U_den : denumerable U.
Hypothesis U_inc_A : Included U A.
Remark R1_aux : denumerable (image U f).
Proof.
apply denumerable_bij_fun with OT U f.
case (Ordering_bijection f_ord).
intros.
split.
intros u u_In_U.
repeat red. exists u; auto.
intros u u_In_img.
case u_In_img.
intros x Hx.
exists x; assumption.
intros u1 u2 u1_In_U u2_In_U Heq.
apply H1; try apply U_inc_A; assumption.
assumption.
Qed.
Definition R1 := let foo := U_den in R1_aux.
Opaque R1.
Remark R2 : In B (sup (image U f)).
Proof.
case B_closed.
intros.
apply H0;auto.
red;red.
destruct 1.
case f_ord.
intros _ (_,(H2,_)).
case H1;intros.
subst x;apply H2.
apply U_inc_A;auto.
case U_non_empty;intros.
exists (f x);auto.
red;red.
exists x;auto.
apply R1_aux.
Qed.
Remark R3: exists alpha, In A alpha /\ f alpha = sup(image U f).
Proof.
case f_ord.
intros.
decompose [and] H0.
case (H2 (|_|image U f)).
apply R2.
intros x; exists x;auto.
Qed.
Let alpha_ : OT.
some_i (fun alpha => In A alpha /\ f alpha = sup(image U f)).
auto with schutte.
apply R3.
Defined.
Lemma alpha_A : In A alpha_.
Proof.
pattern alpha_ . some_elim.
tauto.
Qed.
Lemma alpha_sup : f alpha_ = sup(image U f).
Proof.
pattern alpha_; some_elim.
tauto.
Qed.
Remark R5 : forall khi, In U khi -> f khi <= f alpha_.
Proof.
intros.
rewrite alpha_sup.
pattern (image U f),(|_|image U f).
pfun_e.
split.
apply R1.
red.
destruct 1.
decompose [and] H0.
subst x.
clear H0.
case f_ord;intros.
decompose [and] H2.
apply H3; auto.
destruct 1.
destruct 1.
decompose [and] H3.
case (H4 (f khi)).
case f_ord.
intros.
decompose [and] H7.
generalize (H8 (f khi)).
intros.
apply H11.
auto.
red.
exists khi.
split;auto.
left.
split;auto.
rewrite H6.
auto.
right;auto.
Qed.
Remark R6 : forall khi, In U khi -> khi <= alpha_ .
Proof.
intros.
case (R5 H).
left.
split.
generalize (U_inc_A H).
case f_ord .
destruct 1.
intros.
fold ordinal. red; apply H1; auto.
case (Ordering_bijection f_ord).
intros.
apply H3.
apply U_inc_A;auto.
apply alpha_A.
case H0;auto.
fold lt.
right.
fold lt .
case f_ord.
intros _ H1; decompose [and] H1.
tricho khi alpha_ H7.
generalize (U_inc_A H).
intro.
case f_ord.
intros H11 _; case H11.
intros.
apply H7;auto.
case f_ord.
intros H11 _; case H11.
intros.
apply H5.
apply alpha_A.
auto.
subst khi.
case (lt_irr _ H0).
case (lt_irr (f alpha_)).
apply lt_trans with (f khi).
apply H6;auto.
apply alpha_A.
auto.
Qed.
Remark R000 : forall a, In A a -> ordinal a.
Proof.
case f_ord;intros.
case H;intros.
apply H2;auto.
Qed.
Hint Resolve R000.
Remark R001 : forall u, In U u -> ordinal u.
Proof.
intros.
assert (In A u).
apply U_inc_A;auto.
auto.
Qed.
Hint Resolve R001 alpha_A.
Remark R7 : sup U <= alpha_ .
pattern U,(sup U); pfun_e.
destruct 1.
destruct 1.
decompose [and] H2.
case (H4 alpha_).
auto.
red.
intros.
case (R6 H6).
tauto.
tauto.
left;auto.
right;auto.
Qed.
Remark R4 : forall khi, In U khi -> khi <= sup U.
Proof.
intros.
pattern U,(sup U).
pfun_e.
destruct 1.
destruct 1.
case H3;intros H4 H5.
case ( H4 khi);auto with schutte.
Qed.
Lemma A_closed : In A (sup U).
Proof.
assert (O_segment A).
eapply SA2.
eauto.
case H.
intros.
case R7.
destruct 1;intros.
rewrite H3.
apply alpha_A.
intros;red.
eapply H1 with alpha_ ;auto.
apply alpha_A.
Qed.
Remark R4' : forall khi, In U khi -> f khi <= f (sup U).
Proof.
intros.
case f_ord;intros.
decompose [and] H1.
clear H1.
case (R4 H).
destruct 1.
subst khi;left;auto with schutte.
right;auto.
apply H6;auto with schutte.
apply A_closed;auto.
Qed.
Remark R4'' : sup (image U f) <= f (sup U).
Proof.
pattern (image U f),(sup (image U f)).
pfun_e.
split;auto with schutte.
apply R1.
red;eauto with schutte.
destruct 1.
case H.
intros.
subst x.
clear H.
case f_ord;intros.
decompose [and] H1.
apply H2.
apply H4;auto.
destruct 1.
intros (H'1,H1).
decompose [and] H1.
case (H3 (f (sup U))).
case f_ord;intros.
decompose [and] H5.
generalize (H6 (f (sup U))).
intros.
apply H9.
apply H8.
apply A_closed;auto.
red.
intros.
case H5;intros.
decompose [and] H6.
subst x.
clear H6.
case (R4' H7).
tauto.
fold lt;auto.
auto with schutte.
auto with schutte.
Qed.
Remark R42 : f(sup U) <= sup (image U f).
Proof.
apply le_trans with (f alpha_).
case f_ord;intros.
decompose [and] H0;clear H0.
case R7.
destruct 1.
rewrite H4;auto with schutte.
left.
split;auto.
right;auto.
apply H5;auto.
apply A_closed;auto.
pattern alpha_.
some_elim.
destruct 1.
left;auto.
split;auto.
case f_ord.
intros.
decompose [and] H2.
fold ordinal.
apply H3.
auto.
Qed.
Lemma f_sup_commutes : f (sup U)=sup (image U f).
Proof.
apply le_antisym.
apply R42.
apply R4''.
Qed.
End U_fixed.
Lemma Th_13_5_2 : continuous f A B.
Proof.
split.
red.
case f_ord;tauto.
split.
case f_ord;intros.
case H;auto.
intros;apply A_closed;auto.
intros;symmetry;apply f_sup_commutes;auto.
Qed.
End verso.
End Th13_5.
Inductive normal (f : OT -> OT)(B : Ensemble OT): Prop :=
normal_intro : ordering_function f ordinal B ->
continuous f ordinal B ->
normal f B.
Theorem TH_13_6 : forall B f, Included B ordinal ->
normal f B ->
closed B /\ Unbounded B.
Proof.
destruct 2.
split.
eapply Th_13_5_1;eauto.
red.
intros.
generalize (Ordering_bijection H0).
destruct 1.
exists (f (succ x)).
split.
apply H3.
red.
auto with schutte.
apply le_lt_trans with (f x).
eapply ordering_le;eauto.
eapply ordering_function_mono;eauto.
red.
auto with schutte.
auto with schutte.
Qed.
Theorem O_segment_unbounded : forall (A:Ensemble OT), O_segment A ->
Unbounded A ->
A = ordinal.
Proof.
intros.
red in H0.
apply Extensionality_Ensembles.
split.
case H.
red;auto.
red.
intro.
intro;case (H0 x).
auto.
destruct 1.
case H;intros.
red;eapply H5;eauto.
auto.
Qed.
Lemma ordering_unbounded_unbounded :
forall A B f, Included B ordinal -> ordering_function f A B ->
(Unbounded B <-> Unbounded A).
Proof.
split;intros.
apply not_denumerable_unbounded.
case H0.
intros H2 _;auto with schutte.
red.
case H2.
auto.
red;intro.
assert (denumerable B).
apply denumerable_bij_fun with OT A f;auto.
auto with schutte.
apply Ordering_bijection;auto.
case (denumerable_not_Unbounded H H3);auto.
apply not_denumerable_unbounded.
auto.
red;intro.
assert (denumerable A).
apply denumerable_bij_funR with OT B f;auto.
apply Ordering_bijection;auto.
case (denumerable_not_Unbounded (X:= A));auto.
case H0.
destruct 1;auto.
Qed.
Theorem TH_13_6R : forall A B f, Included B ordinal ->
ordering_function f A B ->
closed B ->
Unbounded B ->
normal f B.
Proof.
intros.
assert (A = ordinal).
apply O_segment_unbounded.
eapply SA1;eauto.
case (ordering_unbounded_unbounded H H0).
tauto.
split.
subst A ;auto.
apply Th_13_5_2.
subst A;auto.
auto.
Qed.
Lemma order_function_least_least :
forall B f , ordering_function f ordinal B ->
is_least_member ordinal lt B (f zero).
Proof.
intros.
case H ;intros.
decompose [and] H1; clear H1.
case H.
intros H8 (H9,H10).
split.
apply H2.
apply H4;auto.
red;auto with schutte.
split.
apply H4;auto.
red;auto with schutte.
intros.
decompose [and] H10.
case (H12 _ H5).
intros x0 (Hx0,H'x0).
subst x.
generalize (ordering_function_mono_weak H (a:=zero) (b:=x0)).
intros.
case H11;auto with schutte.
destruct 1;auto.
Qed.
Lemma O_segment_lt_closed : forall A a b, O_segment A ->
In A b ->
a < b ->
In A a.
Proof.
intros.
case H.
intros.
red;auto.
eapply H3.
2:eauto.
auto.
Qed.