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.