Library schutte.Schutte
Set Implicit Arguments.
Add LoadPath "../hilbert".
Add LoadPath "../prelude".
Add LoadPath "../denumerable".
Require Import Relations.
Require Import Epsilon.
Require Import Classical.
Require Import Well_Orders.
Require Import Lub.
Require Import Denumerable.
Require Import Compare_dec.
Require Import Coq.Sets.Image.
Require Import PartialFun.
Require Import Classical_sets.
Require Import PartialFix.
Hint Unfold In.
Implicit Arguments Included [U].
Parameter ON : WO.
Definition OT := M ON.
Definition lt := Lt ON.
Definition le := Le ON.
Notation "a < b" := (lt a b): ord_scope.
Notation "a <= b" := (le a b):ord_scope.
Delimit Scope ord_scope with ord.
Open Scope ord_scope.
Definition ordinal := D ON.
Ltac ordi := match goal with
[ |- ordinal _ ] => eauto with schutte
| _ => idtac
end.
Definition Unbounded (X : Ensemble OT) :=
forall x, ordinal x -> exists y, In X y /\ x < y.
Implicit Arguments denumerable [U].
Axiom AX2 : forall X: Ensemble OT, Included X ordinal ->
(exists a, ordinal a /\
(forall y, X y -> y < a)) ->
denumerable X.
Axiom AX3 : forall X : Ensemble OT,
denumerable X -> (Included X ordinal) ->
exists a, ordinal a /\ (forall y, X y -> y < a).
Axiom inh_OT : OT.
Hint Resolve inh_OT : schutte.
Lemma Unbounded_not_denumerable : forall X, Included X ordinal ->
Unbounded X -> not (denumerable X).
Proof.
red;intros.
case (AX3 H1 H).
intros x (Hx,H'x).
case (H0 _ Hx).
intros y (Hy,H'y).
case (Lt_irreflexive ON x).
apply (Lt_trans ON x y x).
auto.
fold lt;
auto.
Qed.
Lemma denumerable_not_Unbounded : forall X, Included X ordinal ->
denumerable X -> not (Unbounded X).
Proof.
red;intros.
apply Unbounded_not_denumerable with X;auto.
Qed.
Definition progressive (P : OT -> Prop) : Prop :=
forall a, ordinal a -> (forall b, ordinal b -> b < a -> P b) -> P a.
Theorem Induction : forall (P: OT->Prop), progressive P ->
forall a, ordinal a -> P a.
Proof.
intros P Hp.
case (classic (forall a : OT, ordinal a -> P a));[trivial|idtac].
intro H.
case (not_all_ex_not _ (fun a => ordinal a -> P a) H).
intros x Hx.
case (imply_to_and _ _ Hx).
intros Ox P'x.
elimtype False.
case (well_order ON (fun z => ~ P z) x Ox P'x).
intros x0 H0.
assert (forall b, ordinal b -> b < x0 -> P b).
intros.
case H0.
intros H3 (H4,H5).
apply NNPP.
red;intro.
case (H5 _ H1 H6).
intro;subst x0.
case (Lt_irreflexive _ _ H2).
intro; case (Lt_irreflexive _ b).
eapply (Lt_trans ON);eauto.
unfold progressive in Hp.
assert (~ (P x0)).
case H0.
unfold In;
tauto.
apply H2.
apply Hp.
case H0;tauto.
auto.
Qed.
Lemma le_refl : forall alpha, ordinal alpha -> alpha <= alpha.
Proof.
left;auto.
Qed.
Hint Resolve le_refl : schutte.
Lemma eq_le : forall a b, ordinal a -> a = b -> a <= b.
left;auto.
Qed.
Lemma lt_le : forall a b, a < b -> a <= b.
right;auto.
Qed.
Lemma lt_trans : forall a b c, a < b -> b < c -> a < c.
Proof (Lt_trans ON).
Lemma le_lt_trans : forall a b c, a <= b -> b < c -> a < c.
Proof (Le_Lt_trans (Wo:=ON)).
Lemma lt_le_trans : forall a b c, a < b -> b <= c -> a < c.
Proof (Lt_Le_trans (Wo:=ON)).
Lemma le_trans : forall a b c, a <= b -> b <= c -> a <= c.
Proof (Le_trans (Wo := ON)).
Lemma lt_irr : forall a, ~ (a < a).
Proof (Lt_irreflexive ON).
Lemma le_antisym : forall a b, a <= b -> b <= a -> a = b.
Proof (Le_antisym (Wo:=ON)).
Lemma le_eq_or_lt : forall a b, a <= b -> a = b \/ a < b.
Proof.
intros a b [(_,H)|H];auto.
Qed.
Lemma le_not_gt : forall a b, a <= b -> ~ b < a.
Proof.
intros a b H; case (le_eq_or_lt H).
intro;subst b;apply lt_irr.
intros H0 H1;case (lt_irr a);eapply lt_trans;eauto.
Qed.
Hint Resolve eq_le lt_le lt_trans le_trans le_lt_trans
lt_le_trans lt_irr le_not_gt:
schutte.
Lemma lt_ordinal : forall a b, a < b -> ordinal a.
Proof.
intros; unfold ordinal.
generalize (Lt_inc_D1 ON a);auto.
intro.
eapply H0.
eauto.
Qed.
Lemma gt_ordinal : forall a b, a < b -> ordinal b.
Proof.
intros; generalize (Lt_inc_D2 ON a); unfold In.
intro H0;eapply H0.
auto.
Qed.
Lemma le_ordinal : forall a b, a <= b -> ordinal a.
Proof.
destruct 1.
case H;auto.
eapply lt_ordinal; eauto.
Qed.
Lemma ge_ordinal : forall a b, a <= b -> ordinal b.
Proof.
destruct 1.
case H;intros;subst b;auto.
eapply gt_ordinal; eauto.
Qed.
Lemma le_disj : forall alpha beta, alpha <= beta -> alpha = beta \/ alpha < beta.
Proof.
intros.
elim H;auto.
destruct 1;auto.
Qed.
Hint Resolve lt_ordinal gt_ordinal le_ordinal ge_ordinal : schutte.
Lemma all_ord_acc : forall alpha, ordinal alpha -> Acc lt alpha.
intros.
pattern alpha.
apply Induction.
red.
intros.
split.
intros.
apply H1.
ordi.
auto.
auto.
Qed.
Lemma trichotomy : forall a b, ordinal a -> ordinal b ->
a < b \/ a = b \/ b < a.
Proof (Lt_connect ON).
Ltac tricho t u Hname := case (trichotomy t u);
[auto with schutte |
auto with schutte |
intro Hname |
intros [Hname|Hname]].
Lemma lt_or_ge : forall a b, ordinal a -> ordinal b -> a < b \/ b <= a.
Proof.
intros a b Ha Hb; tricho a b H;auto with schutte.
Qed.
Lemma not_gt_le : forall a b, ordinal a -> ordinal b -> ~(b<a) -> a <= b.
intros.
tricho a b H2; auto with schutte.
case (H1 H2).
Qed.
Hint Unfold Included.
Theorem Non_denum : ~ denumerable ordinal.
Proof.
red; intro H.
case (AX3 H).
auto.
intros x (H1,H2).
case (lt_irr x);auto.
Qed.
Definition zero_spec (z:OT) := ordinal z /\
forall a, ordinal a -> z <= a.
Definition zero : OT.
the_i zero_spec.
auto with schutte.
case (AX3 (X:=Empty_set _)).
apply denumerable_empty.
unfold Included; contradiction.
intros x (Hx,H'x).
case (well_order ON ordinal x);auto.
intros z (H1,(_,H2)).
exists z;unfold zero_spec.
repeat split;auto.
intros x1 D1.
generalize (H2 _ D1 D1).
fold lt.
destruct 1; auto with schutte.
intros y (Hy,H'y).
apply le_antisym;auto.
case (H2 y);auto with schutte.
Defined.
Theorem ordinal_zero : ordinal zero.
Proof.
hilbert_e.
destruct 1;auto.
Qed.
Hint Resolve ordinal_zero : schutte.
Lemma le_zero : forall a, ordinal a -> zero <= a.
Proof.
intros;pattern zero; hilbert_e.
unfold zero_spec ;intuition.
Qed.
Lemma not_lt_zero_0 : forall a, ordinal a -> ~ a < zero.
Proof.
intros;apply le_not_gt.
apply le_zero;auto.
Qed.
Lemma not_lt_zero : forall a, ~ a < zero.
Proof.
red; intros.
case (not_lt_zero_0 a (lt_ordinal _ _ H) H).
Qed.
Lemma zero_or_greater : forall a, ordinal a ->
a = zero \/ exists b, ordinal b /\ b < a.
Proof.
intros a Ha.
tricho zero a t;auto with schutte.
right;exists zero;auto with schutte.
case (not_lt_zero a t).
Qed.
Lemma zero_or_positive : forall a, ordinal a ->
a = zero \/ zero < a.
Proof.
intros a Ha.
tricho zero a t;auto with schutte.
case (not_lt_zero a t).
Qed.
Theorem unbounded : forall alpha, ordinal alpha -> exists beta, ordinal beta /\
alpha < beta.
Proof.
intros.
pose (X0 := fun z => z < alpha /\ ordinal z).
assert (denumerable X0).
apply AX2.
unfold X0, Included, In.
intuition.
exists alpha.
split;auto.
unfold X0;intuition.
pose (X:= Add _ X0 alpha).
assert (denumerable X).
unfold X; unfold Add; apply denumerable_union.
auto.
apply denumerable_singleton.
case (AX3 H1).
unfold X; intros x Hx.
case Hx.
2:inversion 1.
2: subst x0; unfold In;auto.
unfold In, X0;tauto.
intros beta (Hb,H'b).
exists beta.
split;auto.
apply H'b.
unfold X;auto.
right;split.
Qed.
Definition the_least : (OT -> Prop) -> OT.
the_fun_i ( fun (X:OT -> Prop) => Inhabited _ X
/\ Included X ordinal)
(fun X l => (is_least_member (ordinal) lt X l)).
exact inh_OT.
destruct 1.
case H.
intros.
generalize (well_order ON a x (H0 _ H1) H1);auto.
destruct 1;intros.
exists x0;repeat split; auto.
case H2;auto.
case H2;auto.
tauto.
case H2;auto.
tauto.
intros; eapply least_member_unicity;eauto.
Defined.
Lemma the_least_ordinal : the_least ordinal = zero.
Proof.
pattern ordinal, (the_least ordinal).
pfun_e.
split;auto with schutte.
exists zero;auto with schutte.
intros b (H,_) H0.
case H0.
intros H1 (_,H2).
case (H2 _ ordinal_zero).
exact ordinal_zero.
auto.
intro H3; case (not_lt_zero _ H3).
Qed.
Lemma the_least_ok : forall X, Inhabited OT X -> Included X ordinal ->
forall a, X a -> the_least X <= a.
Proof.
intros.
pattern X, (the_least X).
pfun_e.
unfold le.
unfold is_least_member;auto.
red.
intros.
decompose [and] H3.
case (H7 a (H0 a H1) H1);auto.
Qed.
Definition succ_spec (a:OT) := is_least_member (ordinal) lt (fun z => a < z).
Definition succ : OT -> OT.
the_fun_i ordinal succ_spec.
exact inh_OT.
intros.
case (unbounded a H).
intros x (Ox, Hx).
case (well_order ON (fun z => lt a z) x Ox Hx);auto.
intros s Hs;exists s.
split;auto.
unfold succ_spec;intros.
eapply least_member_unicity; eauto.
Defined.
Definition is_succ (a:OT) := exists b, ordinal b /\ a = succ b.
Lemma lt_succ : forall a, ordinal a -> a < succ a.
Proof.
intros; pattern a,(succ a).
pfun_e.
destruct 2;tauto.
Qed.
Hint Resolve lt_succ : schutte.
Lemma ordinal_succ : forall a , ordinal a -> ordinal (succ a).
Proof.
intros a H.
pattern a, (succ a).
pfun_e.
destruct 2;auto.
Qed.
Hint Resolve ordinal_succ : schutte.
Lemma succ_rw : forall a, ordinal a -> succ a = the_least
(fun x => a < x).
Proof.
intros.
pattern a, (succ a).
pfun_e.
intros.
pattern (fun x : OT => a < x),(the_least (fun x : OT => a < x)).
pfun_e.
split.
exists (succ a).
red.
auto with schutte.
eauto with schutte.
intros.
generalize ( least_member_unicity ON (X:=fun x : OT => a < x) (a:=b1)(b:=b0) H3).
intro H4;symmetry;apply H4.
exact H1.
Qed.
Lemma lt_succ_le : forall a b,
a < b -> succ a <= b.
Proof.
intros a b H; pattern a,(succ a).
pfun_e.
ordi.
intros.
red in H1.
red in H1; decompose [and] H1.
case (H5 b ).
red;ordi.
auto.
auto with schutte.
auto with schutte.
Qed.
Lemma lt_succ_le_2 : forall a b,
ordinal b ->
a < succ b ->
a <= b.
Proof.
intros.
tricho a b t;eauto with schutte.
case (lt_irr a).
apply lt_le_trans with (succ b).
assumption.
apply lt_succ_le;eauto with schutte.
Qed.
Lemma succ_mono : forall a b, ordinal a -> ordinal b ->
a < b -> succ a < succ b.
Proof.
intros.
eapply le_lt_trans.
eapply lt_succ_le;eauto.
auto with schutte.
Qed.
Implicit Arguments succ_mono [ a b].
Lemma succ_monoR : forall a b, ordinal a -> ordinal b ->
succ a < succ b -> a < b.
Proof.
intros.
tricho a b t; auto with schutte.
subst b; case (lt_irr (succ a)); eauto with schutte.
case (lt_irr (succ a)).
eapply lt_trans;eauto.
apply succ_mono;auto.
Qed.
Lemma succ_injection : forall a b, ordinal a -> ordinal b ->
succ a = succ b -> a=b.
Proof.
intros.
tricho a b t;auto.
generalize (succ_mono H H0 t).
rewrite H1; intro; case (lt_irr (succ b));auto.
generalize (succ_mono H0 H t).
rewrite H1; intro; case (lt_irr (succ b));auto.
Qed.
Lemma succ_zero_diff : forall a , ordinal a -> succ a <> zero.
Proof.
intros; pattern a,(succ a).
pfun_e.
unfold succ_spec.
red;intros.
subst b0.
case H1.
intros.
case H3.
intros.
red in H4.
case (not_lt_zero _ H4).
Qed.
Lemma zero_lt_succ : forall alpha, ordinal alpha -> zero < succ alpha.
Proof.
intros a Ha; apply le_lt_trans with a;eauto with schutte.
apply le_zero;auto.
Qed.
Hint Resolve zero_lt_succ le_zero : schutte.
Reserved Notation "'F' n" (at level 29) .
Fixpoint finite (i:nat) : OT :=
match i with 0 => zero
| S i=> succ (F i)
end
where "'F' i" := (finite i) : ord_scope.
Lemma ordinal_finite : forall i, ordinal (F i).
Proof.
induction i; simpl; auto with schutte.
Qed.
Hint Resolve ordinal_finite : schutte.
Lemma finite_lt_inv : forall i o, o < F i ->
exists j:nat , (j<i)%nat /\ o= F j.
Proof.
induction i.
simpl (F 0).
intros.
case (not_lt_zero _ H ).
simpl (F (S i));intros.
case (lt_succ_le_2 o (F i));auto with schutte.
exists i.
case H0;intros;
subst o;auto with arith.
intro.
case (IHi o H0).
intros.
exists x; case H1;auto with arith.
Qed.
Lemma finite_mono : forall i j, (i<j)%nat -> F i < F j.
Proof.
induction 1.
simpl (finite (S i)).
auto with schutte.
apply lt_trans with (finite m);auto.
simpl (finite (S m)).
apply lt_succ; auto with schutte.
Qed.
Hint Resolve finite_mono : schutte.
Lemma finite_inj : forall i j, F i = F j -> i = j.
Proof.
intros.
case (lt_eq_lt_dec i j).
destruct 1.
case (lt_irr (F i)).
pattern (F i) at 2 ; rewrite H.
apply finite_mono;auto.
auto.
intro; case (lt_irr (F i)).
pattern (F i) at 1 ; rewrite H.
apply finite_mono;auto.
Qed.
Definition is_finite := seq_range finite.
Definition sup_spec X l := is_lub (ordinal) lt X l.
Lemma sup_exists : forall X, denumerable X ->
Included X ordinal ->
ex (sup_spec X).
Proof.
unfold Included, In.
intros X H H0.
case (AX3 H).
auto.
intros x (Hx,H'x).
assert (H''x : forall y : OT, X y -> y=x \/ lt y x).
intuition.
generalize (well_order ON
(fun z => ordinal z /\
(forall y, ordinal y -> X y -> y=z \/ y < z))
x Hx ).
intros.
case H1;intros.
auto.
exists x0.
unfold is_least_member in H2.
repeat split.
case H2.
auto.
case H2.
intros.
intuition.
red.
intros.
case H2.
intros.
apply H11;auto.
intros.
decompose [and] H2.
apply H8.
assumption.
split.
assumption.
intuition.
Qed.
Lemma sup_unicity : forall X l l',
(denumerable X /\
forall x, X x -> ordinal x) ->
sup_spec X l -> sup_spec X l' -> l = l'.
Proof.
intros X l l' _ H H0.
apply le_antisym.
case H.
case H0.
intuition.
case (H7 l' H1);auto with schutte.
case H;case H0;intuition.
case (H6 l H3);auto with schutte.
Qed.
Definition sup (X:OT->Prop) : OT.
the_fun_i ( fun (X:OT -> Prop) => denumerable X /\ Included X ordinal )
sup_spec.
auto with schutte.
exact inh_OT.
intro X;destruct 1 as [H1 H2]; ex_unic_intro;auto.
apply sup_exists;auto.
intros;apply sup_unicity with X;auto.
Defined.
Notation "'|_|' X" := (sup X) (at level 29) : ord_scope.
Definition is_limit (a:OT) := ordinal a /\ a <> zero /\ ~ (is_succ a).
Lemma lt_succ_lt : forall a b, is_limit b ->
a < b -> succ a < b.
Proof.
intros a b (Ob,(Zb,Sb)) H .
case (lt_succ_le a b H).
intros (_,H') ; subst b.
case Sb.
exists a;eauto with schutte.
auto.
Qed.
Lemma sup_upper_bound : forall (X: OT -> Prop) x, denumerable X ->
(forall x, X x -> ordinal x) -> X x -> x <= |_| X.
Proof.
intros X x H H0.
pattern X,(sup X).
pfun_e.
unfold sup_spec;intros.
intuition.
case H2.
intuition.
case (H7 x); auto with schutte.
Qed.
Lemma sup_least_upper_bound : forall (X: OT->Prop) x, denumerable X ->
(forall y, X y -> ordinal y) -> ordinal x ->
(forall y, X y -> y <= x) -> |_| X <= x.
Proof.
intros.
pattern X, (sup X).
pfun_e.
intros .
clear H3.
red in H4.
red in H4; decompose [and] H4.
unfold upper_bound in H6.
case (H7 _ H1);auto with schutte.
intros.
unfold upper_bound;intros.
case (H2 _ H8);auto.
destruct 1;auto.
Qed.
Lemma sup_ordinal : forall X, denumerable X ->
(forall x, X x -> ordinal x) ->
ordinal (|_| X).
Proof.
intros X HX H.
pattern X, (|_| X).
pfun_e.
unfold sup_spec;intuition.
case H1;auto.
Qed.
Hint Resolve sup_ordinal : schutte.
Lemma sup_of_leq : forall a, ordinal a -> a = |_| (fun x => ordinal x /\
x <= a).
Proof.
intros;pattern (fun x => ordinal x /\ x<=a),(|_| (fun x => ordinal x /\ x <= a)).
pfun_e.
intuition.
assert (denumerable (fun x : OT => ordinal x /\ x <= a)).
apply AX2.
unfold Included, In, ordinal;tauto.
exists (succ a).
split; auto with schutte.
destruct 1.
apply le_lt_trans with a;eauto with schutte.
auto.
intros.
red;intros.
case H0.
auto.
destruct 1.
destruct 1.
decompose [and] H3.
case (H5 a H).
unfold upper_bound.
intros; apply le_eq_or_lt;auto.
case H7;auto.
auto.
intro.
case (lt_irr a).
apply le_lt_trans with b0;eauto with schutte.
case (H4 a);unfold In;auto with schutte.
Qed.
Lemma sup_mono : forall (X Y : Ensemble OT),
denumerable X ->
denumerable Y ->
(Included X ordinal) ->
(Included Y ordinal) ->
(forall x, In X x -> exists y, In Y y /\ x <= y) ->
|_| X <= |_| Y.
Proof.
intros.
apply sup_least_upper_bound; auto with schutte.
intros x Hx; case (H3 x Hx); intros y (Hy,Hy').
apply le_trans with y;auto with schutte.
apply sup_upper_bound;auto with schutte.
Qed.
Lemma sup_eq_intro : forall (X Y : Ensemble OT),
denumerable X ->
denumerable Y ->
(Included X ordinal) ->
(Included Y ordinal) ->
(Included X Y) ->
(Included Y X) ->
|_| X = |_| Y.
Proof.
unfold Included, In; intros; apply le_antisym; apply sup_mono;auto with schutte;
intro x;exists x; unfold In;auto with schutte.
Qed.
Lemma lt_sup_exists_leq : forall X, denumerable X ->
(Included X ordinal) ->
forall y, ordinal y -> y < sup X ->
exists x, In X x /\ y <= x.
Proof.
intros.
case (not_all_not_ex _ (fun x => X x /\ y <= x)).
2 : intros x Hx; exists x;auto.
red;intro.
unfold Included, In , ordinal in H0.
assert (forall n, X n -> n < y).
intro.
intro.
apply NNPP.
red;intro.
assert (y < n).
case (trichotomy n y).
apply H0;auto.
auto.
intro; case H5;auto.
destruct 1.
subst n.
case (H3 y).
auto with schutte.
auto.
case (H3 n).
split;auto with schutte.
clear H3.
case (lt_irr y).
eapply lt_le_trans with (|_|X);eauto.
apply sup_least_upper_bound;auto with schutte.
Qed.
Lemma lt_sup_exists_lt : forall X, denumerable X ->
Included X ordinal ->
forall y, ordinal y -> y < sup X ->
exists x, In X x /\ y < x.
Proof.
intros.
unfold Included, In in H0.
case (not_all_not_ex _ (fun x => X x /\ y < x)).
2 : intros x Hx; exists x;auto.
red;intro.
assert (forall n, X n -> n <= y).
intro.
intro.
apply NNPP.
red;intro.
assert (y < n).
case (trichotomy n y).
apply H0;auto.
auto.
intro.
case H5;auto with schutte.
destruct 1.
case H5;auto with schutte.
auto.
case (H3 n).
split;auto with schutte.
assert (sup X <= y).
apply sup_least_upper_bound.
auto.
auto.
auto.
auto.
case (Lt_irreflexive ON y).
eapply Lt_Le_trans;eauto.
Qed.
Definition members (a:OT) := Intersection _ ordinal (fun b => b < a).
Lemma members_eq : forall a b, ordinal a -> ordinal b ->
members a = members b -> a = b.
Proof.
intros.
tricho a b H2.
assert (members b a).
split;auto.
assert (~(members a a)).
red; inversion_clear 1.
case (lt_irr a);auto.
rewrite H1 in H4.
case H4;auto.
auto.
assert (members a b).
split;auto.
assert (~(members b b)).
red;inversion_clear 1.
case (lt_irr b);auto.
rewrite <- H1 in H4.
case H4;auto.
Qed.
Lemma sup_members_succ : forall a, ordinal a ->
(sup (members a)) < a ->
a = succ (|_| (members a)).
Proof.
intros a H;pose (A := sup (members a)).
fold A.
generalize (lt_succ_le A a).
intros.
assert (ordinal A).
unfold A;apply sup_ordinal.
apply AX2.
unfold Included, In, members. destruct 1;tauto.
exists a;unfold members.
split;auto;destruct 1.
auto.
unfold members.
destruct 1.
auto.
case (le_eq_or_lt (H0 H1)).
symmetry;auto.
intro H3.
assert (succ A <= A).
unfold A;apply sup_upper_bound.
apply AX2.
unfold Included. destruct 1; auto.
exists a;unfold members.
split; auto.
destruct 1;auto.
unfold members;destruct 1;auto.
unfold members at 1.
split.
fold A.
unfold In; apply ordinal_succ.
auto.
unfold In.
auto.
case (lt_irr A).
eapply lt_le_trans.
eapply lt_succ;eauto.
auto.
Qed.
Lemma sup_members_not_succ : forall a b, ordinal a -> ordinal b ->
a = sup (members a) -> a <> succ b.
Proof.
intros a b Ha Hb e e1.
generalize (sup_of_leq b Hb).
intro.
assert (sup (members a) = b).
unfold members;rewrite H.
apply sup_eq_intro.
apply AX2.
auto.
apply Intersection_decreases_l.
exists a. split;auto.
destruct 1.
auto.
apply AX2.
unfold Included. destruct 1.
auto.
exists (succ b).
split;auto with schutte.
intros y (Hy,H'y).
eauto with schutte.
apply Intersection_decreases_l.
unfold Included. destruct 1.
auto.
unfold Included. destruct 1.
split; auto.
unfold In in H1.
rewrite e1 in H1.
apply lt_succ_le_2;auto.
unfold Included, In.
intros x (H1,H2).
split;auto with schutte.
unfold In.
rewrite e1.
eapply le_lt_trans;eauto with schutte.
case (lt_irr a).
pattern a at 2;rewrite e1.
rewrite e;rewrite H0.
auto with schutte.
Qed.
Definition omega_limit (f:nat->OT) : OT
:= |_| (seq_range f).
Definition seq_mono (f:nat -> OT) :=
forall i j, (i<j)%nat -> f i < f j.
Lemma seq_mono_intro : forall f,
(forall i, f i < f (S i)) -> seq_mono f.
Proof.
intros f H; unfold seq_mono; induction 1.
auto.
apply (Lt_trans ON) with (f m);auto.
apply H.
Qed.
Lemma seq_mono_inj : forall f,
seq_mono f -> injective _ _ f.
Proof.
unfold injective;intros f H i j H0.
case (lt_eq_lt_dec i j).
destruct 1.
generalize (H _ _ l).
rewrite H0;intro;case (Lt_irreflexive ON ( f j));auto.
auto.
intro l;generalize (H _ _ l).
rewrite H0;intro;case (Lt_irreflexive ON ( f j));auto.
Qed.
Lemma seq_range_denumerable : forall f,
seq_mono f -> denumerable (seq_range f).
Proof.
intros f _.
apply Denumerable.seq_range_denumerable.
Qed.
Hint Resolve seq_range_denumerable seq_mono_intro : schutte.
Lemma lt_omega_limit : forall f , (forall i, ordinal (f i)) ->
seq_mono f ->
forall i, f i < omega_limit f.
Proof.
unfold omega_limit;intros.
apply lt_le_trans with (f (S i)).
eapply H0.
auto.
apply sup_upper_bound;auto with schutte.
destruct 1.
subst x;auto.
exists (S i);auto.
Qed.
Definition omega := omega_limit finite.
Lemma finite_lt_omega : forall i, F i < omega.
Proof.
unfold omega ; intros.
apply lt_omega_limit; auto with schutte.
Qed.
Lemma lt_omega_finite : forall a, a < omega ->
exists i:nat, a = F i.
Proof.
unfold omega;intros a H0.
assert (H:ordinal a).
eauto with schutte.
unfold omega_limit in H0.
generalize (lt_sup_exists_leq (X:=(seq_range finite)) ).
intros.
assert (denumerable (seq_range finite)).
apply seq_range_denumerable.
unfold seq_mono;intros;apply finite_mono;auto.
generalize (H1 H2);clear H1;intros.
assert (forall y : OT, seq_range finite y -> ordinal y).
destruct 1.
subst y;auto with schutte.
generalize (H1 H3);clear H1;intros.
case (H1 a H H0).
destruct 1.
case H5.
intros (_,H6);subst a.
case H4.
intros.
exists x0;auto.
case H4;intros.
subst x.
case (finite_lt_inv x0 a);auto.
intros x (H8,H9);exists x;auto.
Qed.
Lemma ordinal_omega_limit : forall s, (forall i, s i < s (S i)) ->
ordinal (omega_limit s).
Proof.
unfold omega_limit.
intros;apply sup_ordinal.
apply seq_range_denumerable;auto.
red; apply seq_mono_intro; auto.
destruct 1.
subst x;auto with schutte.
eauto with schutte.
Qed.
Lemma ordinal_omega : ordinal omega.
unfold omega; apply ordinal_omega_limit.
auto with schutte arith.
Qed.
Lemma lt_omega_limit_lt_exists_lt : forall alpha s,
(forall i, s i < s (S i)) ->
alpha < omega_limit s ->
exists j, alpha < s j.
Proof.
intros.
unfold omega_limit in H0.
assert (exists y, In (seq_range s) y /\ alpha < y).
apply lt_sup_exists_lt; auto with schutte.
red;red;red.
destruct 1;auto.
subst x;eauto with schutte.
fold ordinal;eauto with schutte.
eauto with schutte.
case H1; intros y Hy.
case Hy;destruct 1.
subst y;exists x;auto.
Qed.
Hint Resolve ordinal_omega ordinal_omega_limit : schutte.
Lemma is_limit_omega : is_limit omega.
Proof.
unfold is_limit.
repeat split; auto with schutte.
red;intro.
absurd (F 1 < zero).
apply not_lt_zero;auto with schutte.
rewrite <- H.
apply finite_lt_omega.
red;intro.
case H.
intros x (Ox,Ex).
assert (x < omega).
rewrite Ex;auto with schutte.
case (lt_omega_finite _ H0).
intros; subst x.
assert (omega = F (S x0)).
simpl;auto.
case (lt_irr omega);auto with schutte.
pattern omega at 1;rewrite H1;auto with schutte.
apply finite_lt_omega;auto with schutte.
Qed.
Lemma not_is_succ_zero : ~ (is_succ zero).
Proof.
red. intros (b, (Hb,Hb')).
case (succ_zero_diff _ Hb).
auto.
Qed.
Lemma not_is_limit_zero : ~ (is_limit zero).
Proof.
unfold is_limit.
tauto.
Qed.
Lemma not_is_limit_succ : forall a, ordinal a -> is_succ a -> ~ (is_limit a).
Proof.
unfold is_limit;tauto.
Qed.
Lemma not_is_succ_limit : forall a, ordinal a -> is_limit a -> ~(is_succ a).
Proof.
unfold is_limit;tauto.
Qed.
Lemma is_limit_ordinal : forall a, is_limit a -> ordinal a.
Proof.
unfold is_limit;tauto.
Qed.
Lemma is_succ_ordinal : forall a, is_succ a -> ordinal a.
Proof.
unfold is_succ.
intros a (b,(Hb,H'b)).
subst a; auto with schutte.
Qed.
Hint Resolve is_limit_ordinal is_succ_ordinal : schutte.
Lemma denumerable_members : forall a, ordinal a -> denumerable (members a).
Proof.
intros a Ha.
apply AX2.
unfold members.
apply Intersection_decreases_l.
exists a; split ; auto.
destruct 1. auto.
Qed.
Hint Resolve denumerable_members : schutte.
Lemma le_sup_members : forall a, ordinal a -> |_| (members a) <= a.
Proof.
intros; apply sup_least_upper_bound; auto with schutte.
destruct 1; auto.
destruct 1;auto.
right; auto.
Qed.
Lemma is_limit_sup_members : forall a, is_limit a -> a = |_| (members a).
Proof.
intros.
case (le_sup_members a);auto with schutte.
intuition.
intro; generalize (sup_members_succ a).
intuition.
generalize (H1 (is_limit_ordinal H) H0).
intro.
case (not_is_limit_succ (a:=a));auto with schutte.
exists (|_|members a).
split;auto.
apply sup_ordinal;auto with schutte.
destruct 1;auto.
Qed.
Lemma sup_members_disj : forall a, ordinal a -> a = sup (members a) ->
a = zero \/ is_limit a.
Proof.
intros.
unfold is_limit.
case (classic (a=zero)).
auto.
right;repeat split;auto.
red;intro H2.
case H2;intros x (H3,H4).
case (sup_members_not_succ _ H H3 H0).
auto.
Qed.
Lemma ordinal_sup_members : forall a, ordinal a ->
ordinal (sup (members a)).
Proof.
intros; apply sup_ordinal; auto with schutte.
destruct 1;auto.
Qed.
Theorem classification : forall a, ordinal a -> a = zero \/
is_succ a \/
is_limit a.
Proof.
intros a Ha.
case (le_sup_members a Ha).
intro;case (sup_members_disj Ha);auto with schutte.
case H;auto.
right.
left.
exists (sup (members a)).
split.
apply ordinal_sup_members;auto.
apply sup_members_succ;auto.
Qed.
Definition set_eq (X Y: OT -> Prop) := forall a, ordinal a -> (X a <-> Y a).
Implicit Arguments Same_set [U].
Lemma members_omega : Same_set (members omega) is_finite.
Proof.
unfold Same_set;split.
red. unfold members, In.
destruct 1.
case (lt_omega_finite x H0).
intros;exists x0;auto.
unfold Included, members.
destruct 1.
subst x;split;red;auto with schutte.
apply finite_lt_omega.
Qed.
Inductive closed (B : Ensemble OT) : Prop :=
closed_intro : Included B ordinal ->
(forall M, Included M B -> Inhabited _ M -> denumerable M -> In B (sup M )) ->
closed B.
Inductive continuous (f:OT->OT)(A B : Ensemble OT) : Prop :=
continuous_intro : fun_codomain A B f ->
closed A ->
(forall U, Included U A -> Inhabited _ U ->
denumerable U -> sup (image U f) = f (sup U)) ->
continuous f A B.
Lemma Not_Unbounded_bounded : forall X, Included X ordinal ->
not (Unbounded X) ->
exists beta, ordinal beta /\ forall x, In X x -> x < beta.
Proof.
intros.
apply NNPP.
red;intro.
assert (forall beta, ordinal beta ->
exists x, In X x /\ beta <= x).
Focus 2.
clear H1.
case H0.
red;intro.
intros.
case (H2 (succ x)).
auto with schutte.
intros.
exists x0;split;auto with schutte.
case H3;auto.
case H3;intros.
apply lt_le_trans with (succ x).
auto with schutte.
auto.
intro.
intros.
change (exists x:OT, (fun y => In X y /\ beta <= y) x).
apply not_all_not_ex.
red;intro.
case H1.
exists beta; split;auto.
intros.
tricho x beta H5;auto with schutte.
apply H;auto.
case (H3 x).
split;auto with schutte.
case (H3 x);split;auto with schutte.
Qed.
Lemma Not_Unbounded_denumerable : forall X, Included X ordinal ->
not (Unbounded X) -> denumerable X.
intros;eapply AX2;eauto.
case (Not_Unbounded_bounded H);auto.
intros.
exists x;auto.
Qed.
Lemma not_denumerable_unbounded : forall X, Included X ordinal ->
not (denumerable X) -> Unbounded X.
Proof.
intros.
apply NNPP.
red;intro.
apply H0;apply Not_Unbounded_denumerable;auto.
Qed.
Lemma le_alpha_zero : forall alpha, alpha <= zero -> alpha = zero.
Proof.
intros.
apply le_antisym;auto.
apply le_zero.
eauto with schutte.
Qed.