From Coq Require Import Arith ArithRing Lia.
From hydras Require Import Prelude.More_Arith Prelude.Merge_Sort
     Epsilon0.T1.

Set Implicit Arguments.


Fixpoint oplus (alpha beta : T1) : T1 :=
  let fix oplus_aux beta {struct beta} :=
      match alpha, beta with
        | zero, _ ⇒ beta
        | _, zero ⇒ alpha
        | cons a1 n1 b1, cons a2 n2 b2 ⇒
          match compare a1 a2 with
            | Gt ⇒ cons a1 n1 (oplus b1 beta)
            | Lt ⇒ cons a2 n2 (oplus_aux b2)
            | Eq ⇒ cons a1 (S (n1 + n2)%nat) (oplus b1 b2)
          end
      end
  in oplus_aux beta.

Infix "o+" := oplus (at level 50, left associativity).



Fixpoint o_finite_mult n alpha :=
match n with
    0 ⇒ T1.zero
  | S p ⇒ alpha o+ (o_finite_mult p alpha)
                 end.

Open Scope t1_scope.



Lemma oplus_0_r (alpha : T1) : alpha o+ zero = alpha.

Lemma oplus_0_l (beta : T1): zero o+ beta = beta.


Lemma oplus_compare_Lt:
  ∀ a n b a' n' b',
  compare a a' = Lt →
  cons a n b o+ cons a' n' b' = cons a' n' (cons a n b o+ b').

