Library schutte.Plus
Add LoadPath "../hilbert".
Add LoadPath "../prelude".
Add LoadPath "../denumerable".
Require Import Arith.
Require Import Epsilon.
Require Import Ensembles.
Require Import Schutte.
Require Import Ordering_Functions.
Require Import PartialFun.
Require Import Denumerable.
Set Implicit Arguments.
Definition Greater alpha := fun beta => alpha <= beta.
Definition plus alpha := the_ordering_function (Greater alpha).
Lemma Greater_inc_ord : forall alpha, ordinal alpha ->
Included (Greater alpha) ordinal.
Proof.
red;intros.
case H0;auto.
destruct 1.
subst x;auto.
intro.
red;fold ordinal;apply gt_ordinal with alpha;auto.
Qed.
Hint Resolve Greater_inc_ord.
Lemma Unbounded_Greater : forall alpha0, ordinal alpha0 ->
Unbounded (Greater alpha0).
Proof.
red.
intros.
tricho alpha0 x H3.
exists (succ x);split; auto with schutte.
red.
red.
right.
apply lt_trans with x.
auto.
auto with schutte.
subst alpha0.
exists (succ x);auto with schutte.
split;auto with schutte.
red;red.
auto with schutte.
exists (succ alpha0).
split.
red;red.
auto with schutte.
apply lt_trans with alpha0;auto with schutte.
Qed.
Lemma Greater_o_segment : forall alpha0, ordinal alpha0 ->
the_ordering_segment (Greater alpha0) = ordinal.
Proof.
intros;apply O_segment_unbounded.
pattern (the_ordering_segment (Greater alpha0)).
hilbert_e.
generalize (B_of (Greater_inc_ord H)).
auto.
intros.
eapply ordering_function_seg;eauto.
generalize
(ordering_unbounded_unbounded
(A:=the_ordering_segment (Greater alpha0))
(B:=Greater alpha0)
(f:=plus alpha0)).
intros.
generalize (H0 (Greater_inc_ord H)).
intro; clear H0.
unfold plus.
generalize (H1 (the_ordering_function_ok (Greater_inc_ord H))).
destruct 1.
apply H0.
apply Unbounded_Greater;auto.
Qed.
Lemma plus_ordering : forall alpha, ordinal alpha ->
ordering_function (plus alpha)
ordinal
(Greater alpha).
Proof.
intros.
unfold plus.
pattern (the_ordering_function (Greater alpha)).
hilbert_e.
exists (the_ordering_function (Greater alpha));auto.
apply the_ordering_function_ok;auto.
rewrite <- (Greater_o_segment alpha);auto.
Qed.
Lemma plus_elim : forall alpha,
ordinal alpha ->
forall P : (OT->OT)->Prop,
(forall f: OT->OT,
ordering_function f ordinal (Greater alpha)-> P f) ->
P (plus alpha).
Proof.
intros.
apply H0.
apply plus_ordering.
auto.
Qed.
Lemma normal_plus_alpha : forall alpha, ordinal alpha ->
normal (plus alpha) (Greater alpha).
Proof.
intros.
unfold plus;pattern (the_ordering_function (Greater alpha)).
hilbert_e.
exists (the_ordering_function (Greater alpha));auto.
apply the_ordering_function_ok.
auto.
intros.
eapply TH_13_6R with (A:= the_ordering_segment (Greater alpha))(f := a).
auto.
apply H0.
split.
auto.
intros.
red.
red.
case H2;intros.
apply le_trans with x;auto.
apply H1;auto.
apply sup_upper_bound; auto.
intros.
apply ge_ordinal with alpha.
apply H1.
auto.
apply Unbounded_Greater;auto.
Qed.
Notation "alpha + beta " := (plus alpha beta) : ord_scope.
Lemma alpha_plus_zero : forall alpha, ordinal alpha -> alpha + zero = alpha.
Proof.
intros.
pattern (plus alpha).
apply plus_elim;eauto.
intros.
case (order_function_least_least H0).
intros H1 (H2,H3).
case (H3 alpha);auto.
red;red.
auto with schutte.
intro.
case H2.
symmetry;tauto.
intro; case (lt_irr alpha);auto.
apply lt_trans with (f zero);auto.
Qed.
Remark Greater_zero : (Greater zero : Ensemble OT)= ordinal.
apply Extensionality_Ensembles.
split.
apply Greater_inc_ord.
auto with schutte.
unfold Greater.
red.
red.
eauto with schutte.
Qed.
Lemma zero_plus_alpha : forall alpha, ordinal alpha -> zero + alpha = alpha.
Proof.
intros.
pattern (plus zero).
apply plus_elim.
auto with schutte.
rewrite Greater_zero.
intros.
assert (H1:ordering_function (fun o => o) ordinal ordinal).
repeat split;auto with schutte.
eauto with schutte.
intros b Hb; exists b;auto.
generalize (ordering_function_unicity H0 H1).
destruct 1; auto.
Qed.
Lemma le_plus_l : forall alpha beta, ordinal alpha -> ordinal beta ->
alpha <= alpha + beta.
Proof.
intros; pattern alpha at 1.
rewrite <- alpha_plus_zero;auto.
pattern (plus alpha);apply plus_elim;auto.
intros;eapply ordering_function_mono_weak;eauto.
red;auto with schutte.
eauto with schutte.
Qed.
Lemma le_plus_r : forall alpha beta, ordinal alpha -> ordinal beta ->
beta <= alpha + beta.
Proof.
intros.
pattern (plus alpha).
apply plus_elim;auto.
intros; eapply ordering_le; eauto.
Qed.
Lemma plus_mono_r : forall alpha beta gamma,
ordinal alpha ->
beta < gamma ->
alpha + beta < alpha + gamma.
Proof.
intros.
pattern (plus alpha).
apply plus_elim;auto.
intros; eapply ordering_function_mono;eauto.
red;eauto with schutte.
red;eauto with schutte.
Qed.
Lemma ordinal_plus : forall alpha beta,
ordinal alpha ->
ordinal beta ->
ordinal (alpha + beta).
Proof.
intros.
pattern (plus alpha).
apply plus_elim; auto with schutte.
intros.
eapply ordering_function_ordinal_B;eauto.
Qed.
Hint Resolve ordinal_plus : schutte.
Lemma plus_mono_r_weak :forall alpha beta gamma,
ordinal alpha ->
ordinal beta ->
ordinal gamma ->
beta <= gamma ->
alpha + beta <= alpha + gamma.
Proof.
intros.
case (le_disj H2).
intros; subst gamma; auto with schutte.
right; apply plus_mono_r;auto.
Qed.
Lemma plus_reg_r : forall alpha beta gamma, ordinal alpha ->
ordinal beta ->
ordinal gamma ->
alpha + beta = alpha + gamma ->
beta = gamma.
Proof.
intros.
tricho beta gamma H3.
case (lt_irr (alpha+beta)).
pattern (alpha+beta) at 2; rewrite H2.
apply plus_mono_r;auto.
auto.
case (lt_irr (alpha+beta)).
pattern (alpha+beta) at 1; rewrite H2.
apply plus_mono_r;auto.
Qed.
Lemma plus_of_succ : forall a , ordinal a -> forall b, ordinal b ->
a + (succ b) = succ (a+b).
Proof.
intros.
pattern (plus a).
apply plus_elim.
auto.
intros plus_a Hp.
assert (plus_a b < plus_a (succ b)).
eapply ordering_function_mono;eauto.
red;auto with schutte.
apply lt_succ; auto.
generalize (lt_succ_le (plus_a b) (plus_a (succ b))).
intros.
assert (ordinal (plus_a b)).
case Hp.
intros.
decompose [and] H4.
apply H5.
apply H7;auto.
assert (ordinal (plus_a (succ b))).
eauto with schutte.
generalize (H2 H1).
intro.
case (le_disj H5).
auto.
intro.
case Hp;intros.
decompose [and] H8.
case (H10 (succ (plus_a b))).
red.
apply le_trans with (plus_a b).
generalize (H11 b H0).
unfold In.
unfold Greater.
auto.
right.
fold lt;apply lt_succ.
auto.
intros x (Hx,Ex).
clear H8.
absurd ( b < x /\ x < succ b).
red;intro.
decompose [and] H8;clear H8.
assert (succ b <= x).
apply lt_succ_le; eauto with schutte.
case (lt_irr (succ b)).
eapply le_lt_trans;eauto.
split.
eapply ordering_function_monoR;eauto.
rewrite Ex; auto with schutte.
rewrite <- Ex in H6.
eapply ordering_function_monoR;eauto.
red.
auto with schutte.
Qed.
Lemma alpha_plus_sup : forall alpha A , ordinal alpha -> Inhabited _ A ->
denumerable A ->
Included A ordinal ->
alpha + sup A = sup (image A (plus alpha)).
Proof.
intros.
generalize (normal_plus_alpha alpha H).
intro.
case H3.
destruct 2.
rewrite <- (H7 A H2 H0 H1).
auto.
Qed.
Lemma plus_limit : forall alpha beta, is_limit beta ->
ordinal alpha ->
alpha + beta =
|_| (image (members beta) (plus alpha)).
Proof.
intros.
generalize (is_limit_ordinal H); intro H1.
generalize (is_limit_sup_members H);intro e.
generalize (normal_plus_alpha alpha H0); intro H2.
pattern beta at 1;rewrite e.
case H2.
destruct 2.
rewrite <- H6;auto.
red;destruct 1;auto.
case H.
destruct 2.
exists zero.
red.
red.
split.
red;auto with schutte.
red.
generalize (le_zero _ H1).
intro H10; case (le_disj H10).
intro; subst beta; case H8;auto.
auto.
apply denumerable_members; auto.
Qed.
Lemma plus_FF : forall i j, F (i+j) = F i + F j.
induction i.
simpl.
intros;rewrite zero_plus_alpha;auto with schutte.
simpl.
induction j.
simpl.
rewrite alpha_plus_zero;auto with schutte.
rewrite <- (plus_n_O i).
auto.
rewrite IHi.
replace (F (S j)) with (succ (F j)).
2:simpl;auto.
rewrite plus_of_succ.
rewrite plus_of_succ.
rewrite <- IHi.
rewrite IHj.
auto.
auto with schutte.
auto with schutte.
auto with schutte.
auto with schutte.
Qed.
Lemma one_plus_omega : F 1 + omega = omega.
Proof.
rewrite plus_limit; auto with schutte.
2:apply is_limit_omega.
unfold omega at 2; apply le_antisym.
unfold omega_limit.
apply sup_mono;auto.
apply Ordering_Functions.R1 with ordinal (Greater (F 1)).
apply plus_ordering.
apply ordinal_finite.
apply denumerable_members;auto.
auto with schutte.
red. destruct 1. red in H0. eauto with schutte.
apply seq_range_denumerable; auto with schutte.
simpl; auto with schutte.
red.
destruct 1.
decompose [and] H.
subst x.
red.
apply ordinal_plus; auto with schutte.
case H0;auto.
red;destruct 1;auto with schutte.
red;subst x;auto with schutte.
intros x (a,(H1,H2)).
generalize H2;case H1; intros.
red in H0.
case (lt_omega_finite _ H0).
intros n e; exists (F (S n)).
subst x0.
split;auto with schutte.
exists (S n).
auto.
rewrite <- plus_FF in H3.
left.
split;auto.
subst x.
fold ordinal. red;apply ordinal_plus.
auto with schutte.
case H1;auto.
unfold omega_limit; apply sup_mono.
apply seq_range_denumerable; auto with schutte.
simpl; auto with schutte.
apply Ordering_Functions.R1 with ordinal (Greater (succ zero)).
apply plus_ordering. auto with schutte.
apply denumerable_members; auto with schutte.
red; destruct 1; red in H0; eauto with schutte.
red;destruct 1.
subst x; red;auto with schutte.
red.
destruct 1.
decompose [and] H.
red;subst x;apply ordinal_plus;auto with schutte.
case H0;auto.
intros x Hx;case Hx.
intros x0 H0;subst x.
exists (F (S x0));split;auto with schutte.
red;red.
exists (F x0).
split.
red.
split.
red;auto with schutte.
red.
apply finite_lt_omega.
rewrite <- plus_FF.
simpl;auto.
Qed.
Lemma minus_exists : forall alpha beta, alpha <= beta ->
exists gamma, ordinal gamma /\
alpha + gamma = beta.
Proof.
intros.
assert (ordinal alpha). eauto with schutte.
assert (ordinal beta).
eauto with schutte.
pattern (plus alpha).
apply plus_elim;auto.
intros.
case H2;intros.
decompose [and] H4; clear H4.
case (H6 _ H).
intros;exists x;auto.
Qed.
Section proof_of_associativity.
Variables alpha beta : OT.
Hypothesis O_alpha : ordinal alpha.
Hypothesis O_beta : ordinal beta.
Lemma plus_assoc1 : forall gamma,
ordinal gamma ->
alpha + beta <= alpha + (beta + gamma) .
Proof.
intros;apply plus_mono_r_weak;auto.
apply ordinal_plus;auto.
apply le_plus_l; auto.
Qed.
Lemma plus_assoc2 : forall gamma,
ordinal gamma ->
alpha + beta <= gamma ->
exists khi, ordinal khi /\ gamma = alpha + (beta + khi).
Proof.
intros.
assert (alpha <= gamma).
apply le_trans with (alpha + beta);auto.
apply le_plus_l; auto.
case (minus_exists H1).
intros z (Hz,Hz').
assert (beta <= z).
tricho beta z HH.
right;auto.
left;auto.
case (lt_irr gamma).
pattern gamma at 1; rewrite <- Hz'.
apply lt_le_trans with (alpha + beta).
apply plus_mono_r;auto.
auto.
case (minus_exists H2);intros u (Hu,Hu').
exists u;split;auto.
rewrite Hu';auto.
Qed.
Let f_alpha_beta := plus (alpha + beta).
Let g_alpha_beta gamma := alpha + (beta + gamma).
Remark of_g : ordering_function g_alpha_beta ordinal (Greater (alpha+beta)).
Proof.
repeat split.
red;auto.
eauto with schutte.
red; destruct 1.
decompose [and] H; subst x; auto with schutte.
eauto with schutte.
intros;red.
red.
unfold g_alpha_beta.
apply plus_assoc1.
auto.
intros.
red in H.
assert (ordinal b).
eauto with schutte.
case (plus_assoc2 H0 H).
intros x (Hx,H'x).
exists x.
unfold g_alpha_beta;split;auto.
unfold g_alpha_beta;intros.
apply plus_mono_r;auto with schutte.
apply plus_mono_r;auto with schutte.
Qed.
Lemma of_u : fun_eq_gen f_alpha_beta g_alpha_beta ordinal ordinal.
eapply ordering_function_unicity.
2:eexact of_g.
unfold f_alpha_beta.
apply plus_ordering.
apply ordinal_plus;auto.
Qed.
Lemma plus_assoc3 : forall gamma, ordinal gamma -> f_alpha_beta gamma =
g_alpha_beta gamma.
intros.
case of_u.
intros.
auto.
Qed.
Lemma plus_assoc' : forall gamma, ordinal gamma ->
alpha + (beta + gamma) = (alpha + beta) + gamma.
Proof.
intros; generalize plus_assoc3; unfold f_alpha_beta, g_alpha_beta.
intros;symmetry;auto.
Qed.
End proof_of_associativity.
Theorem plus_assoc : forall alpha beta gamma,
ordinal alpha ->
ordinal beta ->
ordinal gamma ->
alpha + (beta + gamma) = (alpha + beta) + gamma.
intros; apply plus_assoc'; auto.
Qed.
Lemma one_plus_ge_omega : forall alpha, omega <= alpha ->
F 1 + alpha = alpha.
Proof.
intros.
assert (ordinal alpha).
eauto with schutte.
generalize (minus_exists H).
intros (gamma, (Og,e)).
subst alpha.
rewrite plus_assoc;auto with schutte.
rewrite one_plus_omega.
trivial.
Qed.
Lemma finite_plus_ge_omega : forall n alpha, omega <= alpha ->
F n + alpha = alpha.
Proof.
induction n.
simpl. intros;rewrite zero_plus_alpha;trivial.
eauto with schutte.
intros; simpl.
replace (succ (F n)) with (F 1 + F n).
rewrite <- plus_assoc; eauto with schutte.
rewrite IHn;auto.
apply one_plus_ge_omega;eauto with schutte.
rewrite <- plus_FF.
simpl.
trivial.
Qed.
Lemma plus_mono_weak_l : forall alpha beta gamma,
ordinal gamma ->
alpha <= beta -> alpha + gamma <= beta + gamma.
Proof.
intros.
assert (ordinal alpha).
eauto with schutte.
assert (ordinal beta).
eauto with schutte.
case (minus_exists H0).
intros khi (Okhi,ekhi).
subst beta.
rewrite <- plus_assoc; eauto with schutte.
apply plus_mono_r_weak; eauto with schutte.
apply le_plus_r;eauto.
Qed.