Library gaia_hydras.GHessenberg

From mathcomp Require Import all_ssreflect zify.
From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic.
From hydras Require Import T1 E0 Hessenberg.

From gaia Require Export ssete9.
From gaia_hydras Require Import T1Bridge.

Set Implicit Arguments.

Open Scope cantor_scope.

#[local] Notation hoplus := Epsilon0.Hessenberg.oplus.

Definition oplus alpha beta := h2g (hoplus (g2h alpha) (g2h beta)).

Infix "o+" := oplus: cantor_scope.

Fixpoint o_finite_mult n alpha :=
  if n is p.+1 then alpha o+ (o_finite_mult p alpha)
  else zero.



Module FixpointDef.
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.
End FixpointDef.

Lemma oplusE (a b :T1) :
  a o+ b =
    match a, b with
    | zero, _ ⇒ b
    | _, 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 oplus0b: left_id zero oplus.

Lemma oplusa0: right_id zero oplus.

Lemma oplus_nf (a b : T1) : T1nf a → T1nf b → T1nf (a o+ b).

Lemma oplusC (a b: T1): T1nf a → T1nf b → a o+ b = b o+ a.

Lemma oplusA (a b c: T1) :
  T1nf a → T1nf b → T1nf c → a o+ (b o+ c) = a o+ b o+ c.

Lemma oplus_lt1 (a b:T1):
  T1nf a → T1nf b → zero < a → b < b o+ a.


Lemma oplus_lt2 (a b: T1):
  T1nf a → T1nf b → zero < b → a < b o+ a.

Lemma oplus_strict_mono_l (a b c: T1):
  T1nf a → T1nf b → T1nf c → a < b → a o+ c < b o+ c.

Lemma oplus_strict_mono_r (a b c: T1):
  T1nf a → T1nf b → T1nf c → b < c → a o+ b < a o+ c.

Lemma oplus_lt_phi0 (a b c: T1):
  T1nf a → T1nf b → T1nf c →
  a < c → b < c → phi0 a o+ phi0 b < phi0 c.