Library gaia_hydras.T1Bridge

Bridge between Hydra-battle's and Gaia's T1 (Experimental)

This library introduces tools for making definitions and lemmas from Hydra battles's ordinals compatible with Gaia's ssete9 library.

From mathcomp Require Import all_ssreflect zify.

From Coq Require Import Logic.Eqdep_dec.
From hydras Require Import DecPreOrder ON_Generic T1 E0.
From gaia Require Export ssete9.
Set Implicit Arguments.

The name T1 denotes Gaia's data type. We use T1.T1 or hT1 for Hydra battles ordinal terms.

#[global] Notation hT1 := T1.T1.
#[global] Notation T1 := ssete9.CantorOrdinal.T1.

We rename Hydra battle's total order on hT1

Restrictions to terms in normal form

#[global] Notation LT := (restrict T1nf T1lt).
#[global] Notation LE := (restrict T1nf T1le).

Translation functions

Fixpoint h2g (a : hT1) : T1 :=
if a is T1.cons a n b then cons (h2g a) n (h2g b) else zero.

Fixpoint g2h (a : T1) : hT1 :=
if a is cons a n b then T1.cons (g2h a) n (g2h b) else T1.zero.

Lemma h2g_g2hK : cancel g2h h2g.

Lemma g2h_h2gK : cancel h2g g2h.

Lemma g2h_eqE (a b: T1): g2h a = g2h b ↔ a = b.

Lemma h2g_eqE (a b :hT1): h2g a = h2g b ↔ a = b.

Lemma g2h_diffE (a b : T1) : g2h a ≠ g2h b ↔ a ≠ b.

Lemma h2g_diffE (a b : hT1) : h2g a ≠ h2g b ↔ a ≠ b.

Pretty printing

Definition T1pp (a:T1) : ppT1 := pp (g2h a).

refinement of constants, functions, etc.

Definition refines0 (x:hT1)(y:T1) := y = h2g x.

Definition refines1 (f:hT1 → hT1) (f': T1 → T1) :=
  ∀ x: hT1, f' (h2g x) = h2g (f x).

Definition refines2 (f:hT1 → hT1 → hT1) (f': T1 → T1 → T1 ) :=
  ∀ x y : hT1, f' (h2g x) (h2g y) = h2g (f x y).

Definition refinesPred (hP: hT1 → Prop) (gP: T1 → Prop) :=
  ∀ x : hT1, hP x ↔ gP (h2g x).

Definition refinesRel (hR: hT1 → hT1 → Prop)
  (gR: T1 → T1 → Prop) :=
  ∀ x y : hT1, hR x y ↔ gR (h2g x) (h2g y).

Lemma refines1_R f f' :
  refines1 f f' ↔ ∀ y: T1, f (g2h y) = g2h (f' y).

Lemma refines2_R f f' :
  refines2 f f' ↔ ∀ y z: T1, f (g2h y) (g2h z) = g2h (f' y z).

Refinements of usual constants

Lemma zero_ref : refines0 T1.zero zero.

Lemma one_ref : refines0 T1.one one.

Lemma Finite_ref (n:nat) : refines0 (T1.T1nat n) (\F n).

Lemma omega_ref : refines0 T1.T1omega T1omega.

unary functions and predicates

Lemma succ_ref: refines1 T1.succ T1succ.
Lemma phi0_ref x: refines0 (T1.phi0 x) (phi0 (h2g x)).
Lemma g2h_phi0 a : g2h (phi0 a) = T1.phi0 (g2h a).

Lemma ap_ref : refinesPred Epsilon0.T1.ap T1ap.

Equality and comparison

Lemma T1eq_refl (a: T1) : T1eq a a.

Lemma T1eqE a b: T1eq a b → g2h a = g2h b.

Lemma T1eq_h2g (a b : hT1) : T1eq (h2g a) (h2g b) → a = b.

Lemma compare_ref (x y: hT1) :
  match T1.compare_T1 x y with
  | Datatypes.Lt ⇒ T1lt (h2g x) (h2g y)
  | Datatypes.Eq ⇒ h2g x = h2g y
  | Datatypes.Gt ⇒ T1lt (h2g y) (h2g x)
  end.

Lemma decide_hltE (a b : hT1):
  bool_decide (T1.lt a b) = (h2g a < h2g b ).

Lemma lt_ref : refinesRel T1.lt T1lt.

Lemma le_ref : refinesRel T1.le T1le.

Ordinal addition

Lemma plus_ref : refines2 T1.T1add T1add.

Ordinal multiplication

