Library schutte.AP
Add LoadPath "../prelude".
Add LoadPath "../hilbert".
Add LoadPath "../denumerable".
Require Import Arith.
Require Import Epsilon.
Require Import Ensembles.
Require Import Denumerable.
Require Import Schutte.
Require Import Ordering_Functions.
Require Import PartialFun.
Require Import Plus.
Require Import Well_Orders.
Set Implicit Arguments.
Inductive AP (alpha : OT) : Prop :=
AP_intro : zero < alpha -> (forall beta, beta < alpha ->
beta + alpha = alpha) ->
AP alpha.
Lemma not_AP_inv : forall alpha,
zero < alpha ->
~ (AP alpha) ->
exists beta,zero < beta /\ beta < alpha /\ alpha < beta + alpha .
intros.
apply Classical_Prop.NNPP.
red;intro;apply H0.
split.
auto.
intros.
tricho (beta+alpha) alpha H3.
eauto with schutte.
eauto with schutte.
case (lt_irr alpha).
apply le_lt_trans with (beta+alpha).
apply le_plus_r;eauto with schutte.
auto.
auto.
case H1.
exists beta;auto.
split;auto.
tricho zero beta H4. eauto with schutte.
auto.
subst beta.
rewrite zero_plus_alpha in H3.
case (lt_irr alpha);auto.
eauto with schutte.
case (not_lt_zero beta).
eauto with schutte.
Qed.
Lemma not_AP_inv2 : forall alpha, zero < alpha -> ~AP alpha ->
exists beta, exists gamma,
zero < beta /\ zero < gamma /\
beta < alpha /\ gamma < alpha /\
alpha = beta + gamma.
Proof.
intros.
case (not_AP_inv H H0).
intros khi (Hkhi, H'khi).
exists khi.
case (minus_exists (alpha:=khi) (beta:= alpha)).
eauto with schutte.
case H'khi;eauto with schutte.
intros eta (H1,H2).
exists eta.
split.
auto.
split;auto.
tricho zero eta H3.
auto.
subst eta.
rewrite alpha_plus_zero in H2.
decompose [and] H'khi.
subst alpha; case (lt_irr khi);auto.
eauto with schutte.
case (not_lt_zero eta);eauto with schutte.
decompose [and] H'khi.
split;auto.
split;auto.
tricho zero khi H5.
eauto with schutte.
tricho eta alpha H6. eauto with schutte.
auto. subst eta.
case (lt_irr (khi+alpha));eauto with schutte.
case (lt_irr (khi + eta));eauto with schutte.
apply lt_trans with (khi+alpha);eauto with schutte.
apply plus_mono_r;eauto with schutte.
subst khi.
case (lt_irr zero);auto.
case (not_lt_zero khi);eauto with schutte.
Qed.
Lemma AP_one : AP (F 1).
Proof.
split.
simpl (F 1).
auto with schutte.
simpl (F 1).
intros.
assert (beta <= zero).
eapply lt_succ_le_2;eauto with schutte.
rewrite (le_alpha_zero H0).
rewrite zero_plus_alpha;eauto with schutte.
Qed.
Lemma least_AP :is_least_member ordinal lt AP (F 1).
Proof.
split.
red;auto with schutte.
split.
red;apply AP_one.
intros.
case H0.
intros.
tricho x (F 1) H3; auto with schutte.
simpl (F 1) in H3.
assert (x = zero).
apply le_alpha_zero;auto with schutte.
apply lt_succ_le_2;eauto with schutte.
subst x.
case (lt_irr zero); auto.
Qed.
Lemma AP_omega : AP omega.
Proof.
repeat split.
apply lt_trans with (F 1).
simpl (F 1); eauto with schutte.
apply finite_lt_omega.
intros.
case (lt_omega_finite _ H).
intros;subst beta.
apply finite_plus_ge_omega;eauto with schutte.
Qed.
Lemma zero_lt_omega : zero < omega.
Proof.
apply lt_trans with (F 1). eauto with schutte.
apply finite_lt_omega;auto.
Qed.
Hint Resolve zero_lt_omega : schutte.
Lemma AP_finite_eq_one : forall n, AP (F n) -> n = 1.
Proof.
intro n; case n.
inversion 1.
simpl in H0.
case (lt_irr zero);auto.
intro n0;case n0.
auto.
inversion_clear 1.
generalize (H1 (F 1)).
intros.
absurd (F 1 + F S (S n1) = F S (S n1)).
rewrite <- plus_FF.
simpl.
red;intro.
case (lt_irr (succ (succ (F n1)))).
pattern (succ (succ (F n1))) at 2; rewrite <- H2.
auto with schutte.
apply H.
apply finite_mono.
auto with arith.
Qed.
Lemma omega_second_AP : is_least_member ordinal lt
(fun alpha => (F 1 < alpha) /\ AP alpha)
omega.
Proof.
split.
red; auto with schutte.
split; auto with schutte.
red; split.
apply finite_lt_omega.
apply AP_omega.
intros.
red in H0.
tricho x (omega) H1;auto with schutte.
case (lt_omega_finite _ H1).
intros; subst x.
decompose [and] H0.
generalize (AP_finite_eq_one _ H3).
intro;subst x0.
case (lt_irr (F 1)).
auto.
Qed.
Lemma AP_plus_closed : forall alpha, AP alpha ->
forall beta gamma, beta < alpha ->
gamma < alpha ->
beta + gamma < alpha.
Proof.
intros.
case H.
intros.
generalize (plus_mono_r beta gamma alpha).
intro.
replace alpha with (beta+alpha).
apply H4; eauto with schutte.
auto.
Qed.
Section AP_Unbounded.
Variable alpha : OT.
Hypothesis o_alpha : ordinal alpha.
Let seq := (fix seq (n:nat) :=
match n with 0 => succ alpha
| S p => (seq p) + (seq p)
end).
Let beta := omega_limit seq.
Remark mono_seq : forall i, seq i < seq (S i).
induction i.
simpl.
pattern (succ alpha) at 1.
rewrite <- alpha_plus_zero.
2:eauto with schutte.
apply plus_mono_r; eauto with schutte.
simpl.
simpl in IHi.
pattern (seq i + seq i) at 1; rewrite <- alpha_plus_zero;auto with schutte.
apply plus_mono_r. eauto with schutte.
apply le_lt_trans with (seq i).
eauto with schutte.
auto.
eauto with schutte.
Qed.
Hint Resolve mono_seq.
Remark o_beta : ordinal beta.
Proof.
unfold beta.
apply ordinal_omega_limit; auto with schutte.
Qed.
Remark alpha_lt_beta : alpha < beta.
Proof.
apply lt_trans with (seq 0).
simpl.
auto with schutte.
unfold beta.
apply lt_omega_limit;auto with schutte.
intros; eapply lt_ordinal; eauto.
Qed.
Remark zero_lt_beta : zero < beta.
apply le_lt_trans with alpha.
eauto with schutte.
apply alpha_lt_beta.
Qed.
Section ksi_fixed.
Variable ksi: OT.
Hypothesis o_ksi : ordinal ksi.
Hypothesis lt_ksi : ksi < beta.
Remark lt_beta_exisys : exists n, ksi < seq n.
unfold beta.
intros.
case (lt_omega_limit_lt_exists_lt ksi seq mono_seq); auto.
intros;exists x;auto.
Qed.
Lemma inh_nat : nat.
exact 0.
Qed.
Let n := epsilon inh_nat (fun n => ksi < seq n).
Remark ksi_plus_seq_n : forall (m:nat), (n <= m)%nat -> ksi + seq m <= beta.
intros.
apply le_trans with (seq (S m)).
simpl.
apply plus_mono_weak_l.
eapply lt_ordinal.
eapply mono_seq.
apply le_trans with (seq n).
right.
pattern n; hilbert_e.
apply lt_beta_exisys.
elim H.
left;split;auto with schutte.
red;red;eapply lt_ordinal;eauto.
intros; apply le_trans with (seq m0);auto.
right;apply mono_seq.
unfold beta.
right;apply lt_omega_limit.
intros; eapply lt_ordinal;eauto.
red.
apply seq_mono_intro.
exact mono_seq.
Qed.
Lemma ksi_plus_seq_n' : forall (m:nat), ksi + seq m <= beta.
Proof.
intros.
case (le_or_lt n m).
intros.
apply ksi_plus_seq_n;auto.
intros.
apply le_trans with (ksi + seq n).
apply plus_mono_r_weak;auto.
eapply lt_ordinal;eauto.
eapply lt_ordinal;eauto.
assert (m <= n)%nat.
auto with arith.
right;fold lt.
induction H.
apply mono_seq.
apply lt_trans with (seq m0);auto.
apply IHle.
auto with arith.
pattern n;hilbert_e.
apply lt_beta_exisys.
intros.
apply le_trans with (seq (S a)).
simpl (seq (S a)).
apply plus_mono_weak_l.
eapply lt_ordinal;eauto.
right;fold lt;apply H0.
unfold beta.
right; apply lt_omega_limit; auto with schutte.
eauto with schutte.
Qed.
Lemma ksi_plus_beta : ksi + beta <= beta.
Proof.
unfold beta at 1.
unfold omega_limit.
rewrite alpha_plus_sup.
apply sup_least_upper_bound. eauto with schutte.
apply R1 with ordinal (Greater ksi).
apply plus_ordering; auto.
apply seq_range_denumerable;auto.
apply seq_mono_intro.
exact mono_seq.
red; destruct 1; eauto with schutte.
destruct 1.
decompose [and] H;subst y.
apply ordinal_plus. eauto with schutte.
case H0.
intros; subst x.
eauto with schutte.
eauto with schutte.
destruct 1.
decompose [and] H.
subst y.
decompose [and] H.
case H1.
intros;subst x.
apply ksi_plus_seq_n'.
eauto with schutte.
exists (seq 0).
red.
exists 0; trivial.
eauto with schutte.
red;destruct 1.
subst x.
red;eauto with schutte.
Qed.
Lemma ksi_plus_beta_eq : ksi + beta = beta.
apply le_antisym.
apply ksi_plus_beta.
apply le_plus_r;auto.
apply o_beta.
Qed.
End ksi_fixed.
Lemma LLL : alpha < beta /\ AP beta.
Proof.
split.
apply alpha_lt_beta.
split.
apply zero_lt_beta.
intros; apply ksi_plus_beta_eq; eauto with schutte.
Qed.
End AP_Unbounded.
Theorem AP_unbounded : Unbounded AP.
Proof.
red.
intros.
generalize (LLL x H).
exists (omega_limit
(fix seq (n : nat) : M ON :=
match n with
| O => succ x
| S p => seq p + seq p
end)).
tauto.
Qed.
Section AP_closed.
Variable M : Ensemble OT.
Hypothesis OM : Included M AP.
Hypothesis inhM : Inhabited _ M.
Hypothesis denM : denumerable M.
Remark inc_M : Included M ordinal.
Proof.
red.
intros.
case (OM H);eauto with schutte.
Qed.
Remark supM_gt0 : zero < |_| M.
Proof.
case inhM.
intros.
apply lt_le_trans with x.
case (OM H).
auto.
apply sup_upper_bound; auto with schutte.
intros. generalize (OM H).
destruct 1.
generalize (OM H0).
destruct 1;eauto with schutte.
Qed.
Lemma AP_sup : In AP (|_| M).
Proof.
red.
split.
apply supM_gt0.
intros ksi Hksi.
case (lt_sup_exists_lt denM inc_M ksi).
eauto with schutte.
auto.
intros alpha (Malpha, ksialpha).
apply le_antisym.
2:apply le_plus_r;eauto with schutte.
rewrite alpha_plus_sup.
2:eauto with schutte.
apply sup_mono.
apply R1 with ordinal (Greater ksi).
apply plus_ordering; eauto with schutte.
auto.
red. intros.
case (OM H); eauto with schutte.
auto.
red;destruct 1.
decompose [and] H;subst x.
red;apply ordinal_plus;auto with schutte.
eauto with schutte.
case (OM H0);eauto with schutte.
apply inc_M.
intros.
case H.
intros beta (Mbeta,ebeta).
case (lt_or_ge beta alpha);auto with schutte.
apply inc_M.
auto.
eauto with schutte.
exists alpha.
split;auto.
subst x.
case (OM Mbeta).
intros.
right.
fold lt.
apply lt_le_trans with (ksi + alpha).
apply plus_mono_r; eauto with schutte.
left.
split;auto.
red.
fold ordinal.
eapply ordinal_plus;eauto with schutte.
case (OM Malpha).
intros.
auto.
exists beta.
split.
auto.
left.
split.
subst x;red;apply ordinal_plus;eauto with schutte.
subst x.
case (OM Mbeta).
intros.
apply H2.
apply lt_le_trans with alpha;auto.
auto.
auto.
apply inc_M.
Qed.
End AP_closed.
Theorem AP_closed : closed AP.
split.
red; destruct 1 ;eauto with schutte.
intros.
apply AP_sup;auto.
Qed.
Definition phi0 := the_ordering_function AP.
Lemma AP_Inc_ordinal : Included AP ordinal.
Proof.
red; destruct 1; eauto with schutte.
Qed.
Lemma AP_o_segment : the_ordering_segment AP = ordinal.
Proof.
intros;apply O_segment_unbounded.
eapply SA2.
eapply the_ordering_function_ok;eauto.
apply AP_Inc_ordinal.
generalize
(ordering_unbounded_unbounded
(A:=the_ordering_segment AP)
(B:=AP)
(f:=phi0)).
intros.
generalize (H (AP_Inc_ordinal)).
intro; clear H.
unfold phi0.
generalize (H0 (the_ordering_function_ok AP_Inc_ordinal )).
destruct 1.
apply H.
apply AP_unbounded;auto.
Qed.
Theorem normal_phi0 : normal phi0 AP.
apply TH_13_6R with ordinal.
red;destruct 1;red;eauto with schutte.
unfold phi0.
pattern (the_ordering_function AP).
hilbert_e.
exists (the_ordering_function AP).
apply the_ordering_function_ok.
apply AP_Inc_ordinal.
intros.
rewrite AP_o_segment in H.
auto.
apply AP_closed.
apply AP_unbounded.
Qed.
Lemma phi0_ordering : ordering_function phi0 ordinal AP.
Proof.
intros.
unfold phi0.
pattern (the_ordering_function AP); epsilon_elim.
exists (the_ordering_function AP).
apply the_ordering_function_ok.
apply AP_Inc_ordinal.
rewrite <- (AP_o_segment);auto.
Qed.
Lemma phi0_elim : forall P : (OT->OT)->Prop,
(forall f: OT->OT,
ordering_function f ordinal AP-> P f) ->
P phi0.
Proof.
intros.
apply H.
apply phi0_ordering.
Qed.
Lemma AP_phi0 : forall alpha, ordinal alpha -> AP (phi0 alpha).
intros; pattern phi0; apply phi0_elim.
destruct 1.
decompose [and] H1.
apply H4;auto.
Qed.
Lemma ordinal_phi0 : forall alpha, ordinal alpha -> ordinal (phi0 alpha).
Proof.
intros.
pattern (phi0 alpha).
apply phi0_elim; auto with schutte.
intros.
eapply ordering_function_ordinal_B;eauto.
Qed.
Hint Resolve ordinal_phi0: schutte.
Lemma phi0_zero : phi0 zero = F 1.
generalize (order_function_least_least phi0_ordering).
generalize least_AP.
intros.
rewrite (least_member_unicity ON H H0);eauto.
Qed.
Lemma phi0_mono : forall alpha beta, alpha < beta ->
phi0 alpha < phi0 beta.
intros.
pattern phi0.
apply phi0_elim.
intros;eapply ordering_function_mono;eauto with schutte.
Qed.
Lemma phi0_mono_weak : forall alpha beta, alpha <= beta ->
phi0 alpha <= phi0 beta.
Proof.
destruct 1.
decompose [and] H.
subst beta; auto with schutte.
right;apply phi0_mono;auto.
Qed.
Lemma phi0_mono_R : forall alpha beta, ordinal alpha -> ordinal beta ->
phi0 alpha < phi0 beta -> alpha < beta.
Proof.
intros alpha beta Oalpha Obeta.
pattern phi0.
apply phi0_elim.
intros;eapply ordering_function_monoR; eauto;ordi.
Qed.
Lemma phi0_mono_R_weak : forall alpha beta, ordinal alpha -> ordinal beta ->
phi0 alpha <= phi0 beta -> alpha <= beta.
Proof.
intros alpha beta Oalpha Obeta.
pattern phi0.
apply phi0_elim.
intros.
eapply ordering_function_mono_weakR;eauto;ordi.
Qed.
Lemma phi0_inj : forall alpha beta, ordinal alpha -> ordinal beta ->
phi0 alpha = phi0 beta ->alpha = beta.
Proof.
intros; apply le_antisym; apply phi0_mono_R_weak;auto;ordi;
auto with schutte.
Qed.
Lemma phi0_positive : forall alpha, ordinal alpha -> zero < phi0 alpha.
Proof.
intros.
apply lt_le_trans with (phi0 zero).
rewrite phi0_zero.
eauto with schutte arith.
pattern phi0 ; apply phi0_elim.
intros.
eapply ordering_function_mono_weak; eauto with schutte.
Qed.
Lemma plus_lt_phi0 : forall ksi alpha, ordinal alpha ->
ksi < phi0 alpha ->
ksi + phi0 alpha = phi0 alpha.
Proof.
intros ksi alpha Halpha.
pattern (phi0 alpha).
apply phi0_elim.
intros f Hf.
assert (AP (f alpha)).
case Hf.
intros.
decompose [and] H0; clear H0.
apply H3.
red;auto.
case H.
auto.
Qed.
Lemma phi0_alpha_phi0_beta : forall alpha beta, alpha < beta ->
phi0 alpha + phi0 beta =
phi0 beta.
Proof.
intros.
apply plus_lt_phi0; eauto with schutte.
apply phi0_mono.
auto.
Qed.
Lemma phi0_sup : forall U, Included U ordinal -> Inhabited _ U ->
denumerable U ->
phi0 (sup U) = sup (image U phi0).
Proof.
intros.
case normal_phi0.
destruct 2;symmetry; auto.
Qed.
Lemma phi0_of_limit : forall alpha, is_limit alpha ->
phi0 alpha =
sup (image (members alpha) phi0).
Proof.
intros.
pattern alpha at 1;
rewrite (is_limit_sup_members H).
case normal_phi0.
destruct 2;symmetry;auto.
apply H3.
red;destruct 1;auto.
exists zero.
red.
red.
split.
red;auto with schutte.
red.
case H;auto.
destruct 2.
tricho zero alpha HH.
auto.
subst alpha; case (H5);auto.
case (not_lt_zero alpha);auto.
apply denumerable_members;auto.
case H;auto.
Qed.
Lemma AP_to_phi0 : forall alpha, AP alpha -> exists beta, ordinal beta /\
alpha = phi0 beta.
intros.
pattern phi0;apply phi0_elim.
destruct 1.
decompose [and] H1.
case (H3 _ H).
intro x;exists x.
split;auto.
case H5;auto.
case H5;auto.
Qed.
Definition log (alpha : OT) := sup (fun beta => ordinal beta /\
phi0 beta <= alpha).
Lemma log_ordinal : forall alpha, zero < alpha -> ordinal (log alpha).
unfold log.
intros.
apply sup_ordinal.
apply AX2.
red.
destruct 1.
red;auto.
exists (succ alpha).
split;ordi.
destruct 1.
apply le_lt_trans with (phi0 y);auto.
pattern phi0;apply phi0_elim.
intros;
eapply ordering_le;eauto.
apply le_lt_trans with alpha;auto.
eauto with schutte.
tauto.
Qed.
Lemma phi0_log_le : forall alpha, zero < alpha ->
phi0 (log alpha) <= alpha.
Proof.
intros; unfold log.
rewrite phi0_sup.
apply sup_least_upper_bound.
apply R1 with ordinal AP.
apply phi0_ordering.
apply AX2.
red.
destruct 1.
red;auto.
exists (succ alpha).
split;ordi.
destruct 1.
apply le_lt_trans with (phi0 y);auto.
pattern phi0;apply phi0_elim.
intros;
eapply ordering_le;eauto.
apply le_lt_trans with alpha;auto.
eauto with schutte.
red; destruct 1; eauto with schutte.
red.
destruct 1.
case H0.
destruct 1.
fold ordinal.
intro;subst y;ordi.
ordi.
destruct 1.
decompose [and] H0.
red in H1.
decompose [and] H1.
subst y;auto.
red.
destruct 1.
red;auto.
exists zero.
red.
split.
auto with schutte.
rewrite phi0_zero.
simpl;apply lt_succ_le.
ordi.
ordi.
auto.
apply AX2.
red;destruct 1.
red.
auto.
exists (succ alpha).
split;ordi.
destruct 1.
apply le_lt_trans with (phi0 y);auto.
pattern phi0;apply phi0_elim.
intros;
eapply ordering_le;eauto.
apply le_lt_trans with alpha;auto.
eauto with schutte.
Qed.
Lemma AP_plus_AP : forall alpha beta gamma, ordinal alpha ->
zero < beta -> ordinal gamma ->
phi0 alpha + beta = phi0 gamma -> alpha < gamma /\
beta = phi0 gamma.
Proof.
intros.
tricho alpha gamma H3.
split;auto.
tricho beta (phi0 gamma) H4.
auto.
ordi.
case (lt_irr (phi0 gamma)).
pattern (phi0 gamma) at 1.
rewrite <- H2.
apply AP_plus_closed.
apply AP_phi0;
eauto with schutte.
apply phi0_mono;auto.
auto.
auto.
rewrite <- H2 in H4.
case (lt_irr beta).
eapply le_lt_trans;eauto.
apply le_plus_r.
ordi.
ordi.
subst gamma.
case (lt_irr (phi0 alpha)).
pattern (phi0 alpha) at 2.
rewrite <- H2.
pattern (phi0 alpha) at 1; rewrite <- alpha_plus_zero.
apply plus_mono_r;auto.
ordi.
ordi.
assert( phi0 alpha <= phi0 gamma).
rewrite <- H2.
apply le_plus_l.
ordi.
ordi.
case (le_not_gt H4).
apply phi0_mono;auto.
Qed.
Lemma is_limit_phi0 : forall alpha, zero < alpha ->
is_limit (phi0 alpha).
Proof.
intros.
split.
ordi.
split.
red.
intros.
case (lt_irr zero).
apply lt_le_trans with alpha;auto.
rewrite <- H0.
pattern phi0; apply phi0_elim.
intros.
eapply ordering_le;eauto.
ordi.
red.
destruct 1.
decompose [and] H0.
generalize (AP_phi0 alpha).
intro.
case H3.
ordi.
intros.
rewrite H2 in H5.
assert (x < succ x).
auto with schutte.
generalize (H5 _ H6).
rewrite plus_of_succ; auto.
intros.
assert (zero < x).
tricho zero x H8.
auto.
subst x.
replace (succ zero) with (F 1) in H2.
rewrite <- phi0_zero in H2.
case (lt_irr (phi0 zero)).
pattern (phi0 zero) at 2; rewrite <- H2.
apply phi0_mono;auto.
simpl;auto.
case (not_lt_zero x).
auto.
assert (x < x+x).
pattern x at 1;rewrite <- alpha_plus_zero.
apply plus_mono_r;auto.
auto.
assert (ordinal (x+x)).
ordi.
generalize (succ_mono H1 H10 H9).
rewrite <- H7.
intros; apply lt_irr with (succ (x+x)).
auto.
Qed.