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.