Section Proof_of_mult_ref.

  Lemma T1mul_a0E (c : T1) : c × zero = zero.

  Lemma T1mul_cons_cons_E n b n' b' :
    cons zero n b × cons zero n' b' =
      cons zero (n × n' + n + n') b'.

  Lemma T1mulE4 a n b n' b' :
    a != zero → (cons a n b) × (cons zero n' b') =
                   cons a (n × n' + n + n') b.

  Lemma multE4 a n b n' b' :
    a ≠ Epsilon0.T1.zero →
    Epsilon0.T1.T1mul (T1.cons a n b)
      (T1.cons Epsilon0.T1.zero n' b') =
      T1.cons a (n × n' + n + n') b.

  Lemma T1mulE5 a n b a' n' b' :
    a' != zero →
    (cons a n b) × (cons a' n' b') =
      cons (a + a') n' (T1mul (cons a n b) b').

  Lemma multE5 a n b a' n' b' :
    a' ≠ T1.zero →
    Epsilon0.T1.T1mul (T1.cons a n b) (T1.cons a' n' b') =
      T1.cons (T1.T1add a a') n' (T1.T1mul (T1.cons a n b) b').

  Lemma h2g_cons a n b : h2g (T1.cons a n b)= cons (h2g a) n (h2g b).

  Lemma g2h_cons a n b : g2h (cons a n b) = T1.cons (g2h a) n (g2h b).

  Lemma h2g_zero : h2g T1.zero = zero.

  Lemma g2h_zero : g2h zero = T1.zero.

  Lemma mult_ref0 : refines2 T1.T1mul T1mul.

End Proof_of_mult_ref.

Lemma mult_ref : refines2 T1.T1mul T1mul.

Lemma g2h_multE (a b : T1) : g2h (a × b) = T1.T1mul (g2h a) (g2h b).

Lemma g2h_plusE (a b: T1) : g2h (a + b) = T1.T1add (g2h a) (g2h b).

Ordinal terms in normal form

Lemma nf_ref (a: hT1) : T1.nf_b a = T1nf (h2g a).

Lemma LT_ref : refinesRel T1.LT LT.

Lemma LE_ref : refinesRel T1.LE LE.

Limits, successors, etc

Lemma T1limit_ref (a:Epsilon0.T1.T1) : T1.T1limit a = T1limit (h2g a).

Lemma T1is_succ_ref (a:Epsilon0.T1.T1): T1.T1is_succ a = T1is_succ (h2g a).

Lemma hnf_g2h a : T1.nf (g2h a) = T1nf a.

Lemma g2h_succ a : g2h (T1succ a) = T1.succ (g2h a).

Lemma hlt_iff a b: T1.lt a b ↔ h2g a < h2g b.

Lemma T1lt_iff a b: T1nf a → T1nf b →
a < b ↔ g2h a t1 < g2h b.

Lemma T1le_iff (a b: T1):
a ≤ b ↔ T1.le (g2h a) (g2h b).

Well formed ordinals as a data type

#[global] Notation hE0 := E0.E0.
#[global] Notation hcnf := E0.cnf.
#[global] Notation hE0lt := E0.E0lt.
#[global] Notation hE0le := E0.E0le.
#[global] Notation hE0zero := E0.E0zero.
#[global] Notation hE0omega := E0.E0_omega.
#[global] Notation hE0phi0 := E0.E0_phi0.
#[global] Notation hE0fin := E0.E0fin.
#[global] Notation hE0limit := E0.E0limit.
#[global] Notation hE0is_succ := E0.E0is_succ.

Record E0 := mkE0 { cnf : T1 ; _ : T1nf cnf == true}.
Coercion cnf : E0 >-> T1.

Canonical e0Sub := [subType for cnf].

Check fun (x:E0) ⇒ val x.

Remark omeganf : T1nf T1omega == true.

Check (Sub T1omega).

Check (Sub T1omega omeganf : e0Sub).

Check (Sub T1omega omeganf : E0).

Definition E0eqb (a b: E0):= cnf a == cnf b.

Lemma gE0_eq_intro a b : cnf a = cnf b → a = b.

Definition E0_eq_mixin : Equality.mixin_of E0.

Definition E0_eqtype := Equality.Pack E0_eq_mixin.
Canonical Structure E0_eqtype.

Definition ppE0 (a: E0) := T1pp (cnf a).

Definition E0lt (a b: E0) := cnf a < cnf b.
Definition E0le (a b: E0) := cnf a ≤ cnf b.

#[global, program] Definition E0zero: E0 := @mkE0 zero _.

#[global, program]
Definition E0_succ (a: E0): E0 := @mkE0 (T1succ (cnf a)) _.

#[global, program]
Definition E0_pred (a:E0) : E0:= @mkE0 (T1pred (cnf a)) _.

Fixpoint E0fin (n:nat) : E0 :=
  if n is p.+1 then E0_succ (E0fin p) else E0zero.

#[program] Definition E0_omega: E0 := @mkE0 T1omega _.

#[program] Definition E0_phi0 (a: E0) : E0 := @mkE0 (phi0 (cnf a)) _.

#[program] Definition E0plus (a beta: E0) : E0 :=
  @mkE0 (T1add (cnf a) (cnf beta)) _.

#[program] Definition E0mul (a beta: E0) : E0 :=
  @mkE0 (T1mul (cnf a) (cnf beta)) _.

Lemma E0fin_cnf (n:nat) : cnf (E0fin n) = \F n.

#[program] Definition E0_h2g (a: hE0): E0:= @mkE0 (h2g (E0.cnf a)) _.

#[program] Definition E0_g2h (a: E0): hE0 := @E0.mkord (g2h (cnf a)) _.

Definition E0limit a := hE0limit (E0_g2h a).

Definition E0is_succ a := hE0is_succ (E0_g2h a).

Lemma E0_h2g_nf (a:hE0) : T1nf (cnf (E0_h2g a)).

Lemma gE0lt_iff a beta : E0lt a beta ↔ E0_g2h a o < E0_g2h beta.

Lemma gE0le_iff a beta : E0le a beta ↔ E0_g2h a o ≤ E0_g2h beta.

Lemma E0_h2g_g2hK : cancel E0_g2h E0_h2g.

Lemma E0_g2h_h2gK : cancel E0_h2g E0_g2h.

Lemma g2h_E0_succ a : E0_g2h (E0_succ a)= E0.E0_succ (E0_g2h a).

Lemma E0is_succ_succ a : E0is_succ (E0_succ a).

Lemma E0is_succE a: E0is_succ a → {beta : E0 | a = E0_succ beta }.

Lemma E0_eqE (x y: E0) : x = y ↔ (E0_g2h x = E0_g2h y ).

Lemma E0_diffE (x y: E0) : x ≠ y ↔ (E0_g2h x ≠ E0_g2h y ).

Lemma E0_pred_succK x : E0_pred (E0_succ x) = x.

Lemma g2h_E0zero : E0_g2h E0zero = E0.E0zero.

Lemma E0g2h_Fin i: E0_g2h (E0fin i) = E0.E0fin i.

Lemma E0g2h_phi0 a : E0_g2h (E0_phi0 a) = E0.E0_phi0 (E0_g2h a).

Lemma E0g2h_mulE (a b: E0): E0_g2h (E0mul a b) = E0.E0mul (E0_g2h a) (E0_g2h b).

Lemma E0g2h_plusE (a b: E0): E0_g2h (E0plus a b)= E0.E0add (E0_g2h a) (E0_g2h b).

Lemma E0g2h_omegaE : E0_g2h E0_omega = hE0omega.

From Coq Require Import Relations Basics
     Wellfounded.Inverse_Image Wellfounded.Inclusion.

TODO: simplify this proof !!!

Lemma gE0lt_wf : well_founded E0lt.

Lemma L1' (a: T1) : T1omega × (a × T1omega) = T1omega × a × T1omega.

Sequences and limits

Definition g2h_seq (s: nat → T1) n := g2h (s n).
Definition h2g_seq (s: nat → hT1) n := h2g (s n).

Definition gstrict_lub (s : nat → T1) (lambda : T1) :=
  (∀ i : nat, LT (s i) lambda ) ∧
    (∀ a : T1, (∀ i : nat, LE (s i) a ) → LE lambda a ).

Lemma strict_lub_ref (s:nat → hT1) (lambda: hT1) :
  strict_lub s lambda ↔ gstrict_lub (h2g_seq s) (h2g lambda).

Search ( _ × ?beta = ?beta)%ca.

Search ( _ × ?beta = ?beta)%t1.

#[global] Instance T1compare : Compare T1:=
  fun a beta ⇒ compare (g2h a) (g2h beta).

Lemma compare_g2h (a beta : T1):
  compare (g2h a) (g2h beta) = compare a beta .

Lemma compare_h2g (a beta: hT1) :
   compare (h2g a) (h2g beta) =compare a beta .

Make E0 an ordinal notation

Lemma T1compare_correct (a b: T1):
  CompSpec eq T1lt a b (compare a b).

#[global] Instance E0compare: Compare E0 :=
  fun (alpha beta: E0) ⇒ T1compare (cnf alpha) (cnf beta).

Lemma E0compare_correct (alpha beta : E0) :
  CompSpec eq E0lt alpha beta (compare alpha beta).

#[global] Instance E0_sto : StrictOrder E0lt.

#[global] Instance E0_comp : Comparable E0lt compare.

#[global] Instance Epsilon0 : ON E0lt compare.

Locate T1omega.

Abstract properties of arithmetic functions (with SSreflect inequalities)

Definition strict_mono (f: nat → nat) :=
∀ n p, (n< p)%N → (f n < f p)%N.

Definition dominates_from (n : nat) (g f : nat → nat) :=
∀ p : nat, (n ≤ p)%N → (f p < g p)%N.

Definition dominates g f := ∃ n : nat , dominates_from n g f .

Definition dominates_strong g f := {n : nat | dominates_from n g f }.

Definition fun_le f g := ∀ n:nat, (f n ≤ g n)%N.