Library epsilon0.E0_ARITH

Require Import Arith.
Require Import Omega.
Require Import Compare_dec.
Add LoadPath "../prelude".
Require Import More_nat.
Add LoadPath "../rpo".
Require Import EPSILON0.
Require Import ArithRing.
Require Import Tools.

Lemma plus_assoc0 : forall a, nf a ->
             forall c1, c1 < phi0 a ->
    nf c1 -> forall c2, c2 < phi0 a ->nf c2 ->
                              forall c3, c3 < phi0 a -> nf c3 ->
                                         c1 + (c2 + c3) =
                                         (c1 + c2) + c3.
 intros a Ha;pattern a.
 apply EPSILON0.transfinite_induction.
 2:assumption.
 intros x Cx Hx.
 destruct c1.
 intros;simpl;auto.
 destruct c2.
 intros;simpl (plus_zero c3);rewrite plus_a_zero;auto.
 destruct c3.
 intros; repeat rewrite plus_a_zero;trivial.
 apply plus_nf;auto.
 intros.

 case (trichotomy_inf c1_1 c2_1).
 destruct 1.
 rewrite (plus_cons_cons_rw1 n c1_2 n0 c2_2 l).
 case (trichotomy_inf c2_1 c3_1).
 destruct 1.
 repeat rewrite plus_cons_cons_rw1;auto.
 eapply lt_trans;eauto.
 subst c3_1.
  repeat rewrite plus_cons_cons_rw2;auto.
 rewrite plus_cons_cons_rw1;auto.
 intro.
 repeat (rewrite (plus_cons_cons_rw3 l0 H2 H4);auto).
 rewrite plus_cons_cons_rw1;auto.
 subst c2_1.
 repeat rewrite plus_cons_cons_rw2;auto.
 case (trichotomy_inf c1_1 c3_1).
 destruct 1.
  repeat (rewrite plus_cons_cons_rw1;auto).
 subst c3_1.
 repeat rewrite plus_cons_cons_rw2;auto.
 assert ((S (n + S (n0 + n1))) = (S (S (n + n0) + n1))).
 omega.
 rewrite H5;auto.
 eapply nf_coeff_irrelevance;eauto.
  eapply nf_coeff_irrelevance;eauto.
 intro.
 repeat rewrite (plus_cons_cons_rw3 l H2 H4);auto.
 rewrite plus_cons_cons_rw2.
 assert (nf (cons c1_1 (S (n + n0)) c2_2)).
 eapply nf_coeff_irrelevance;eauto.
 rewrite (plus_cons_cons_rw3 l H5 H4).
 auto.
 auto.
 replace (cons c1_1 n0 (plus c2_2 (cons c3_1 n1 c3_2)))
 with (plus (cons c1_1 n0 c2_2) (cons c3_1 n1 c3_2)).
 apply plus_nf;auto.
 rewrite plus_cons_cons_rw3.
 auto.
 auto.
 auto.
 auto.
 intro.
 case (trichotomy_inf c3_1 c1_1).
 destruct 1.
 case_eq ( (plus (cons c2_1 n0 c2_2) (cons c3_1 n1 c3_2))).
 intro e'.
 case (plus_is_zero H2 H4 e').
 discriminate 1.
 intros.
 assert (lt t c1_1).
 generalize H5;simpl.
 case c2_1.
 case c3_1.
 injection 1.
 intros.
 subst t.
 Admitted.

Lemma plus_assoc :
             forall a,
    nf a -> forall b, nf b ->
                              forall c, nf c ->
                                         a + (b + c) = (a + b) + c.
Proof.
 intros c1 H c2 HO c3 H1.

 apply plus_assoc0 with (a:= succ (max (log c1) (max (log c2)
                                                               (log c3))));
 auto.
 apply succ_nf.
 case (max_dec (log c1) (max (log c2) (log c3))).
 intro e;rewrite e.
 apply log_nf;auto.
 intros;
 case (max_dec (log c2) (log c3)).
 rewrite e.
 intro e';rewrite e'.
 apply log_nf;auto.
 intro e';rewrite e'.
 case (max_dec (log c1) (log c3)).
 intro e1;rewrite e1.
 apply log_nf;auto.
 intro e1;rewrite e1;apply log_nf;auto.
 eapply lt_le_trans with (phi0 (succ (log c1))).
 apply phi0_log.
 apply le_phi0_phi0.
 apply le_succ_succ.
 apply log_nf;auto.
 repeat apply max_nf;apply log_nf;auto.
 apply max_le_1.

 apply lt_le_trans with (phi0 (succ (log c2))).
 apply phi0_log.
  apply le_phi0_phi0.
 apply le_succ_succ.
 apply log_nf;auto.
 repeat apply max_nf;apply log_nf;auto.
 rewrite max_comm.
 rewrite max_assoc.
 apply max_le_1.

  apply lt_le_trans with (phi0 (succ (log c3))).
  apply phi0_log.
  apply le_phi0_phi0.
  apply le_succ_succ.
 apply log_nf;auto.
 repeat apply max_nf;apply log_nf ;auto.
 rewrite <- max_assoc.
 rewrite max_comm.
  apply max_le_1.
Qed.

Set Implicit Arguments.
Lemma pred_nf : forall a b, nf a -> pred a = Some b -> nf b.
Admitted.

Lemma pred_of_succ : forall a, nf a -> pred (succ a) = Some a.
Admitted.

Lemma pred_defined : forall c c', pred c = Some c' -> c' = succ c.
Admitted.

Lemma c_no_pred : forall c, nf c -> pred c = None ->
                                      forall c', nf c' -> succ c' <> c.
Admitted.

Lemma minus_nf : forall c c', nf c -> nf c' -> nf (EPSILON0.minus c c').
Admitted.

Lemma mult_nf : forall c c', nf c -> nf c' -> nf (mult c c').
Admitted.

Lemma exp_nf : forall c c', nf c -> nf c' -> nf (exp c c').
Admitted.