Lemma oplus_lt_rw :
  ∀ a n b a' n' b', T1.lt a a' →
                         cons a n b o+ cons a' n' b'=
                         cons a' n' (cons a n b o+ b').

Lemma oplus_eq_rw :
  ∀ a n b n' b',
    cons a n b o+ cons a n' b'=
    cons a (S (n+n')%nat) (b o+ b').

Lemma oplus_gt_rw :
  ∀ a n b a' n' b',
  T1.lt a' a →
    cons a n b o+ cons a' n' b' = cons a n (b o+ cons a' n' b').

Lemma oplus_compare_Gt :
  ∀ a n b a' n' b', compare a a' = Gt →
                         cons a n b o+ cons a' n' b' =
                         cons a n (b o+ cons a' n' b').


Lemma oplus_eqn :
  ∀ a b,
    a o+ b =
    match a, b with
        T1.zero, _ ⇒ b
      | _, T1.zero ⇒ a
      | cons a1 n1 b1, cons a2 n2 b2 ⇒
        match compare a1 a2 with
            Gt ⇒ cons a1 n1 (b1 o+ b)
          | Eq ⇒ cons a1 (S (n1 + n2)) (b1 o+ b2)
          | Lt ⇒ cons a2 n2 (a o+ b2)
        end
    end.

Lemma oplus_cons_cons :
  ∀ a n b a' n' b',
    (cons a n b) o+ (cons a' n' b') =
    match compare a a' with
          | Gt ⇒ cons a n (b o+ (cons a' n' b') )
          | Eq ⇒ cons a (S (n + n')%nat) (b o+ b')
          | Lt ⇒ cons a' n' (cons a n b o+ b')
    end.

Lemma lt_a_phi0_b_oplus : ∀ gamma alpha beta,
                        alpha <_phi0 gamma →
                        beta <_phi0 gamma →
                        alpha o+ beta <_phi0 gamma.

Lemma oplus_bounded_phi0 alpha beta gamma :
  nf alpha → nf beta → nf gamma →
  lt alpha (phi0 gamma) →
  lt beta (phi0 gamma) →
  lt (alpha o+ beta) (phi0 gamma).

Section Proof_of_plus_nf.

  Lemma oplus_nf_0 (gamma : T1):
    nf gamma → ∀ alpha beta, nf alpha → nf beta →
                               T1.lt alpha gamma →
                               T1.lt beta gamma →
                               nf (alpha o+ beta).

  Lemma oplus_nf (alpha beta : T1) :
      nf alpha → nf beta → nf (alpha o+ beta).

End Proof_of_plus_nf.

Lemma o_finite_mult_nf : ∀ a n, nf a → nf (o_finite_mult n a).

Section Proof_of_oplus_comm.
  Lemma oplus_comm_0 (gamma: T1):
    nf gamma →
    ∀ alpha beta, nf alpha → nf beta →
                        T1.lt alpha gamma →
                        T1.lt beta gamma →
                        alpha o+ beta = beta o+ alpha.

  Lemma oplus_comm (alpha beta: T1):
   nf alpha → nf beta → alpha o+ beta = beta o+ alpha.

End Proof_of_oplus_comm.

Lemma oplus_lt_rw2 : ∀ a n b x, nf (cons a n b) → nf x →
                                     x <_phi0 a →
                                     cons a n b o+ x =
                                     cons a n (b o+ x).

Section Proof_of_oplus_assoc.

  Ltac ass_rw Hrec alpha a b c :=
    match goal with |- context Gamma [oplus ?a (oplus ?b ?c)] ⇒
                    erewrite Hrec with alpha a b c end.

  Ltac ass_rw_rev Hrec alpha a b c :=
    match goal with |- context Gamma [oplus (oplus ?a ?b) ?c] ⇒
                          erewrite <- Hrec with alpha a b c end.
  Lemma oplus_assoc_0 (alpha: T1):
      nf alpha →
      ∀ a b c, nf a → nf b → nf c →
                      T1.lt a alpha →
                      T1.lt b alpha → T1.lt c alpha →
                      a o+ (b o+ c) = (a o+ b) o+ c.

  Lemma oplus_assoc (alpha beta gamma:T1) :
    nf alpha → nf beta → nf gamma →
    alpha o+ (beta o+ gamma) =
    alpha o+ beta o+ gamma.

End Proof_of_oplus_assoc.

Section Proof_of_oplus_lt1.
  Variables a1 a2: T1.
  Variable n : nat.
  Hypothesis H0 : nf (cons a1 n a2).

  Lemma oplus_lt_0 : ∀ b, nf b → T1.lt b (b o+ (cons a1 n a2)).

End Proof_of_oplus_lt1.

Lemma oplus_lt1 : ∀ a b, nf a → nf b → T1.lt T1.zero a →
                              T1.lt b (b o+ a).

Lemma oplus_lt2 : ∀ a b, nf a → nf b → T1.lt T1.zero b →
                              T1.lt a (b o+ a).

Lemma oplus_le1 : ∀ a b, nf a → nf b → leq lt a (a o+ b).

Lemma oplus_le2 : ∀ a b, nf a → nf b → leq lt b (a o+ b).

Lemma oplus_strict_mono_0 :
  ∀ alpha, nf alpha →
                ∀ a (Ha:nf a) b (Hb: nf b) c (Hc : nf c),
                  lt a alpha → lt c alpha → lt b c →
                  lt (a o+ b) (a o+ c).

Lemma oplus_strict_mono_r : ∀ a b c, nf a → nf b → nf c →
                                          lt b c → lt (a o+ b) (a o+ c).

Lemma oplus_strict_mono_l : ∀ a b c, nf a → nf b → nf c →
                                          T1.lt a b →
                                          T1.lt (a o+ c) (b o+ c).


Lemma oplus_strict_mono_LT_l (alpha beta gamma : T1) :
  nf gamma → alpha t1< beta →
  alpha o+ gamma t1< beta o+ gamma.
Lemma oplus_strict_mono_LT_r (alpha beta gamma : T1) :
  nf alpha → beta t1< gamma →
  alpha o+ beta t1< alpha o+ gamma.
Lemma oplus_strict_mono_bi : ∀ a b c d ,
    nf a → nf b → nf c → nf d →
    T1.lt a b → T1.lt c d → T1.lt (a o+ c) (b o+ d).

Lemma oplus_of_phi0_0 : ∀ a b,
                          phi0 a o+ phi0 b =
                          match compare (phi0 a) (phi0 b)
                          with Lt ⇒ cons b 0 (cons a 0 T1.zero)
                            | Eq ⇒ cons a 1 T1.zero
                            | Gt ⇒ cons a 0 (cons b 0 T1.zero)
                          end.

Lemma oplus_of_phi0 : ∀ a b,
                        phi0 a o+ phi0 b =
                        match compare a b
                        with Lt ⇒ cons b 0 (cons a 0 T1.zero)
                          | Eq ⇒ cons a 1 T1.zero
                          | Gt ⇒ cons a 0 (cons b 0 T1.zero)
                        end.

Lemma o_finite_mult_rw : ∀ a n, o_finite_mult (S n) (phi0 a) =
                                     cons a n T1.zero.

Lemma o_finite_mult_lt_phi0_1 : ∀ a b n,
                                  T1.lt a b →
                                  T1.lt (o_finite_mult n (phi0 a)) (phi0 b).

Lemma o_finite_mult_mono : ∀ a b n, nf a → nf b → T1.lt a b →
                                          T1.lt (o_finite_mult (S n) a)
                                             (o_finite_mult (S n) b).

Lemma oplus_lt_phi0 : ∀ a b c, nf a → nf b → nf c →
                                     T1.lt a c → T1.lt b c →
                                     T1.lt (phi0 a o+ phi0 b) (phi0 c).