Library gaia_hydras.nfwfgaia

Copy of gaia's ssete9.v (for experimenting Alectryon documentation) Changes from original proof script are signaled as additions/changes or inside Alectryon snippets

Ordinals in Pure Coq

From mathcomp
Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
From mathcomp Require Import fintype bigop.

Set Implicit Arguments.

prelude

Useful lemmas missing in ssreflect

Lemma if_simpl (p: bool): (if p then true else false ) = p.

Lemma ltn_simpl1 n n': ((n' + n).+1 < n ) = false.

Lemma eqn_simpl1 n n': ((n' + n).+1 == n ) = false.

Lemma ltn_simpl2 n n' n'':
(n × n' + n + n' < n × n'' + n + n'') = (n' < n'').

Lemma eqn_simpl2 n n' n'':
(n × n' + n + n' == n × n'' + n + n'') = (n' == n'').

Lemma ltn_add_le m1 m2 n1 n2: m1 < n1 → m2 ≤ n2 → m1 + m2 < n1 + n2.

Lemma ltn_add_el m1 m2 n1 n2: m1 ≤ n1 → m2 < n2 → m1 + m2 < n1 + n2.

Lemma ltn_add_ll m1 m2 n1 n2: m1 < n1 → m2 < n2 → m1 + m2 < n1 + n2.

The ssreflect comparison on nat is WF

Lemma lt_wf: well_founded (fun (a b:nat) ⇒ a < b).

Example 1

An example of function defined by transfinite induction using Fix

Module Wf_ex.

Definition f_spec f n :=
   if n is m.+2 then (f (f m.+1).+1 ).+1 else 0.

Lemma f_spec_simp f n: (∀ n, f n = f_spec f n ) → f n = n.-1.

Lemma f0 n p: p ≤ n → p.+2 ≤ n.+2.

Definition f1 :
  ∀ x, (∀ z, z < x → {y :nat |y ≤ z.-1}) →
  {y :nat | y ≤ x.-1}.

Definition f2 := Fix lt_wf _ f1.
Definition f (x:nat): nat := sval (f2 x).

Lemma f_eqn x: f2 x = f1 (fun y _ ⇒ f2 y).

Lemma f_correct n: f n = f_spec f n.

End Wf_ex.

Example 2

Second example, f(n) = 1 + \sum_{(i < n)} f(i)

Module Wfsum.

Definition psum (f: nat → nat) n := \sum_(i< n) (f i).
Definition f_spec f:= ∀ n, f n = (psum f n).+1.

Lemma f_spec_simp f n: f_spec f → f n = 2 ^ n.

Lemma psum_exten n f g :
   (∀ k, k < n → f k = g k ) → (psum f n).+1 = (psum g n).+1.

Lemma lt_dec n m: {n <m } + {~~ (n < m ) }.

Definition extension (n : nat) (p : ∀ k : nat, k < n → nat) k :=
  match lt_dec k n with
    | left x ⇒ p k x
    | _ ⇒ 0 end.

Definition f1 (n : nat) (h : ∀ z : nat, z < n → nat) :=
    (psum (extension h) n).+1.

Definition f2 := Fix lt_wf _ f1.

Lemma f_eqn x: f2 x = f1 (n:=x) (fun y _ ⇒ f2 y).

Definition f (x:nat): nat := f2 x.

Lemma f_correct: f_spec f.

End Wfsum.

Example 3

We consider here only even numbers, show that comparison is WF, define a function by transfinite induction and show it is correct.

Module Wf_ex3.

Definition lte n m := [&& ~~ odd n , ~~ odd m & n < m ].

Lemma lte_wf: well_founded lte.

Definition f_spec f n :=
   if n is m.+4 then (f (f (m.+2)).*2.+2 ).+1 else 0.

Lemma f_spec_simp f n: ~~ odd n → (∀ n, ~~odd n → f n = f_spec f n )
   → f n = (n.-1)./2.

Lemma f_spec_simp1 f n: (∀ n, ~~odd n → f n = f_spec f n )
   → f (n.*2.+2) = n.

Lemma f_spec_simp2 f n: (∀ n, f n = f_spec f n ) → f(n.*2.+3) = n.

Lemma f0a y n: odd n = false → odd n.+2 ∨ y ≤ (n.+2)./2.-1 →
   y ≤ n./2 ∧ lte (y.*2).+2 n.+4.

Lemma f0b a b: odd a.*2.+2 ∨ b ≤ (a.*2.+2)./2.-1 → b ≤ a.

Lemma f0c n: odd n = false → lte n.+2 n.+4.

Lemma odd_dec n : {odd n } + {odd n = false }.

Definition f1 :
  ∀ x, (∀ z, lte z x → {y :nat | odd z ∨ y ≤ (z./2).-1}) →
  {y :nat | odd x ∨ y ≤ (x./2).-1}.

Definition f2 := Fix lte_wf _ f1.
Definition f (x:nat): nat := sval (f2 x).

Lemma f_eqn x: f2 x = f1 (fun y _ ⇒ f2 y).

Lemma f_correct n: ~~odd n → f n = f_spec f n.

End Wf_ex3.

More on accessiblity

We show that there is no striclty decreasing function with domain nat

Section Sequences.

Variable A : Set.
Variable R : A → A → Prop.

Lemma acc_rec a b: R a b → Acc R b → Acc R a.

Hypothesis W : well_founded R.

Theorem not_decreasing :
¬ (∃ f : nat → A , (∀ i:nat, R (f i.+1) (f i))).

End Sequences.

We show here an induction principle; we could use it for ordinals in NF form.

Section restricted_recursion.

Variables (A:Type)(P:A →Prop)(R:A →A →Prop).

Definition restrict a b := [/\ P a , R a b & P b ].

Definition well_founded_P := ∀ a, P a → Acc restrict a.

Lemma P_well_founded_induction_type :
       well_founded_P →
       ∀ Q : A → Type,
       (∀ x : A, P x → (∀ y : A, P y → R y x → Q y ) → Q x ) →
       ∀ a : A, P a → Q a.
End restricted_recursion.
Module CantorOrdinal.

The type T1

This type represents all ordinals less that ε ₀ , via the Cantor Normal Form. More exactly cons a n b represents ω ^A * (n.+1) + B if a represents A and b represents B.

Inductive T1 : Set :=
zero : T1
| cons : T1 → nat → T1 → T1.

Equality

we define a boolean equality, the use the mechanism of canonical structures provided by ssreflect

Fixpoint T1eq x y {struct x} :=
  match x, y with
  | zero, zero ⇒ true
  | cons a n b, cons a' n' b' ⇒ [&& T1eq a a', n== n' & T1eq b b' ]
  | _, _ ⇒ false
end.

Lemma T1eqP : Equality.axiom T1eq.

Canonical T1_eqMixin := EqMixin T1eqP.
Canonical T1_eqType := Eval hnf in EqType T1 T1_eqMixin.

Arguments T1eqP {x y}.

Lemma T1eqE a n b a' n' b':
  (cons a n b == cons a' n' b') = [&& a == a', n== n' & b == b' ].

Declare Scope cantor_scope.
Delimit Scope cantor_scope with ca.
Open Scope cantor_scope.

Some definitions

φ₀(x) is cons x 0 zero , it represents ω ^x
one is φ₀(0)
omega is φ₀(1)
bad is an example of an ordinal not in normal form
fun n := \F n is the canonical injection of nat into T1
the log of cons a n b is a
an ordinal is AP if it is in the image of φ₀.

Definition phi0 a := cons a 0 zero.
Definition one := cons zero 0 zero.
Definition T1omega := phi0 (phi0 zero).
Definition T1bad := cons zero 0 T1omega.
Definition T1nat (n:nat) : T1 :=
if n is p.+1 then cons zero p zero else zero.
Definition T1log a := if a is cons a _ _ then a else zero.
Definition T1ap x := if x is cons a n b then ((n==0) && (b==zero )) else false.

Notation "\F n" := (T1nat n)(at level 29) : cantor_scope.

Lemma T1F_inj: injective T1nat.

Lemma T1phi0_zero : phi0 zero = \F 1.
Lemma T1phi0_zero' : phi0 zero = one.
Lemma T1log_phi0 x : T1log (phi0 x) = x.
Lemma T1ap_phi0 x: T1ap (phi0 x).

Order on T1

We give here a recursion definition of comparison. Essentially, φ₀(x) is strictly increasing,

Fixpoint T1lt x y {struct x} :=
  if x is cons a n b then
    if y is cons a' n' b' then
      if a < a' then true
      else if a == a' then
         if (n < n')%N then true
         else if (n == n') then b < b' else false
         else false
      else false
  else if y is cons a' n' b' then true else false
where "x < y" := (T1lt x y) : cantor_scope.

Definition T1le (x y :T1) := (x == y ) || (x < y ).
Notation "x <= y" := (T1le x y) : cantor_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : cantor_scope.
Notation "x > y" := (y < x) (only parsing) : cantor_scope.

Lemma T1lenn x: x ≤ x.

#[local] Hint Resolve T1lenn : core.

Lemma T1ltnn x: (x < x ) = false.

Lemma T1lt_ne a b : a < b → (a == b ) = false.

Lemma T1lt_ne' a b : a < b → (b == a ) = false.

Lemma T1ltW a b : (a < b ) → (a ≤ b ).

Lemma T1le_eqVlt a b : (a ≤ b ) = (a == b ) || (a < b ).

Lemma T1lt_neAle a b : (a < b ) = (a != b ) && (a ≤ b ).

Lemma T1ltn0 x: (x < zero ) = false.
Lemma T1le0n x: zero ≤ x.
Lemma T1len0 x: (x ≤ zero ) = (x == zero ).
Lemma T1lt0n x: (zero < x ) = (x != zero ).

Lemma T1ge1 x: (one ≤ x ) = (x != zero ).

Lemma T1lt1 x: (x < one ) = (x==zero ).

Lemma T1nat_inc n p : (n < p)%N = (\F n < \F p ).

This is an alternative version of less-or-equal

Lemma T1le_consE a n b a' n' b':
(cons a n b ≤ cons a' n' b') =
    if a < a' then true
      else if a == a' then
         if (n < n')%N then true
         else if (n == n') then b ≤ b' else false
         else false.

We have exactly one of: a is less than, greater than, or equal to b

Lemma T1lt_trichotomy a b: [|| (a < b ), (a==b ) | (b < a )].

Lemma T1lt_anti b a: a < b → (b < a ) = false.

Lemma T1leNgt a b: (a ≤ b ) = ~~ (b < a ).

Lemma T1ltNge a b: (a < b ) = ~~ (b ≤ a ).

Lemma T1eq_le m n : (m == n ) = ((m ≤ n ) && (n ≤ m )).

Lemma T1le_total m n : (m ≤ n ) || (n ≤ m ).

The next three definitions are similar to to those defined in ssrnat. we shall use T1ltgtP a lot.

CoInductive T1ltn_xor_geq m n : bool → bool → Set :=
  | T1LtnNotGeq of m < n : T1ltn_xor_geq m n false true
  | T1GeqNotLtn of n ≤ m : T1ltn_xor_geq m n true false.

CoInductive T1leq_xor_gtn m n : bool → bool → Set :=
  | T1GeqNotGtn of m ≤ n : T1leq_xor_gtn m n true false
  | T1GtnNotLeq of n < m : T1leq_xor_gtn m n false true.

CoInductive compare_T1 m n : bool → bool → bool → Set :=
  | CompareT1Lt of m < n : compare_T1 m n true false false
  | CompareT1Gt of m > n : compare_T1 m n false true false
  | CompareT1Eq of m = n : compare_T1 m n false false true.

Lemma T1leP x y : T1leq_xor_gtn x y (x ≤ y) (y < x).

Lemma T1ltP m n : T1ltn_xor_geq m n (n ≤ m) (m < n).

Lemma T1ltgtP m n : compare_T1 m n (m < n) (n < m) (m == n).

We show here transitivity of comparison, using T1ltgtP .

Lemma T1lt_trans b a c: a < b → b < c → a < c.

Lemma T1lt_le_trans b a c: a < b → b ≤ c → a < c.

Lemma T1le_lt_trans b a c: a ≤ b → b < c → a < c.

Lemma T1le_trans b a c: a ≤ b → b ≤ c → a ≤ c.

The following lemma implies x < ω ^x, so all ordinals are less than ε ₀

Lemma head_lt_cons a n b: a < cons a n b.

Lemma T1lt_cons_le a n b a' n' b': (cons a n b < cons a' n' b') → (a ≤ a').

Lemma T1le_cons_le a n b a' n' b': (cons a n b ≤ cons a' n' b') → (a ≤ a').

Lemma phi0_lt a b: (phi0 a < phi0 b ) = (a < b ).

Lemma phi0_le a b: (phi0 a ≤ phi0 b ) = (a ≤ b ).

Lemma phi0_lt1 a n b a': (cons a n b < phi0 a') = (a < a').

Normal form

There exists a strictly infinite decreasing sequence of ordinals, so the order is not well founded

Theorem lt_not_wf : ¬ (well_founded T1lt ).

We say that cons a n b is NF if )b <φ₀(a). If b is cons a' n' b', this says that b is less than b'. If a is zero, this says that b=0.

Fixpoint T1nf x :=
if x is cons a _ b then [&& T1nf a, T1nf b & b < phi0 a ]
else true.

Lemma T1nf_cons0 a n: T1nf a → T1nf (cons a n zero).

Lemma T1nf_cons_cons a n a' n' b' : T1nf (cons a n (cons a' n' b')) → a' < a.

Lemma T1nf_consa a n b: T1nf (cons a n b) → T1nf a.

Lemma T1nf_consb a n b: T1nf (cons a n b) → T1nf b.

Lemma T1nf_finite1 n b: T1nf (cons zero n b) = (b == zero ).

Lemma T1nf_finite n b: T1nf (cons zero n b) → (b = zero ).

Lemma T1nfCE: ~~(T1nf T1bad ).

We show here that the restriction of T1lt to NF ordinals is well-founded, then prove two induction principles. Note that nf_Wf' says every NF x is accessible by the relation: u<v, u and v NF. If x is not NF it is trivially accessible. The proof is a bit tricky

Section AddLocalNotation.
  #[local] Notation LT :=
    (@restrict T1 (fun x : T1 ⇒ is_true (T1nf x))
               (fun x y : T1 ⇒ is_true (x < y))).

  Lemma nf_Wf : well_founded (restrict T1nf T1lt).
  Lemma nf_Wf' : well_founded_P T1nf T1lt.

  Lemma T1transfinite_induction P:
    (∀ x, T1nf x → (∀ y, T1nf y → y < x → P y ) → P x ) →
    ∀ a, T1nf a → P a.

  Lemma T1transfinite_induction_Q (P: T1 → Type) (Q: T1 → Prop):
    (∀ x:T1, Q x → T1nf x →
                  (∀ y:T1, Q y → T1nf y → y < x → P y ) → P x ) →
    ∀ a, T1nf a → Q a → P a.

  Lemma T1nf_rect (P : T1 → Type):
    P zero →
    (∀ n: nat, P (cons zero n zero)) →
    (∀ a n b n' b', T1nf (cons a n b) →
                         P (cons a n b) →
                         b' < phi0 (cons a n b) →
                         T1nf b' →
                         P b' →
                         P (cons (cons a n b) n' b')) →
    ∀ a, T1nf a → P a.

End AddLocalNotation.

Successor

We say that cons a n b is

limit if a is non-zero, b is limit or zero
finite if a is zero
a successor if a is zero or b is a successor

and define its

successor as \F (n+2) or cons a n (succ b)
predecessor as \F n or cons a n (pred b)
split u,v as cons a n x, y if b split as x,y and a is non-zero; and as 0,n+1 if a is zero

Note that if a=0, the quantity b is ignored; but when x is NF, then b is zero.

Fixpoint T1limit x :=
  if x is cons a n b then
    if a==zero then false else (b== zero ) || T1limit b
  else false.

Definition T1finite x := if x is cons a n b then a == zero else true.

Fixpoint T1is_succ x :=
  if x is cons a n b then (a==zero ) || T1is_succ b else false.

Fixpoint T1succ (c:T1) : T1 :=
  if c is cons a n b
  then if a == zero then cons zero n.+1 zero else cons a n (T1succ b)
  else one.

Fixpoint T1pred (c:T1) : T1 :=
  if c is cons a n b then
    if (a==zero ) then \F n else (cons a n (T1pred b))
  else zero.

Fixpoint T1split x:=
  if x is cons a n b then
    if a==zero then (zero , n.+1) else
      let: (x, y) := T1split b in (cons a n x ,y)
  else (zero ,0).

Lemma split_limit x: ((T1split x ).2 == 0) = ((x==zero ) || T1limit x ).

Lemma split_is_succ x: ((T1split x ).2 != 0) = (T1is_succ x ).

Lemma split_finite x: ((T1split x ).1 == zero ) = T1finite x.

Lemma split_succ x: let:(y,n):= T1split x in T1split (T1succ x) = (y,n.+1).

Lemma split_pred x: let:(y,n):= T1split x in T1split (T1pred x) = (y,n.-1).

Lemma split_le x : (T1split x ).1 ≤ x.

Lemma nf_split x : T1nf x → T1nf (T1split x ).1.

Lemma T1finite1 n: T1finite (\F n).

Lemma T1finite2 x: T1finite x → T1nf x → x = \F ((T1split x ).2 ).

Lemma T1finite2CE: T1finite T1bad ∧ ∀ n, T1bad ≠ \F n.

Lemma T1finite_succ x: T1finite x → T1finite (T1succ x).

Lemma T1succ_nat n: T1succ (\F n) = \F (n.+1).

Lemma nf_omega : T1nf T1omega.
Lemma nf_finite n: T1nf (\F n).
Lemma nf_phi0 a: T1nf (phi0 a) = T1nf a.
Lemma nf_log a: T1nf a → T1nf (T1log a).

An ordinal is zero, limit or a successor, exclusively. When we split x the first component is zero or limit, the second is a natural number

Lemma limit_pr1 x: (x == zero ) (+) (T1limit x (+) T1is_succ x ).

Lemma split_limit1 x (y:= (T1split x ).1): (y == zero ) || (T1limit y ).

If x is limit, if y is less than x, so is the successor of y

Lemma limit_pr x y: T1limit x → y < x → T1succ y < x.

Lemma pred_le a: T1pred a ≤ a.

Lemma pred_lt a: T1is_succ a → T1pred a < a.

Lemma succ_lt a: a < T1succ a.

Lemma nf_succ a: T1nf a → T1nf (T1succ a).

Lemma nf_pred a: T1nf a → T1nf (T1pred a).

Lemma succ_pred x: T1nf x → T1is_succ x → x = T1succ (T1pred x).

Lemma succ_predCE: T1is_succ T1bad ∧ ∀ y, T1bad ≠ T1succ y.

Lemma succ_p1 x: T1is_succ (T1succ x).

Lemma pred_succ x: T1nf x → T1pred (T1succ x) = x.

Lemma pred_succ_CE: T1pred (T1succ T1bad) ≠ T1bad.

Lemma succ_inj x y: T1nf x → T1nf y → (T1succ x == T1succ y ) = (x==y ).

Lemma succ_injCE: one ≠ T1bad ∧ (T1succ one = T1succ T1bad ).

Lemma lt_succ_succ x y: T1succ x < T1succ y → x < y.

Lemma le_succ_succ x y: x ≤ y → T1succ x ≤ T1succ y.

Lemma lt_succ2CE: one < T1bad ∧ T1bad < T1succ one.

Lemma lt_succ_succE x y:
T1nf x → T1nf y → (T1succ x < T1succ y ) = (x < y ).

Some properties of comparison and successor

Lemma le_succ_succE x y:
T1nf x → T1nf y → (T1succ x ≤ T1succ y ) = (x ≤ y ).

Lemma lt_succ_le_1 a b : T1succ a ≤ b → a < b.

Lemma lt_succ_le_2 a b: T1nf a → a < T1succ b → a ≤ b.

Lemma lt_succ_le_3 a b: T1nf a → (a < T1succ b ) = (a ≤ b ).

Lemma lt_succ_le_4 a b: T1nf b → (a < b ) = (T1succ a ≤ b ).

Lemma phi0_log a: a < phi0 (T1succ (T1log a)).

Lemma tail_lt_cons a n b: b < phi0 a → b < cons a n b.

Addition

The definition of addition and subtraction given here are straightforward given our interpretation of cons

Fixpoint T1add x y :=
  if x is cons a n b then
    if y is cons a' n' b' then
      if a < a' then cons a' n' b'
      else if a' < a then (cons a n (b + (cons a' n' b')))
           else (cons a (n+n').+1 b')
    else x
  else y
where "a + b" := (T1add a b) : cantor_scope.

Fixpoint T1sub x y :=
  if x is cons a n b then
    if y is cons a' n' b' then
      if x < y then zero
      else if a' < a then cons a n b
           else if (n < n')%N then zero
                else if (a==zero ) then
                       if (n ==n') then zero else cons zero ((n-n').-1) zero
                     else if (n == n') then b - b' else cons a (n-n').-1 b
    else x
  else zero
where "x - y" := (T1sub x y):cantor_scope.

Easy properties

Lemma succ_is_add_one a: T1succ a = a + one.

Lemma add1Nfin a: ~~ T1finite a → one + a = a.

Lemma sub1Nfin a: ~~ T1finite a → a - one = a.

Lemma sub1a x: x != zero → T1nf x → x = one + (x - one ).

Lemma sub1b x: T1nf x → x = (one + x ) - one.

Lemma sub_1aCE (a:= cons zero 0 T1bad) : one + (a - one ) != a.

Lemma sub_1bCE (a:= cons zero 0 T1bad) : (one + a - one) != a.

Lemma T1add0n : left_id zero T1add.
Lemma T1addn0: right_id zero T1add.

Lemma T1subn0 x: x - zero = x.

Lemma T1subnn x: x - x = zero.

Lemma add_int n m : \F n + \F m = \F (n +m)%N.

Lemma sub_int n m : \F n - \F m = \F (n -m)%N.

Lemma add_fin_omega n: \F n + T1omega = T1omega.

Lemma fooCE (x:= T1bad):
  ~~T1limit x /\(∀ u v, T1limit u → x ≠ u + \F v.+1).

Lemma split_add x: let: (y,n) :=T1split x in T1nf x →
                                             (x == y + \F n) && ((y==zero ) || T1limit y ).

Lemma add_to_cons a n b:
  b < phi0 a → cons a n zero + b = cons a n b.

Lemma addC_CE (a := one) (b := T1omega):
  [/\ T1nf a , T1nf b & a + b ≠ b + a ].

We say that x is AP is the sum of two ordinals less than x is less than x. This conditionq holds if x has the form )φ₀(a); the converse is true when x is non-zero. We may also assume everything NF.

Lemma ap_pr0 a (x := phi0 a) b c:
  b < x → c < x → b + c < x.

Lemma ap_pr1 c:
  (∀ a b, a < c → b < c → a + b < c ) →
  (c== zero ) || T1ap c.

Lemma ap_pr2 c:
  T1nf c → c ≠ zero →
  (∀ a b, T1nf a → T1nf b → a < c → b < c → a + b < c ) →
  T1ap c.

Lemma ap_pr2CE (c := cons T1bad 1 zero):
  (∀ a b, T1nf a → T1nf b → a < c → b < c → a + b < c).

Alternate definition of an AP: if a<x then a+x=x.

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

Lemma add_simpl2 n b a' n' b': a' != zero →
cons zero n b + cons a' n' b' = cons a' n' b'.

Lemma ap_pr3 a b (x := phi0 a): b < x → b + x = x.

Lemma ap_pr4 x: (∀ b, b < x → b + x = x ) → (x == zero ) || T1ap x.

It follows tthat the sum of two NF ordinals is NF

Lemma nf_add a b: T1nf a → T1nf b → T1nf (a + b).

Results anbout addition subtraction comparison

Lemma T1add_eq0 m n: (m + n == zero ) = (m == zero ) && (n == zero ).

Lemma add_le1 a b: a ≤ a + b.

Lemma add_le2 a b: b ≤ a + b.

Lemma minus_lt a b: a < b → a - b = zero.

Lemma minus_le a b: a ≤ b → a - b = zero.

Lemma T1sub0 a: a - zero = a.

Lemma nf_sub a b: T1nf a → T1nf b → T1nf (a - b).

Lemma sub_le1 a b : T1nf a → (a - b ) ≤ a.

Lemma sub_pr a b: T1nf b → (a + b ) - a = b.

Lemma add_inj a b c : T1nf b → T1nf c → a + b = a + c → b = c.

Lemma sub_pr1 a b: T1nf b → a ≤ b → b = a + (b - a ).

Lemma sub_pr1CE: (one ≤ T1bad ) && (T1bad != one + (T1bad - one )).

Lemma sub_pr1r a b: T1nf a → a - b = zero → a ≤ b.

Lemma omega_minus_one : T1omega - one = T1omega.

Lemma sub_nz a b: T1nf b → a < b → (b - a) != zero.

Lemma sub_nzCE (a := one) (b := (cons zero 0 one)):
(a < b ) && (b -a == zero ).

Associativity of addition

Lemma T1addA c1 c2 c3: c1 + (c2 + c3 ) = (c1 + c2 ) + c3.

Lemma T1addS a b : (a + T1succ b ) = T1succ (a + b).

Lemma T1le_add2l p m n : (p + m ≤ p + n ) = (m ≤ n ).

Lemma T1lt_add2l p m n : (p + m < p + n ) = (m < n ).

Lemma T1lt_add2r p m n : (m + p < n + p ) → (m < n ).

Lemma T1le_add2r p m n : (m ≤n ) → (m + p ≤ n + p ).

Lemma T1eq_add2l p m n : (p + m == p + n ) = (m == n ).

Lemma add_le3 a b: a = a + b → b = zero.

Lemma add_le4 a b: b != zero → a < a + b.

Lemma sub_pr1rCE (a := T1bad) (b := one) : (a - b == zero ) && (b < a ).

Limits

A limit ordinal is the supremum of a sequence of ordinals. We first show that some sequences are unbounded. We then show that, if the sequence is bounded, there is a least upper bound, more preciselly, if a property is satisfied for some NF ordinal, it is satisfied for a least NF aordinal. This requires teh excluded middel principle.

Fixpoint omega_tower (n:nat) : T1 :=
  if n is p.+1 then phi0 (omega_tower p) else one.

Lemma omega_tower_nf n: T1nf (omega_tower n).

Lemma omega_tower_unbounded x: ¬ (∀ n, (omega_tower n ) < x ).

Definition ex_middle:=
  ∀ (P: T1 → Prop), let Q := ∃ x , (T1nf x ∧ P x ) in Q ∨ ¬Q.

Lemma ex_middle_pick (P: T1 → Prop): ex_middle →
                                       (∃ x , (T1nf x ∧ P x )) ∨ (∀ x, T1nf x → ¬ (P x )).

Lemma min_exists (P: T1 → Prop) x: ex_middle →
                                    T1nf x → (P x ) →
                                    ∃ y , T1nf y ∧ P y ∧ ∀ z, T1nf z → P z → y ≤ z.

Definition

We say that x is the limit of f, or the supremum of the f(i) if f(i)<x (we could use less-or-equal here as f will be strictly increasing) and if moreover, every ordinal less than x is bounded by some f(i). Note that x is then the least upper bound. The trouble is that each f(i) may be NF and x is not. Thus , we give an alternate definition. Trouble is: a function may have more then one limit (at most one of them being NF).

Notation Tf := (nat → T1).

Definition limit_v1 (f: Tf) x :=
  (∀ n, f n < x ) ∧ (∀ y, y < x → (∃ n , y ≤ f n )).

Definition limit_v2 (f: Tf) x :=
  (∀ n, f n < x ) ∧ (∀ y, T1nf y → y < x → (∃ n , y ≤ f n )).

Lemma limit_unique1 (f: Tf) x x' :limit_v1 f x → limit_v1 f x' →
                                  x = x'.

Lemma limit_unique2 (f: Tf) x x' : limit_v2 f x → limit_v2 f x' →
                                   T1nf x → T1nf x'→ x = x'.

Definition omega_plus_n n := cons one 0 (cons zero n zero).

Lemma nf_omega_plus_n n : T1nf ( omega_plus_n n).

Lemma limit_CE1: limit_v1 omega_plus_n (cons one 0 T1omega).

Lemma limit_CE2: limit_v2 omega_plus_n (cons one 1 zero).

Lemma limit_CE3: limit_v2 omega_plus_n (cons one 0 T1omega).

The normal form

To each ordinal, one can associate another ordinal that is NF. However, this is in general incompatible with other operations

Fixpoint toNF x :=
if x is cons a n b then (cons (toNF a) n zero ) + toNF b else zero.

Lemma nf_toNF x: T1nf (toNF x).

Lemma toNF_nz x : toNF x = zero → x = zero.

Lemma toNF_nf x: T1nf x → toNF x = x.

Lemma toNF_mon x : x ≤ toNF x.

Lemma toNF_ex1 x: toNF (cons zero 0 x) = one + toNF x.

Lemma toNF_ex2: toNF (cons one 0 T1omega) = cons one 1 zero.

Lemma toNF_succ (x := cons zero 0 one): toNF (T1succ x) != T1succ (toNF x).

Lemma toNF_pred (x := cons zero 0 one): toNF (T1pred x) != T1pred (toNF x).

Realizing the limit

This is a simplification of the code given for the type T3 below. We define a function F(x); so that for any limit ordinal x, if f= F(x), then f is stictly increasing (of type nat → T1), and its limit is x.

Lemma fincP (f: Tf) :
  (∀ n, f n < f n.+1) →
  (∀ n m, (n < m)%N → f n < f m ).

Definition limit_of (f: Tf) x :=
  [/\ (∀ n m, (n < m)%N → f n < f m ), limit_v2 f x & T1nf x ].

Lemma limit_unique f x y: limit_of f x → limit_of f y → x = y.

Lemma limit_lub f x y: limit_of f x → (∀ n, f n ≤ y ) → T1nf y →
                       x ≤ y.

Definition phi1 a (f:Tf) := fun n ⇒ a + f n.
Definition phi2 (f:Tf) := fun n ⇒ phi0 (f n).
Definition phi3 a:= fun n ⇒ cons a n zero.

Lemma limit1 a b f: T1nf a → limit_of f b → limit_of (phi1 a f) (a + b).

Lemma limit2 b f: limit_of f b → limit_of (phi2 f) (phi0 b).

Lemma limit3 a: T1nf a → limit_of (phi3 a) (phi0 (T1succ a)).

Normal functions

We say that f:T2 → T2 is a normal function if it is striclly increasing and the suppremum of all f(y), for y<x is f(x) whenever x is limit. Everything is assumed NF.

Fixpoint limit_fct x :=
  if x is cons a n b then
    if (b==zero ) then
      if (a==zero ) then phi3 a
      else if (T1is_succ a)
           then if (n==0) then phi3 (T1pred a) else
                  phi1 (cons a n.-1 zero) (phi3 (T1pred a))
           else if (n==0) then (phi2 (limit_fct a))
                else phi1 (cons a n.-1 zero) (phi2 (limit_fct a))
    else phi1 (cons a n zero) (limit_fct b)
  else phi3 zero.

Lemma limit_prop x: T1nf x → T1limit x → limit_of (limit_fct x) x.

Definition sup (f: T1 → T1) x z :=
  [/\ T1nf z ,
   (∀ y, T1nf y → y < x → f y ≤ z ) &
   (∀ z', T1nf z' → z' < z → ∃ y ,
                   [&& T1nf y , y < x & z' < f y ])].

Definition normal f:=
  [/\ ∀ x, T1nf x → T1nf (f x),
     (∀ x y, T1nf x → T1nf y → x < y → f x < f y )&
     (∀ x, T1nf x → T1limit x → sup f x (f x)) ].

Lemma sup_unique f x z z': sup f x z → sup f x z' → z = z'.

Lemma sup_Oalpha_zero: sup id zero zero.

Lemma sup_Oalpha_succ x: T1nf x → sup id (T1succ x) x.

Lemma sup_Oalpha_limit x: T1nf x → T1limit x → sup id x x.

Identity is normal, composition of normal functions is normal, addition is normal when the firtst argument is fixed. A normal function maps limit ordinals to limit ordinls

Lemma normal_id: normal id.

Lemma normal_limit f x: normal f → T1nf x → T1limit x → T1limit (f x).

Lemma add_normal a: T1nf a → normal (T1add a).

Lemma normal_compose f g:
normal f → normal g → normal (f \o g).

multiplication

There is a unique way to define multiplication (for NF arguments) compatible with our interpretation of cons. In the case where a and a' are zero, we could use zero or b instead of b'. With the current implementation, multiplication is associative, and there is a distributivity law

Fixpoint T1mul (c1 c2 : T1) {struct c2}:T1 :=
  if c2 is cons a' n' b' then
    if c1 is cons a n b then
       if ((a==zero ) && (a' == zero )) then cons zero (n×n' + n + n')%N b'
       else if (a'==zero ) then cons a (n×n' + n + n')%N b
       else cons (a + a') n' ((cons a n b) × b')
     else zero
  else zero
where "c1 * c2" := (T1mul c1 c2) : cantor_scope.

Lemma mul_na n b x: (cons zero n b ) × x = (cons zero n zero ) × x.

Lemma T1muln0 x: x × zero = zero.

Lemma T1mul0n x: zero × x = zero.

Lemma mul_int n m : \F n × \F m = \F (n ×m)%N.

Lemma mul_phi0 a b: phi0 (a + b) = phi0 a × phi0 b.

Lemma T1mul_eq0 x y: (x × y == zero ) = (x== zero ) || (y == zero ).

Lemma T1mul_eq1 a b: T1nf a → (a × b == one ) = ((a == one ) && (b == one )).

Lemma mul_distr: right_distributive T1mul T1add.

Lemma mulA: associative T1mul.

Note that in some case the product of x and one is not x

Lemma T1muln1 x: T1nf x → x × one = x.

Lemma T1mul1n x: one × x = x.

Lemma T1mul1nCE (x := T1bad): x × one ≠ x.

Lemma T1muln1_CE x:
  (x == x × one ) =
    (if x is cons a n b then ((a != zero ) || (b== zero )) else true ).

Lemma mul_succ x y: T1nf x → x × (T1succ y ) = x × y + x.

Lemma T1lt_mul2l x y z: x != zero → T1nf z → ((x ×y < x ×z ) = (y < z )).

Lemma mulnf0 a n b: a != zero → b < phi0 a → (cons zero n zero ) × b < phi0 a.

Lemma nf_mul a b: T1nf a → T1nf b → T1nf (a × b).

Lemma T1lt_mul2r x y z: (y × x < z × x ) → (y < z ).

Lemma T1le_mul2l x y z : x != zero → T1nf y →
    (x ×y ≤ x ×z ) = (y ≤ z ).

Lemma T1le_mul2r x y z: (y ≤ z ) → (y × x ≤ z × x ).

Lemma T1eq_mul2l p m n : p != zero → T1nf m → T1nf n →
   (p × m == p × n ) = (m == n ).

Lemma T1le_pmulr x a: T1nf a → x != zero → a ≤ a × x.

Lemma T1le_pmulrCE (x:= \F1 ) (a:=T1bad) : (a ≤ a × x ) = false.

Lemma T1le_pmulrl x a: x != zero → a ≤ x × a.

Lemma T1le_mulCE (m1:= one) (m2:= T1bad) (n1 := \F1) (n2 := one) :
   (m1 ≤ n1 ) && (m2 ≤ n2 ) && ( m1 × m2 ≤ n1 × n2 ) == false.

Lemma T1le_mul m1 m2 n1 n2 : T1nf m2 → m1 ≤ n1 → m2 ≤ n2 →
   m1 × m2 ≤ n1 × n2.

Preparation of the exponention

The prouct of an integer and omega is omega. This holds in fact for any limit ordinals. We give here a formula for the product of omega and x, and show that this is a limit ordinal. The converse holds.

Lemma mul_fin_omega n: (\F n.+1) × T1omega = T1omega.

Lemma mul_int_limit n y: T1limit y → \F n.+1 × y = y.

Lemma T1mul_omega a n b:
   T1omega × (cons a n b ) =
   if (a== zero ) then cons one n zero else cons (one + a) n (T1omega × b).

Lemma mul_omega_limit x: x != zero → T1limit (T1omega × x).

Fixpoint T1div_by_omega x :=
  if x is cons a n b then cons (a - one) n (T1div_by_omega b) else zero.

Lemma div_by_omega_pr x: T1nf x → ((x==zero ) || T1limit x )
  → T1omega × (T1div_by_omega x ) = x.

We show here every ordinal x is the product of omega and y, to which an integer is added. We study the behaviour of this decomposition and multiplication

Normality of multiplication

If a is a non-zero ordinal, the multiplication by a is normal. This means, if b is limit, the supremum of all a ×c for c<b is a×b. We show this for omega, and for some special cases. This is equivalent to existence of ordinal division.

Lemma mul_omega_pr1 a: a != zero → T1nf a →
  sup (T1mul a) T1omega (a × T1omega).

Lemma mul_omega2_pr1 a (u:= cons one 1 zero): a != zero → T1nf a →
  sup (T1mul a) u (a × u).

Lemma mul_omega_pr3 a b c: a != zero → c != zero →
   T1nf a → T1nf b → T1nf c →
  sup (T1mul a) c (a × c) →
  sup (T1mul a) (b +c) (a × (b + c )).

Exponentiation

In order to compute a ^b , we first write b as the sum of a limit ordinal and an integer n. Computing a ^n is trivial. The limit ordinal is omega times c; if a is at least one, then a ^omega = omega ^d for some d, and the result is a ^ (omega × c) = omega ^(d×c)=phi0(d×c) . This leads to the following definitions.

Fixpoint exp_F a n :=
  if n is p.+1 then a × (exp_F a p) else one.

Definition exp_O a b :=
  if (a==zero ) then if (b== zero ) then one else a
  else if (a== one ) then one
  else if (T1finite a ) then (phi0 b )
  else phi0 ((T1log a ) × T1omega × b).

Definition T1exp a b:=
  (exp_O a (T1div_by_omega (T1split b ).1)) × (exp_F a ( (T1split b ).2)).

Notation "a ^ b" := (T1exp a b) : cantor_scope.

Properties of exp_O

Lemma expO_mul1 a b: (exp_O a b ) × (one ) = exp_O a b.

Lemma nf_expO a b: T1nf a → T1nf b → T1nf (exp_O a b).

Lemma expO_n0 x: exp_O x zero = one.

Lemma expO_1n n: exp_O (one) n = one.

Lemma expO_eq0 a b: (exp_O a b == zero ) = ((a== zero ) && (b != zero )).

Lemma expO_eq1 a b: (exp_O a b == one ) = ((a== one ) || (b == zero )).

Lemma expO_add z u v: exp_O z u × exp_O z v = exp_O z (u + v).

Properties of exp_F

Lemma nf_expF a n: T1nf a → T1nf (exp_F a n).

Lemma expF_add a n m: (exp_F a n ) × (exp_F a m ) = exp_F a (n + m).

Lemma expF_mul a n m: exp_F a (n × m) = exp_F (exp_F a n) m.

Lemma expF_1n n: exp_F (one) n = one.

Lemma expF_eq0 a n: (exp_F a n == zero ) = ((a== zero ) && (n != 0)).

Lemma expF_eq1 a n: T1nf a → (exp_F a n == one ) = ((a== one ) || (n == 0)).

Properties of exp

Lemma nf_exp a b: T1nf a → T1nf b → T1nf (a ^b).

Lemma exp00: zero ^zero = one.

Lemma expx0 x: x ^zero = one.

Lemma expx_pnat x n b: x ^ (cons zero n b ) = exp_F x n.+1.

Lemma expx_nat x n: x ^ \F n = exp_F x n.

Lemma expx1 x: T1nf x → x ^ one = x.

Lemma expx1CE: T1bad ^ one = one.

Lemma exp2omega n: (\F n.+2)^ T1omega = T1omega.

Lemma exp1x x: one ^ x = one.

Lemma exp_eq0 x y: x ^y == zero = ((x==zero ) && (y != zero )).

Lemma exp0nz x: x != zero → zero ^ x = zero.

Lemma exp_eq1 x y: T1nf x → T1nf y →
(x ^y == one ) = ((x== one ) || (y == zero )).

Lemma exp_int a b: (\F a ) ^ (\F b ) = \F (a ^b%N).

Lemma exp_consCE1 (x := \F 2) (a := zero) (n := 0)(b := T1omega):
x ^(cons a n b ) != x ^(cons a n zero ) × x ^b.

Lemma pow_omega x: T1nf x → T1omega ^x = phi0 x.

Existence and uniqueness of the Cantor Normal Form

Lemma cantor_exists a n b: T1nf (cons a n b) →
    cons a n b = (T1omega ^a ) × (\F n.+1) + b.

Lemma cantor_unique a n b a' n' b':
  T1nf (cons a n b) → T1nf (cons a' n' b') →
  (T1omega ^a ) × (\F n.+1) + b = (T1omega ^a') × (\F n'.+1) + b' →
  (a =a' ∧ n = n' ∧ b = b').

Lemma cantor_CE1 : T1omega ^ T1bad != phi0 T1bad.

Lemma cantorCE2: cons zero 0 T1omega != (T1omega ^ zero ) × (one ) + T1omega.

Lemma cantorCE3: cons T1bad 0 zero != (T1omega ^ T1bad ) × (one ) + zero.

Lemma T1log_prod a b: a != zero → b != zero →
    T1log(a × b) = T1log a + T1log b.

Lemma T1log_exp0 x n: T1nf x → T1log (exp_F x n) = (T1log x ) × (\F n ).

Lemma T1log_exp1 z x: T1nf z → T1nf x → ~~ T1finite z →
   T1log (z ^ x) = (T1log z ) × x.

Lemma T1log_exp2 z u v: (z == zero ) = false → (z == one ) = false →
   T1finite z → T1nf u → T1log (z ^ (T1omega × u + \F v )) = u.

Lemma exp_FO z n v: v != zero → exp_F z n × exp_O z v = exp_O z v.

Lemma exp_FO1 z v n m: T1nf z → T1nf v → v != zero → n != 0 →
  exp_O z (v × \F n) × exp_F z m = exp_F (exp_O z v × exp_F z m) n.

Lemma exp_FO2 z m u: T1nf z → m != 0 → exp_O (exp_F z m) u = exp_O z u.

Lemma exp_FO3 z x u (w := T1div_by_omega (T1split x ).1):
   T1nf z → T1nf w → (w == zero ) = false → (z == zero ) = false →
  exp_O (z ^ x) u = phi0( T1log (z ^x) × T1omega × u).

Basic Properties

Lemma exp_sum x y z: T1nf x → T1nf y → z ^(x +y ) = z ^x × z ^y.

Lemma exp_prod x y z: T1nf z → T1nf x → T1nf y → z ^(x ×y ) = (z ^x ) ^y.

Lemma pow_mon1 x y z: T1nf x → T1nf y → T1nf z → x != zero →
y ≤ z → x ^y ≤ x ^z.

Lemma pow_mon2 x y z: T1nf x → T1nf y → T1nf z → x != zero → x != one →
y < z → x ^y < x ^z.

Lemma T1le_pmull x a: x != zero → a ≤ x × a.

Lemma pow_mon3 x y z: T1nf x → x ≤ y → x ^z ≤ y ^z.

End CantorOrdinal.

Export CantorOrdinal.

The type T2

Module Gamma0.

Definition and Equality

This is like T1 with one more argument

Inductive T2 : Set :=
  zero : T2
| cons : T2 → T2 → nat → T2 → T2.

Declare Scope g0_scope.
Delimit Scope g0_scope with g0.
Open Scope g0_scope.

Fixpoint T2eq x y {struct x} :=
  match x, y with
  | zero, zero ⇒ true
  | cons a b n c, cons a' b' n' c' ⇒
      [&& T2eq a a', T2eq b b', n== n' & T2eq c c' ]
  | _, _ ⇒ false
end.

Lemma T2eqP : Equality.axiom T2eq.

Canonical T2_eqMixin := EqMixin T2eqP.
Canonical T2_eqType := Eval hnf in EqType T2 T2_eqMixin.

Arguments T2eqP {x y}.

Lemma T2eqE a b n d a' b' n' d':
  (cons a b n d == cons a' b' n' d') =
      [&& a == a', b == b', n== n' & d == d' ].

We write psi a b instead of cons a b 0 0; we introduce omega and epsilon0. We consider also the size, this is really the depth of the object

Notation "[ x , y ]" := (cons x y 0 zero) (at level 0) :g0_scope.

Definition T2nat p := if p is n.+1 then cons zero zero n zero else zero.

Notation "\F n" := (T2nat n)(at level 29) : g0_scope.

Definition psi a b := [a , b ].

Definition one := [zero , zero ].

Definition omega := [zero , one ].

Definition epsilon0 := [one ,zero ].

Fixpoint T1T2 (c: T1) : T2 :=
  if c is CantorOrdinal.cons a n b then cons zero (T1T2 a) n (T1T2 b)
  else zero.

Fixpoint size x :=
  if x is cons a b n c then
     (maxn (size a) (maxn (size b) (size c))).+1
  else 0.

Lemma size_prop1 a b n c (l:= size (cons a b n c)):
   [/\ size a < l , size b < l , size c < l & size [a , b ] ≤ l ]%N.

Lemma size_prop a b n c a' b' n' c'
   (l := (size (cons a b n c) + size (cons a' b' n' c'))%N) :
   (size c + size c' < l)%N ∧ (size [a , b ] + size b' < l)%N ∧
   (size a' + size a < l)%N ∧ (size b + size b' < l)%N ∧
   (size b + size [a', b'] < l)%N ∧ (size a + size a' < l)%N.

Order

Comparing ordinals is complicated. We are looking for the fixpoint of some complicated expression F(a,b), in which the psi-parts of a and b appear as arguments of F. Thus, a definition by induction is impossible. However if l is the some of the size if the arguments of F, then all calls of F have a smaller value. Thus, we use a definition by induction on l. All proofs will be by induction on l as well.

Definition lt_rec f x y :=
if x is cons a b n c then
   if y is cons a' b' n' c' then
     if ( ((f a a') && (f b ([a', b'])))
         || ((a == a') && (f b b'))
         || ((f a' a) && (f ([a, b]) b'))
         || (((f a' a) && ([a, b] == b'))))
     then true
     else if ((a== a') && (b==b')) then
       if (n < n')%N then true
       else if (n == n') then (f c c') else false
       else false
   else false
else if y is cons a' b' n' c' then true else false.

Fixpoint T2lta k:=
if k is k.+1 then lt_rec (T2lta k) else fun x y ⇒ false.

Definition T2lt a b := T2lta ((size a) + size b).+1 a b.
Definition T2le (x y :T2) := (x == y ) || (T2lt x y ).
Notation "x < y" := (T2lt x y) : g0_scope.
Notation "x <= y" := (T2le x y) : g0_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : g0_scope.
Notation "x > y" := (y < x) (only parsing) : g0_scope.

Main result: Our comparison is a fix-point

Lemma T2ltE x y : x < y = lt_rec T2lt x y.

This is how we compare two psi-terms

Definition lt_psi a b a' b':=
      ((a < a') && (b < [a', b']))
   || ((a == a') && (b < b'))
   || ((a' < a ) && ([a , b ] < b'))
   || ((a' < a ) && ([a , b ] == b')).

Lemma T2lt_psi a b a' b': [a ,b ] < [a', b'] = lt_psi a b a' b'.

Lemma T2lt_consE a b n c a' b' n' c' :
   cons a b n c < cons a' b' n' c' =
     if (lt_psi a b a' b') then true
     else if ((a== a') && (b==b')) then
       if (n < n')%N then true
       else if (n == n') then (c < c') else false
       else false.

Less-or-equal

Lemma T2le_consE a b n c a' b' n' c' :
   cons a b n c ≤ cons a' b' n' c' =
     if (lt_psi a b a' b') then true
     else if ((a== a') && (b==b')) then
       if (n < n')%N then true
       else if (n == n') then (c ≤ c') else false
       else false.

Lemma T2ltn0 x: (x < zero ) = false.
Lemma T2lt0n x: (zero < x ) = (x != zero ).
Lemma T2le0n x: zero ≤ x.
Lemma T2len0 x: (x ≤ zero ) = (x == zero ).
Lemma omega_lt_epsilon0: omega < epsilon0.

Lemma T2ltnn x: (x < x ) = false.

Lemma T2lt_ne a b : a < b → (a == b ) = false.

Lemma T2lt_ne' a b : a < b → (b == a ) = false.

Lemma T2ltW a b : (a < b ) → (a ≤ b ).

Lemma T2le_eqVlt a b : (a ≤ b ) = (a == b ) || (a < b ).

Lemma T2lt_neAle a b : (a < b ) = (a != b ) && (a ≤ b ).

Lemma T2lenn x: x ≤ x.

#[local] Hint Resolve T2lenn : core.

Lemma T2ge1 x: (one ≤ x ) = (x != zero ).

Lemma T2lt1 x: (x < one ) = (x==zero ).

Lemma T2nat_inc n p : (n < p)%N = (\F n < \F p ).

Lemma psi_lt1 a b c n a' b':
   cons a b n c < [a', b'] = ([a , b ] < [a', b']).

Lemma psi_lt2 a b n c n' c': cons a b n' c' < cons a b n c =
   (if (n' < n)%N then true else if n' == n then c' < c else false ).

Lemma T1T2_inj n p : (n == p ) = (T1T2 n == T1T2 p ).

Lemma T1T2_inc n p : (n < p)%ca = (T1T2 n < T1T2 p)%g0.

First two non-trivial results

Lemma T2lt_anti b a: a < b → (b < a ) = false.

Lemma T2lt_trichotomy a b: [|| (a < b ), (a==b ) | (b < a )].

what follows is the same as for T1

Lemma T2leNgt a b: (a ≤ b ) = ~~ (b < a ).

Lemma T2ltNge a b: (a < b ) = ~~ (b ≤ a ).

Lemma T2eq_le m n : (m == n ) = ((m ≤ n ) && (n ≤ m )).

Lemma T2le_total m n : (m ≤ n ) || (n ≤ m ).

CoInductive T2ltn_xor_geq m n : bool → bool → Set :=
  | T2LtnNotGeq of m < n : T2ltn_xor_geq m n false true
  | T2GeqNotLtn of n ≤ m : T2ltn_xor_geq m n true false.

CoInductive T2leq_xor_gtn m n : bool → bool → Set :=
  | T2GeqNotGtn of m ≤ n : T2leq_xor_gtn m n true false
  | T2GtnNotLeq of n < m : T2leq_xor_gtn m n false true.

CoInductive compare_T2 m n : bool → bool → bool → Set :=
  | CompareT2Lt of m < n : compare_T2 m n true false false
  | CompareT2Gt of m > n : compare_T2 m n false true false
  | CompareT2Eq of m = n : compare_T2 m n false false true.

Lemma T2leP x y : T2leq_xor_gtn x y (x ≤ y) (y < x).

Lemma T2ltP m n : T2ltn_xor_geq m n (n ≤ m) (m < n).

Lemma T2ltgtP m n : compare_T2 m n (m < n) (n < m) (m == n).

Lemma T2lt_psi_aux a b a' b': a < a' → b < [a', b'] → [a ,b ] < [a',b'].

Lemma T2gt1 x: (one < x ) = ((x != zero ) && (x != one )).

Second non-trivial result

Theorem T2lt_trans b a c: a < b → b < c → a < c.

Lemma T2lt_le_trans b a c: a < b → b ≤ c → a < c.

Lemma T2le_lt_trans b a c: a ≤ b → b < c → a < c.

Lemma T2le_trans b a c: a ≤ b → b ≤ c → a ≤ c.

Lemma T2le_psi1 a b n c: [a , b ] ≤ cons a b n c.

Lemma T2lt_psi_b a b: b < [a ,b ].

Lemma T2lt_psi_a a b: a < [a ,b ].

Normal form

Same as in T1. TODO:: show that compraison is well-founded for NF

Fixpoint T2nf x :=
  if x is cons a b n c then [&& T2nf a, T2nf b, T2nf c & c < [a,b] ]
  else true.

Lemma T2nf_cons_cons a b n a' b' n' c':
  T2nf(cons a b n (cons a' b' n' c')) =
   [&& [a', b'] < [a , b ], T2nf a , T2nf b & T2nf(cons a' b' n' c') ].

Lemma nf_psi a b n: T2nf (cons a b n zero) = T2nf a && T2nf b.

Lemma T2nf_consE a b n c:
    T2nf (cons a b n c) = [&& T2nf a , T2nf b , T2nf c & c < [a ,b ] ].

Lemma nf_omega : T2nf omega.
Lemma nf_one : T2nf one.
Lemma nf_finite n: T2nf (\F n).

Successor and predecessor

Same as for T1

Lemma lt_tail a b n c: T2nf (cons a b n c) → c < cons a b n c.

Lemma T1T2range1 x: T1T2 x < epsilon0.

Lemma T1T2range2 x: T2nf x → x < epsilon0 → {y : T1 | x = T1T2 y }.

Definition T2finite x:=
  if x is cons a b n c then ([a,b]==one) else true.

Fixpoint T2limit x :=
  if x is cons a b n c then
    if ([a,b]==one ) then false else (c== zero ) || T2limit c
  else false.

Fixpoint T2split x:=
if x is cons a b n c then
      if ([a,b]==one ) then (zero , n.+1) else
     let: (x, y) := T2split c in (cons a b n x ,y)
   else (zero ,0).

Lemma T2nf_finite a b n c: [a ,b ]==one → T2nf (cons a b n c) → c = zero.

Lemma split_finite x: ((T2split x ).1 == zero ) = T2finite x.

Lemma T2finite2 x: T2finite x → T2nf x → x = \F ((T2split x ).2 ).

Lemma omega_least_inf1 x: T2finite x → x < omega.

Lemma omega_least_inf2 x: ~~ T2finite x → omega ≤ x.

Lemma split_limit x: ((T2split x ).2 == 0) = ((x==zero ) || T2limit x ).

Fixpoint T2is_succ x :=
  if x is cons a b n c then ([a,b]==one ) || T2is_succ c else false.

Fixpoint T2succ x :=
  if x is cons a b n c
     then if ([a,b]==one ) then \F n.+2 else cons a b n (T2succ c)
  else one.

Fixpoint T2pred x :=
  if x is cons a b n c then
     if ([a,b]==one ) then \F n else (cons a b n (T2pred c))
  else zero.

Lemma split_is_succ x: ((T2split x ).2 != 0) = (T2is_succ x ).

Lemma split_succ x: let:(y,n):= T2split x in T2split (T2succ x) = (y,n.+1).

Lemma split_pred x: let:(y,n):= T2split x in T2split (T2pred x) = (y,n.-1).

Lemma split_le x : (T2split x ).1 ≤ x.

Lemma nf_split x : T2nf x → T2nf (T2split x ).1.

Lemma T2finite_succ x: T2finite x → T2finite (T2succ x).

Lemma T1succ_nat n: T2succ (\F n) = \F (n.+1).

Lemma limit_pr1 x: (x == zero ) (+) (T2limit x (+) T2is_succ x ).

Lemma limit_pr x y: T2limit x → y < x → T2succ y < x.

Lemma T2le_psi_b a b : T2succ b ≤ [a ,b ].

Lemma pred_le a: T2pred a ≤ a.

Lemma pred_lt a: T2is_succ a → T2pred a < a.

Lemma succ_lt a: a < T2succ a.

Lemma nf_succ a: T2nf a → T2nf (T2succ a).

Lemma nf_pred a: T2nf a → T2nf (T2pred a).

Lemma succ_pred x: T2nf x → T2is_succ x → x = T2succ (T2pred x).

Lemma succ_p1 x: T2is_succ (T2succ x).

Lemma pred_succ x: T2nf x → T2pred (T2succ x) = x.

Lemma succ_inj x y: T2nf x → T2nf y → (T2succ x == T2succ y ) = (x==y ).

Lemma lt_succ_succ x y: T2succ x < T2succ y → x < y.

Lemma le_succ_succ x y: x ≤ y → T2succ x ≤ T2succ y.

Lemma lt_succ_succE x y:
  T2nf x → T2nf y → (T2succ x < T2succ y ) = (x < y ).

Lemma le_succ_succE x y:
  T2nf x → T2nf y → (T2succ x ≤ T2succ y ) = (x ≤ y ).

Lemma lt_succ_le_1 a b : T2succ a ≤ b → a < b.

Lemma lt_succ_le_2 a b: T2nf a → a < T2succ b → a ≤ b.

Lemma lt_succ_le_3 a b: T2nf a → (a < T2succ b ) = (a ≤ b ).

Lemma lt_succ_le_4 a b: T2nf b → (a < b ) = (T2succ a ≤ b ).

Lemma succ_nz x: T2succ x != zero.

Lemma succ_psi a b: [a , b ] != one → T2succ [a ,b ] = cons a b 0 one.

Lemma succ_psi_lt x a b : [a , b ] != one → x < [a ,b ] → T2succ x < [a ,b ].

Lemma succ_psi_lt2 a b x: [a , b ] != one → ([a , b ] ≤ T2succ x ) = ([a , b ] ≤ x ).

Addition

same as for T1

Fixpoint T2add x y :=
  if x is cons a b n c then
    if y is cons a' b' n' c' then
       if [a,b] < [a',b'] then y
       else if [a',b'] < [a,b] then cons a b n (c + y)
       else cons a b (n+n').+1 c'
    else x
  else y
where "x + y" := (T2add x y) : g0_scope.

Fixpoint T2sub x y :=
  if x is cons a b n c then
     if y is cons a' b' n' c' then
           if (x < y ) then zero
           else if ([a',b'] < [a,b]) then x
           else if (n<n')%N then zero
           else if ([a,b]==one ) then
             if (n==n')%N then zero else cons zero zero ((n-n').-1) zero
           else if (n==n') then c - c' else cons a b (n - n').-1 c
     else x
  else zero
where "a - b" := (T2sub a b) : g0_scope.

Lemma T2subn0 x: x - zero = x.

Lemma T2sub0n x: zero - x = zero.

Lemma minus_lt a b: a < b → a - b = zero.

Lemma T2subnn x: x - x = zero.

Lemma minus_le a b: a ≤ b → a - b = zero.

Lemma nf_sub a b: T2nf a → T2nf b → T2nf (a - b).

Lemma sub_int n m : \F n - \F m = \F (n -m)%N.

Lemma succ_is_add_one a: T2succ a = a + one.

Lemma add1Nfin a: ~~ T2finite a → one + a = a.

Lemma sub1Nfin a: ~~ T2finite a → a - one = a.

Lemma sub1a x: x != zero → T2nf x → x = one + (x - one ).

Lemma sub1b x: T2nf x → x = (one + x ) - one.

Lemma T2add0n: left_id zero T2add.
Lemma T2addn0: right_id zero T2add.

Lemma add_int n m : \F n + \F m = \F (n +m)%N.

Lemma add_fin_omega n: \F n + omega = omega.

Lemma split_add x: let: (y,n) :=T2split x in T2nf x →
   (x == y + \F n) && ((y==zero ) || T2limit y ).

Lemma add_to_cons a b n c:
  c < [a ,b ] → cons a b n zero + c = cons a b n c.

Lemma nf_add a b: T2nf a → T2nf b → T2nf (a + b).

Lemma T2add_eq0 m n: (m + n == zero ) = (m == zero ) && (n == zero ).

Lemma add_le1 a b: a ≤ a + b.

Lemma add_le2 a b: b ≤ a + b.

Lemma sub_le1 a b : T2nf a → (a - b ) ≤ a.

Lemma sub_pr a b: T2nf b → (a + b ) - a = b.

Lemma add_inj a b c : T2nf b → T2nf c → a + b = a + c → b = c.

Lemma sub_pr1 a b: T2nf b → a ≤ b → b = a + (b - a ).

Lemma omega_minus_one : omega - one = omega.

Lemma sub_nz a b: T2nf b → a < b → (b - a) != zero.

Lemma T2addA c1 c2 c3: c1 + (c2 + c3 ) = (c1 + c2 ) + c3.

Lemma T2le_add2l p m n : (p + m ≤ p + n ) = (m ≤ n ).

Lemma T2lt_add2l p m n : (p + m < p + n ) = (m < n ).

Lemma T2lt_add2r p m n : (m + p < n + p ) → (m < n ).

Lemma T2le_add2r p m n : (m ≤n ) → (m + p ≤ n + p ).

Lemma T2eq_add2l p m n : (p + m == p + n ) = (m == n ).

Lemma add_le3 a b: a = a + b → b = zero.

Lemma add_le4 a b: b != zero → a < a + b.

Lemma sub_pr1r a b: T2nf a → a - b = zero → a ≤ b.

Definition T2ap x :=
  if x is cons a b n c then ((n==0) && (c==zero )) else false.

Lemma ap_pr0 a b (x := [a ,b ]) u v:
  u < x → v < x → u + v < x.

Lemma ap_limit x: T2ap x → (x == one ) || (T2limit x ).

Lemma ap_pr1 c:
   (∀ a b, a < c → b < c → a + b < c ) →
   (c== zero ) || T2ap c.

Lemma ap_pr2 c:
   T2nf c → c ≠ zero →
   (∀ a b, T2nf a → T2nf b → a < c → b < c → a + b < c ) →
   T2ap c.

Lemma ap_pr3 a b y (x := [a ,b ]): y < x → y + x = x.

Lemma ap_pr4 x: (∀ b, b < x → b + x = x ) → (x == zero ) || T2ap x.

The function phi

We consider he some funciton phi

Definition T2_pr1 x:= if x is cons a b n c then a else zero.
Definition T2_pr2 x:= if x is cons a b n c then b else zero.
Definition T2finite1 x:=
  if x is cons a b n c then [&& a == zero , b== zero & c == zero ] else false.

Definition phi a b :=
   if b is cons u v n k then
     if ((n==0) && (k==zero )) then
        if (a < u) then b else [a ,b ]
     else if ((n==0) && (T2finite1 k) && (a <u))
       then [a , cons u v 0 (T2pred k) ]
     else [a ,b ]
   else [a ,b ].

Lemma phi_ap x y : (phi x y ) = [T2_pr1 (phi x y), T2_pr2 (phi x y)].

Lemma phi_le1 a b: a ≤ T2_pr1 (phi a b).

Lemma phi_le2 a b: T2_pr2 (phi a b) ≤ b.

Lemma phi_le3 a b: a < T2_pr1 (phi a b) → (phi a b ) = b.

Lemma phi_fix1 a u v: a < u → phi a [u ,v ] = [u , v ].

Lemma phi_fix2 a b (u:= T2_pr1 b) (v:= T2_pr2 b):
  phi a b = b → b = [u ,v ] ∧ a < u.

Lemma phi_succ a u v n: a < u →
  phi a (cons u v 0 (\F n.+1)) = [a , cons u v 0 (\F n)].

phi a b is either b, psi a b or psi a (b-1).

Lemma phi_cases a b:
    {phi a b = b } + {phi a b = [a , b ]} +
    { phi a b = [a , T2pred b ] ∧ b = T2succ (T2pred b) }.

Lemma nf_phi x y : T2nf x → T2nf y → T2nf (phi x y).

Lemma phi_principalR a b: { c :T2 | [a , b ] = phi zero c }.

Theorem phi_spec1 a b c: c < a → phi c (phi a b) = phi a b.

Lemma phi_spec2 a x:
    T2nf a → T2nf x → (∀ c, T2nf c → c < a → phi c x = x ) →
    a ≤ T2_pr1 x.

Lemma phi_spec3 a x:
  T2nf a → T2nf x → (∀ c, T2nf c → c < a → phi c x = x ) →
  a != zero → {b : T2 | x = phi a b }.

Lemma phi_spec4a u v: u != zero → phi zero [u ,v ] = [u , v ].

Lemma phi_spec4b x: phi zero x = x →
  x = [T2_pr1 x , T2_pr2 x ] ∧ T2_pr1 x != zero.

Lemma phi_spec4c x: T2nf x → phi zero x = x →
  { b : T2 | x = phi one b }.

Lemma no_critical a: a < phi a zero.

Lemma phi_ab_le1 a b: b ≤ phi a b.

Lemma phi_ab_le2 a b:a < phi a b.

Lemma phi_inv1 a b: phi a (T2succ b) = [a ,b ] →
   { n : nat | (b = cons (T2_pr1 b) (T2_pr2 b) 0 (\F n) ∧ a < T2_pr1 b ) }.

Monotonicity is non-trivial

Lemma phi_mono_a a b b': T2nf b → b < b' → phi a b < phi a b'.

Lemma phi_mono_b a b b': T2nf b → b ≤ b' → phi a b ≤ phi a b'.

Lemma phi_mono_c a b b': T2nf b → T2nf b' → (phi a b < phi a b') = (b < b').

Lemma phi_inj a b b': T2nf b → T2nf b' → phi a b = phi a b' → b = b'.

Lemma phi_inj1 a b b': T2nf b → T2nf b' → (phi a b == phi a b') = (b == b').

Two lemmas for equal or less-than

Lemma phi_eqE a b a' b': T2nf a → T2nf a' → T2nf b → T2nf b' →
   (phi a b == phi a' b') =
    (if a < a' then b == phi a' b'
     else if a' < a then phi a b == b' else b== b').

Lemma phi_ltE a b a' b': T2nf a → T2nf a' → T2nf b → T2nf b' →
   (phi a b < phi a' b') =
    (if a < a' then b < phi a' b'
     else if a' < a then phi a b < b' else b < b').

Every x is uniquely a phi with some conditions

Lemma phi_inv0 a b a' b':
  phi a b = phi a' b' → b < phi a b → b' < phi a' b' → a = a'.

Lemma phi_inv2 a b a' b':
  phi a b = phi a' b' → b < phi a b → b' < phi a' b' → b = b'.

Lemma phi_inv3 x:
T2ap x → { a : T2 & { b : T2 |
    [/\ x = phi a b , b < x , (size a < size x)%N & (size b < size x)%N ] }}.

Expression psi in terms of phi

Definition psi_phi_aux a b :=
let (b', n) := T2split b in if phi a b' == b' then (T2succ b ) else b.

Definition psi_phi a b := phi a (psi_phi_aux a b).

Lemma psi_phi1 a b (c:= psi_phi_aux a b): c < phi a c.

End Gamma0.

Ackermann

Module Ackermann.
Declare Scope ak_scope.
Delimit Scope ak_scope with ak.
Open Scope ak_scope.

Inductive T3 : Set :=
  zero : T3
| cons : T3 → T3 → T3 → nat → T3 → T3.

Fixpoint T3eq x y {struct x} :=
  match x, y with
  | zero, zero ⇒ true
  | cons a b c n d, cons a' b' c' n' d' ⇒
      [&& T3eq a a', T3eq b b', T3eq c c', n== n' & T3eq d d' ]
  | _, _ ⇒ false
end.

Lemma T3eqP : Equality.axiom T3eq.

Canonical T3_eqMixin := EqMixin T3eqP.
Canonical T3_eqType := Eval hnf in EqType T3 T3_eqMixin.

Arguments T3eqP {x y}.

Lemma T3eqE a b c n d a' b' c' n' d':
  (cons a b c n d == cons a' b' c' n' d') =
      [&& a == a', b == b', c == c', n== n' & d == d' ].

Notation "[ x , y , z ]" := (cons x y z 0 zero) (at level 0) :ak_scope.
Definition T3nat p := if p is n.+1 then cons zero zero zero n zero else zero.
Notation "\F n" := (T3nat n)(at level 29) : ak_scope.

Fixpoint size x :=
  if x is cons a b c n d then
     (maxn (size a) (maxn (size b) (maxn (size c) (size d)))).+1
  else 0.

Lemma size_a a b c n d: (size a < size (cons a b c n d))%N.

Lemma size_b a b c n d: (size b < size (cons a b c n d))%N.

Lemma size_c a b c n d: (size c < size (cons a b c n d))%N.

Lemma size_d a b c n d: (size d < size (cons a b c n d))%N.

Lemma size_psi a b c n d: (size [a , b , c ] ≤ size (cons a b c n d))%N.

Lemma size_prop1 a b c n d (l:= size (cons a b c n d)):
   [&& size a < l , size b < l , size c < l , size d < l
   & size [a , b , c ] ≤ l ]%N.

Lemma size_prop a b c n d a' b' c' n' d'
   (l := ((size (cons a b c n d) + size (cons a' b' c' n' d')))%N) :
  [&& (size a' + size a < l ), (size b + size b' < l ),
   (size c + size c' < l ), (size d + size d' < l ),
   (size a + size a' < l ), (size b' + size b < l ),
   (size [a , b , c ] + size b' < l ),(size b + size [a', b', c'] < l ),
   (size [a , b , c ] + size c' < l ) &(size c + size [a', b', c'] < l )]%N.

Comparison

Definition lt_psi_rec f a b c a' b' c' (x := [a ,b ,c ])(x':= [a', b', c']):=
  [|| [&& a==a', b==b' & f c c'],
      [&& a==a', f b b' & f c x'],
      [&& a==a', f b' b & f x c'],
      [&& a==a', f b' b & x == c'],
      [&& f a a', f b x' & f c x'],
      ((f a' a ) && f x b'),
      ((f a' a ) && (x == b')),
      ((f a' a ) && f x c') |
      ((f a' a ) && (x == c'))].

Definition lt_rec f x y :=
if x is cons a b c n d then
   if y is cons a' b' c' n' d' then
     if (lt_psi_rec f a b c a' b' c')
     then true
     else if ((a== a') && (b==b') && (c==c')) then
       if (n < n')%N then true
       else if (n == n') then (f d d') else false
       else false
   else false
else if y is cons a' b' c' n' d' then true else false.

Fixpoint T3lta k {struct k}:=
if k is k.+1 then lt_rec (T3lta k) else fun x y ⇒ false.

Definition T3lt a b := T3lta ((size a) + size b).+1 a b.
Definition T3le (x y :T3) := (x == y ) || (T3lt x y ).
Notation "x < y" := (T3lt x y) : ak_scope.
Notation "x <= y" := (T3le x y) : ak_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : ak_scope.
Notation "x > y" := (y < x) (only parsing) : ak_scope.

Lemma T3ltE x y : x < y = lt_rec T3lt x y.

Definition lt_psi (a b c a' b' c': T3):=
[|| [&& a==a', b==b' & c < c'],
      [&& a==a', b < b' & c < [a',b',c']],
      [&& a==a', b' < b & [a ,b ,c ] < c'],
      [&& a==a', b' < b & [a ,b ,c ] == c'],
      [&& a < a', b < [a',b',c'] & c < [a',b',c']],
      ((a' < a ) && ([a ,b ,c ] < b')),
      ((a' < a ) && ([a ,b ,c ] == b')),
      ((a' < a ) && ([a ,b ,c ] < c')) |
      ((a' < a ) && ([a ,b ,c ] == c'))].

Lemma T3lt_psi a b c a' b' c': [a ,b ,c ] < [a', b',c'] = lt_psi a b c a' b' c'.

Lemma T3lt_consE a b c n d a' b' c' n' d' :
   cons a b c n d < cons a' b' c' n' d' =
     if ([a , b , c ] < [a', b', c']) then true
     else if ([a , b , c ] == [a', b', c']) then
       if (n < n')%N then true
       else if (n == n') then (d < d') else false
       else false.

Lemma T3ltn0 x: (x < zero ) = false.
Lemma T3lt0n x: (zero < x ) = (x != zero ).

Lemma T3ltnn x: (x < x ) = false.

Lemma T3lt_ne a b : a < b → (a == b ) = false.

Lemma T3lt_ne' a b : a < b → (b == a ) = false.

Lemma T3ltW a b : (a < b ) → (a ≤ b ).

Lemma T3le_eqVlt a b : (a ≤ b ) = (a == b ) || (a < b ).

Lemma T3lt_neAle a b : (a < b ) = (a != b ) && (a ≤ b ).

Definition one := [zero ,zero ,zero ].
Definition omega := [zero ,zero , one ].
Definition epsilon0 := [zero , one , zero ].
Definition T3bad := cons zero zero zero 0 one.

Lemma T3le0n x: zero ≤ x.
Lemma T3len0 x: (x ≤ zero ) = (x == zero ).

Lemma T3ge1 x: (one ≤ x ) = (x != zero ).

Lemma T3lt1 x: (x < one ) = (x==zero ).

Lemma T3lcp0_pr x y: x < y → (y==zero ) = false.

Lemma finite_ltP n p : (n < p)%N = (\F n < \F p ).

Lemma T3lt_anti b a: a < b → (b < a ) = false.

Lemma T3lt_trichotomy a b: [|| (a < b ), (a==b ) | (b < a )].

Lemma T3lenn x: x ≤ x.

#[local] Hint Resolve T3lenn : core.

Lemma T3leNgt a b: (a ≤ b ) = ~~ (b < a ).

Lemma T3ltNge a b: (a < b ) = ~~ (b ≤ a ).

Lemma T3eq_le m n : (m == n ) = ((m ≤ n ) && (n ≤ m )).

CoInductive T3ltn_xor_geq m n : bool → bool → Set :=
  | T3LtnNotGeq of m < n : T3ltn_xor_geq m n false true
  | T3GeqNotLtn of n ≤ m : T3ltn_xor_geq m n true false.

CoInductive T3leq_xor_gtn m n : bool → bool → Set :=
  | T3GeqNotGtn of m ≤ n : T3leq_xor_gtn m n true false
  | T3GtnNotLeq of n < m : T3leq_xor_gtn m n false true.

CoInductive compare_T3 m n : bool → bool → bool → Set :=
  | CompareT3Lt of m < n : compare_T3 m n true false false
  | CompareT3Gt of m > n : compare_T3 m n false true false
  | CompareT3Eq of m = n : compare_T3 m n false false true.

Lemma T3leP x y : T3leq_xor_gtn x y (x ≤ y) (y < x).

Lemma T3ltP m n : T3ltn_xor_geq m n (n ≤ m) (m < n).

Lemma T3ltgtP m n : compare_T3 m n (m < n) (n < m) (m == n).

Lemma T3le_consE a b c n d a' b' c' n' d' :
   cons a b c n d ≤ cons a' b' c' n' d' =
     if ([a , b , c ] < [a', b', c']) then true
     else if ([a , b , c ] == [a', b', c']) then
       if (n < n')%N then true
       else if (n == n') then (d ≤ d') else false
       else false.

Lemma T3lt_psi' a b c a' b' c': [a , b , c ] < [a', b', c' ] =
  [|| [&& a==a', b==b' & c < c'],
      [&& a==a', b < b' & c < [a', b', c'] ],
      [&& a==a', b' <b & [a ,b ,c ] ≤ c'],
      [&& a < a', b < [a', b', c'] & c < [a', b', c']],
      ((a' < a ) && ([a ,b ,c ] ≤ b')) |
      ((a' < a ) && ([a ,b ,c ] ≤ c'))].

Theorem T3lt_trans b a c: a < b → b < c → a < c.

Lemma T3lt_le_trans b a c: a < b → b ≤ c → a < c.

Lemma T3le_lt_trans b a c: a ≤ b → b < c → a < c.

Lemma T3le_trans b a c: a ≤ b → b ≤ c → a ≤ c.

Lemma T3le_anti : antisymmetric T3le.

Lemma T3le_total m n : (m ≤ n ) || (n ≤ m ).

Lemma T3le_psi a b c n d: [a ,b ,c ] ≤ cons a b c n d.

Lemma T3lt_psi_bc a b c: ((b < [a ,b ,c ]) && (c < [a , b , c ])).

Lemma psi_lt1 a b c d n a' b' c':
   cons a b c n d < [a', b', c'] = ([a , b ,c ] < [a', b', c']).

Lemma psi_lt2 a b c n d n' d': cons a b c n' d' < cons a b c n d =
   (if (n' < n)%N then true else if n' == n then d' < d else false ).

Lemma T3lt_psi_b a b c: b < [a ,b ,c ].

Lemma T3lt_psi_c a b c: c < [a ,b ,c ].

Lemma T3lt_psi_a a b c: a < [a ,b ,c ].

Normal form

Fixpoint T3nf x :=
  if x is cons a b c _ d
  then [&& T3nf a, T3nf b, T3nf c, T3nf d & d < [a,b,c] ]
  else true.

Lemma nf_0: T3nf zero.

Lemma nf_psi a b c: T3nf [a , b , c ] = [&& T3nf a , T3nf b & T3nf c ].

Lemma nf_int n: T3nf (\F n).

Lemma nf_cons_cons a b c n a' b' c' n' d':
  T3nf (cons a b c n (cons a' b' c' n' d')) =
   [&& [a', b',c'] < [a , b ,c ], T3nf [a ,b , c ] &
    T3nf (cons a' b' c' n' d') ].

Lemma nf_consE a b c n d:
    T3nf (cons a b c n d) = [&& T3nf [a ,b ,c ], T3nf d & d < [a ,b ,c ] ].

Lemma nf_Wf : well_founded_P T3nf T3lt.

Theorem lt_not_wf : ¬ (well_founded T3lt ).

Successor Predecessor

Fixpoint T1_T3 (c:CantorOrdinal.T1) : T3 :=
  if c is CantorOrdinal.cons a n b then cons zero zero (T1_T3 a) n (T1_T3 b)
  else zero.

Lemma lt_epsilon0 a b c n d :
  cons a b c n d < epsilon0 = [&& a==zero , b == zero & c < epsilon0 ].

Lemma T1T3_lt_epsilon0 x: T1_T3 x < epsilon0.

Delimit Scope cantor_scope with ca.
Notation "x < y" := (CantorOrdinal.T1lt x y) : cantor_scope.

Lemma T1T3_inc x y: (x <y)%ca→ (T1_T3 x ) < (T1_T3 y ).

Lemma TT1T3_inj: injective T1_T3.

Lemma T1T3_surj x: T3nf x → x < epsilon0 → ∃ y , x = T1_T3 y.

Definition all_zero a b c :=[&& a==zero , b==zero & c== zero ].

Fixpoint T3limit x :=
  if x is cons a b c n d then
    if (all_zero a b c) then false else (d== zero ) || T3limit d
  else false.

Definition T3finite x :=
   if x is cons a b c n d then all_zero a b c else true.

Fixpoint T3split x:=
if x is cons a b c n d then
      if all_zero a b c then (zero , n.+1) else
     let: (x, y) := T3split d in (cons a b c n x ,y)
   else (zero ,0).

Lemma all_zeroE a b c: all_zero a b c = ([a ,b ,c ] == one ).

Lemma T3nf_finite a b c n d: all_zero a b c → T3nf (cons a b c n d) →
    d = zero.

Lemma split_finite x: ((T3split x ).1 == zero ) = T3finite x.

Lemma T3finite1 n: T3finite (\F n).

Lemma T3finite2 x: T3finite x → T3nf x → x = \F ((T3split x ).2 ).

Lemma T3gt1 x: (one < x ) = ((x != zero ) && (x != one )).

Lemma omega_least_inf1 x: T3finite x → x < omega.

Lemma omega_least_inf2 x: ~~ T3finite x → omega ≤ x.

Lemma lt_omega1 c n d a' b' c' n' d' :
   cons zero zero c n d < cons a' b' c' n' d' =
     if ((a'== zero ) && (b'==zero )) then
       ((c < c') || ((c==c') && ((n < n')%N || ((n==n') && (d < d')))))
    else (c < [a', b', c']).

Lemma lt_omega2 c a' b' c' :
   ([zero , zero , c ] < [a', b', c']) =
     if ((a'== zero ) && (b'==zero )) then c < c' else (c < [a', b', c']).

Lemma split_limit x: ((T3split x ).2 == 0) = ((x==zero ) || T3limit x ).

Fixpoint T3is_succ x :=
  if x is cons a b c n d then (all_zero a b c) || T3is_succ d else false.

Fixpoint T3succ x :=
  if x is cons a b c n d
     then if all_zero a b c then \F n.+2 else cons a b c n (T3succ d)
  else one.

Fixpoint T3pred x :=
  if x is cons a b c n d then
     if all_zero a b c then \F n else (cons a b c n (T3pred d))
  else zero.

Lemma split_is_succ x: ((T3split x ).2 != 0) = (T3is_succ x ).

Lemma split_succ x: let:(y,n):= T3split x in T3split (T3succ x) = (y,n.+1).

Lemma split_pred x: let:(y,n):= T3split x in T3split (T3pred x) = (y,n.-1).

Lemma split_le x : (T3split x ).1 ≤ x.

Lemma nf_split x : T3nf x → T3nf (T3split x ).1.

Lemma T3finite_succ x: T3finite x → T3finite (T3succ x).

Lemma T1succ_nat n: T3succ (\F n) = \F (n.+1).

Lemma nf_omega : T3nf omega.
Lemma nf_finite n: T3nf (\F n).

Lemma limit_pr1 x: (x == zero ) (+) (T3limit x (+) T3is_succ x ).

Lemma limit_pr x y: T3limit x → y < x → T3succ y < x.

Lemma pred_le a: T3pred a ≤ a.
Lemma pred_lt a: T3is_succ a → T3pred a < a.

Lemma succ_lt a: a < T3succ a.

Lemma nf_succ a: T3nf a → T3nf (T3succ a).

Lemma nf_pred a: T3nf a → T3nf (T3pred a).

Lemma succ_pred x: T3nf x → T3is_succ x → x = T3succ (T3pred x).

Lemma succ_p1 x: T3is_succ (T3succ x).

Lemma pred_succ x: T3nf x → T3pred (T3succ x) = x.

Lemma succ_inj x y: T3nf x → T3nf y → (T3succ x == T3succ y ) = (x==y ).

Lemma lt_succ_succ x y: T3succ x < T3succ y → x < y.

Lemma le_succ_succ x y: x ≤ y → T3succ x ≤ T3succ y.

Lemma lt_succ_succE x y:
  T3nf x → T3nf y → (T3succ x < T3succ y ) = (x < y ).

Lemma le_succ_succE x y:
  T3nf x → T3nf y → (T3succ x ≤ T3succ y ) = (x ≤ y ).

Lemma lt_succ_le_1 a b : T3succ a ≤ b → a < b.

Lemma lt_succ_le_2 a b: T3nf a → a < T3succ b → a ≤ b.
Lemma lt_succ_le_3 a b: T3nf a → (a < T3succ b ) = (a ≤ b ).

Lemma lt_succ_le_4 a b: T3nf b → (a < b ) = (T3succ a ≤ b ).

Lemma succ_nz x: T3succ x != zero.

Lemma succ_psi a b c: [a , b , c ] != one → T3succ [a ,b ,c ] = cons a b c 0 one.

Lemma succ_psi_lt x a b c: [a , b , c ] != one →
   x < [a ,b ,c ] → T3succ x < [a ,b ,c ].

Lemma succ_psi_lt2 a b c x: [a , b , c ] != one →
  ([a , b , c ] ≤ T3succ x ) = ([a , b , c ] ≤ x ).

Addition

Fixpoint T3add x y :=
  if x is cons a b c n d then
    if y is cons a' b' c' n' d' then
       if [a,b,c] < [a',b',c'] then y
       else if [a',b',c'] < [a,b,c] then cons a b c n (d + y)
       else cons a b c (n+n').+1 d'
    else x
  else y
where "x + y" := (T3add x y) : ak_scope.

Fixpoint T3sub x y :=
  if x is cons a b c n d then
     if y is cons a' b' c' n' d' then
           if (x < y ) then zero
           else if ([a',b',c'] < [a,b,c]) then x
           else if (n<n')%N then zero
           else if ([a,b,c] == one ) then
             if (n==n')%N then zero else cons zero zero zero ((n-n').-1) zero
           else if (n==n') then d - d' else cons a b c (n - n').-1 d
     else x
  else zero
where "a - b" := (T3sub a b) : ak_scope.

Lemma T3subn0 x: x - zero = x.

Lemma T3sub0n x: zero - x = zero.

Lemma minus_lt a b: a < b → a - b = zero.

Lemma T3subnn x: x - x = zero.

Lemma minus_le a b: a ≤ b → a - b = zero.

Lemma nf_sub a b: T3nf a → T3nf b → T3nf (a - b).

Lemma sub_int n m : \F n - \F m = \F (n -m)%N.

Lemma succ_is_add_one a: T3succ a = a + one.

Lemma add1Nfin a: ~~ T3finite a → one + a = a.

Lemma sub1Nfin a: ~~ T3finite a → a - one = a.

Lemma sub1a x: x != zero → T3nf x → x = one + (x - one ).

Lemma sub1b x: T3nf x → x = (one + x ) - one.

Lemma sub_1aCE (a:= T3bad) : one + (a - one ) != a.

Lemma sub_1bCE (a:= T3bad) : (one + a - one) != a.

Lemma T3add0n : left_id zero T3add.
Lemma T3addn0: right_id zero T3add.

Lemma add_int n m : \F n + \F m = \F (n +m)%N.

Lemma add_fin_omega n: \F n + omega = omega.

Lemma fooCE (x:= T3bad):
   ~~T3limit x /\(∀ u v, T3limit u → x ≠ u + \F v.+1).

Lemma split_add x: let: (y,n) :=T3split x in T3nf x →
   (x == y + \F n) && ((y==zero ) || T3limit y ).

Lemma add_to_cons a b c n d:
  d < [ a ,b ,c ] → cons a b c n zero + d = cons a b c n d.

Lemma addC_CE (a := one) (b := omega):
  [&& T3nf a , T3nf b & a + b != b + a ].

Lemma nf_add a b: T3nf a → T3nf b → T3nf (a + b).

Lemma T3add_eq0 m n: (m + n == zero ) = (m == zero ) && (n == zero ).

Lemma add_le1 a b: a ≤ a + b.

Lemma add_le2 a b: b ≤ a + b.

Lemma sub_le1 a b : T3nf a → (a - b ) ≤ a.

Lemma sub_pr a b: T3nf b → (a + b ) - a = b.

Lemma add_inj a b c : T3nf b → T3nf c → a + b = a + c → b = c.

Lemma sub_pr1 a b: T3nf b → a ≤ b → b = a + (b - a ).

Lemma omega_minus_one : omega - one = omega.

Lemma sub_nz a b: T3nf b → a < b → (b - a) != zero.

Lemma T3addA c1 c2 c3: c1 + (c2 + c3 ) = (c1 + c2 ) + c3.

Lemma T3le_add2l p m n : (p + m ≤ p + n ) = (m ≤ n ).

Lemma T3lt_add2l p m n : (p + m < p + n ) = (m < n ).

Lemma T3lt_add2r p m n : (m + p < n + p ) → (m < n ).

Lemma T3le_add2r p m n : (m ≤n ) → (m + p ≤ n + p ).

Lemma T3eq_add2l p m n : (p + m == p + n ) = (m == n ).

Lemma add_le3 a b: a = a + b → b = zero.

Lemma add_le4 a b: b != zero → a < a + b.

Lemma sub_pr1r a b: T3nf a → a - b = zero → a ≤ b.

Lemma sub_pr1rCE (a := T3bad) (b := one) : (a - b == zero ) && (b < a ).

Lemma T3addS a b : (a + T3succ b ) = T3succ (a + b).

limit

Notation Tf := (nat → T3).

Definition limit_of (f: Tf) x :=
  [/\ (∀ n m, (n < m)%N → f n < f m ),
      (∀ n, f n < x ) &
      (∀ y, T3nf y → y < x → (∃ n , y ≤ f n ))].

Lemma fincP (f: Tf) :
  (∀ n, f n < f n.+1) →
  (∀ n m, (n < m)%N → f n < f m ).

Definition limit12_hyp a b c:=
   if c is cons a1 b1 c1 n1 d1 then
       (n1 == 0) && (d1 == zero ) &&
       ( ((a == a1) && (b < b1)) || ((a < a1) && (b < c )))
   else false.

Definition phi0:= fun _ :nat ⇒ zero.
Definition phi1 a (f:Tf) := fun n ⇒ a + f n.
Definition phi5 (f:Tf) := fun n ⇒ [f n , zero ,zero ].
Definition phi12a a b (f:Tf) := fun n ⇒ [a ,b ,f n ].

Lemma limit1 a b f:
   T3nf a → (limit_of f b ) → (limit_of (phi1 a f) (a + b)).

Lemma limit5 f x: (limit_of f x ) → (limit_of (phi5 f) [x ,zero ,zero ]).

Lemma limit12a f a b c: ~~ (limit12_hyp a b c ) →
   (limit_of f c ) → (limit_of (phi12a a b f)[a , b , c ]).

Fixpoint phi3 x n := if n is n.+1 then phi3 x n + x else x.

Lemma phi3v a b c k: phi3 [a ,b ,c ] k = cons a b c k zero.

Lemma limit3 x: limit_of (phi3 [zero ,zero ,x ]) [zero , zero , T3succ x ].

Lemma limit2: limit_of (phi3 one) omega.

Lemma limit12b1 x: (limit12_hyp zero zero x ) →
  limit_of (phi3 x) [zero , zero , x ].

Fixpoint phi4 x n :=
   if n is n.+1 then [x , phi4 x n , phi4 x n ] else [x ,zero ,zero ].

Lemma limit4 x: limit_of (phi4 x) [T3succ x , zero , zero ].

Fixpoint phi8 x y n :=
   if n is n.+1 then [x , phi8 x y n , phi8 x y n ] else [T3succ x ,zero ,y ].

Lemma limit8 x y: limit_of (phi8 x y) [T3succ x , zero , T3succ y ].

Fixpoint phi12b2 x y n :=
   if n is n.+1 then [x , phi12b2 x y n , phi12b2 x y n ] else y.

Lemma limit12b2 x y: (limit12_hyp (T3succ x) zero y ) →
    limit_of (phi12b2 x y) [T3succ x , zero , y ].

Fixpoint phi6 x y n :=
   if n is n.+1 then [x , y , phi6 x y n ] else [x ,y ,zero ].

Fixpoint phi10 x y z n :=
   if n is n.+1 then [x , y , phi10 x y z n ] else [x ,T3succ y ,z ].

Fixpoint phi12b4 x y z n :=
   if n is n.+1 then [x , y , phi12b4 x y z n ] else z.

Lemma limit6 x y:
    limit_of (phi6 x y) [x ,T3succ y , zero ].

Lemma limit10 x y z:
    limit_of (phi10 x y z) [x ,T3succ y , T3succ z ].

Lemma limit12b4 x y z: (limit12_hyp x (T3succ y) z ) →
    limit_of (phi12b4 x y z) [x ,T3succ y ,z ].

Fixpoint phi7 x y f n :=
  if n is n.+1 then [x , f n , phi7 x y f n ] else y.

Fixpoint phi9 x y f n :=
  if n is n.+1 then [f n , phi9 x y f n , phi9 x y f n ] else [x , zero ,y ].

Fixpoint phi11 x y z f n :=
  if n is n.+1 then [x ,f n , phi11 x y z f n ] else [x , y ,z ].

Fixpoint phi12b3 y f n :=
  if n is n.+1 then [f n , phi12b3 y f n , phi12b3 y f n ] else y.

Fixpoint phi12b5 x z f n :=
  if n is n.+1 then [x ,f n , phi12b5 x z f n ] else z.

Lemma limit7 x y f: (limit_of f y ) →
  (limit_of ( phi7 x y f) [x ,y ,zero ]).

Lemma limit9 x y f: (limit_of f x ) →
  (limit_of (phi9 x y f) [x ,zero , T3succ y ]).

Lemma limit11 x y z f: (limit_of f y ) →
  (limit_of (phi11 x y z f) [x , y , T3succ z ]).

Lemma limit12b3 x y f: (limit_of f x ) → (limit12_hyp x zero y ) →
  (limit_of (phi12b3 y f) [x , zero , y ]).

Lemma limit12b5 x y z f: (limit_of f y ) → (limit12_hyp x y z ) →
  (limit_of (phi12b5 x z f) [x ,y ,z ]).

Definition phi_rec_psi f a b c :=
  if (c==zero ) then
    if (b==zero ) then
       if (a==zero ) then phi0
       else if (T3is_succ a ) then phi4 (T3pred a)
       else phi5 (f a)
    else if (T3is_succ b ) then phi6 a (T3pred b)
    else phi7 a b (f b)
  else if (T3is_succ c ) then
    if (b==zero ) then
      if (a==zero ) then phi3 [zero ,zero , T3pred c ]
      else if (T3is_succ a ) then phi8 (T3pred a) (T3pred c)
      else phi9 a (T3pred c) (f a)
    else if (T3is_succ b ) then phi10 a (T3pred b) (T3pred c)
    else phi11 a b (T3pred c) (f b)
  else if (limit12_hyp a b c ) then
    if (b==zero ) then
      if (a==zero ) then phi3 c
      else if (T3is_succ a ) then phi12b2 (T3pred a) c
      else phi12b3 c (f a)
    else if (T3is_succ b ) then phi12b4 a (T3pred b) c
    else phi12b5 a c (f b)
  else phi12a a b (f c).

Definition phi_rec f (x: T3) :=
  if x is cons a b c n d then
  if (d==zero ) then
    if n is n.+1 then phi1 (cons a b c n zero) (phi_rec_psi f a b c)
     else phi_rec_psi f a b c
  else phi1 (cons a b c n zero) (f d)
  else phi0.

Fixpoint phia k := if k is k.+1 then phi_rec (phia k) else (fun x ⇒phi0).
Definition phi x := phia (size x).+1 x.

Lemma phiE x : phi x = phi_rec phi x.

Lemma phiE_1 a b c n:
  phi (cons a b c n.+1 zero) = phi1 (cons a b c n zero) (phi [a , b , c ]).

Lemma phiE_2 a b c n d: d != zero →
  phi (cons a b c n d) = phi1 (cons a b c n zero) (phi d).

Lemma phiE_3 a b c: phi ([a ,b ,c ]) = phi_rec_psi phi a b c.

Lemma phiL x: T3nf x → T3limit x → limit_of (phi x) x.

Lemma conc1 (x:= [zero ,zero , epsilon0 ]): limit_of (phi3 epsilon0) x.

additive principal

Definition T3ap x :=
  if x is cons a b c n d then ((n==0) && (d==zero )) else false.

Lemma ap_pr0 a b c (x := [a ,b ,c ]) u v:
  u < x → v < x → u + v < x.

Lemma ap_limit x: T3ap x → (x == one ) || (T3limit x ).

Lemma ap_pr1 c:
   (∀ a b, a < c → b < c → a + b < c ) →
   (c== zero ) || T3ap c.

Lemma ap_pr2 c:
   T3nf c → c ≠ zero →
   (∀ a b, T3nf a → T3nf b → a < c → b < c → a + b < c ) →
   T3ap c.

Lemma ap_pr3 a b c y (x := [a ,b ,c ]): y < x → y + x = x.

Lemma ap_pr4 x: (∀ b, b < x → b + x = x ) → (x == zero ) || T3ap x.

Lemma ap_pr2CE (c := cons zero zero T3bad 1 zero):
   (∀ a b, T3nf a → T3nf b → a < c → b < c → a + b < c).

Definition psi_succ x :=
  if x is cons a b c _ _ then
   if ((a==zero ) && (b==zero )) then [zero ,zero , T3succ c] else [zero ,zero , x ]
  else zero.

Lemma psi_succ_pr1 a b c: [a ,b ,c ] < psi_succ ([a ,b ,c ]).

Lemma succ_psi1 a b c (x:= [a , b , c ]): ((a != zero ) || (b != zero )) →
    (∀ a' b' c', x < [a',b',c'] → (psi_succ x ) ≤ [a',b',c']).

Lemma succ_psi2 u (x := [zero ,zero ,u ]) :
   (∀ a' b' c', T3nf c' → x < [a',b',c'] → (psi_succ x ) ≤ [a',b',c']).

Lemma succ_prCE (u:= one) (v := T3bad): (u < v ) && (v < T3succ u ).

Lemma succ_psiCE (z := [zero ,zero , T3bad ]):
   (omega < z ) && (z < (psi_succ omega )) && ~~(T3nf z ).

Definition sup_of (f: T3 → T3) x z :=
  [/\ T3nf z ,
      (∀ y, T3nf y → y < x → f y ≤ z ) &
      (∀ z', T3nf z' → z' < z → ∃ y ,
          [&& T3nf y , y < x & z' < f y ])].

Definition normal f:=
  [/\ ∀ x, T3nf x → T3nf (f x),
      (∀ x y, T3nf x → T3nf y → x < y → f x < f y )&
      (∀ x, T3nf x → T3limit x → sup_of f x (f x)) ].

Lemma sup_unique f x z z': sup_of f x z → sup_of f x z' → z = z'.

Lemma sup_Oalpha_zero: sup_of id zero zero.

Lemma sup_Oalpha_limit x: T3nf x → T3limit x → sup_of id x x.

Lemma sup_Oalpha_succ x: T3nf x → sup_of id (T3succ x) x.

Lemma normal_id: normal id.

Lemma normal_limit f x: normal f → T3nf x → T3limit x → T3limit (f x).

Lemma normal_compose f g:
   normal f → normal g → normal (f \o g).

Lemma add_normal a: T3nf a → normal (T3add a).

End Ackermann.