Library hydras.Gamma0.T2
Data-type for Veblen normal form
(ordinals below Gamma0)
From Coq Require Import Arith Compare_dec Relations Wellfounded Lia.
From hydras Require Import More_Arith Restriction T1 OrdNotations Compat815.
Set Implicit Arguments.
Declare Scope T2_scope.
Delimit Scope T2_scope with t2.
Open Scope T2_scope.
Inductive T2 : Set :=
| zero : T2
| gcons : T2 → T2 → nat → T2 → T2.
Notation "[ alpha , beta ]" := (gcons alpha beta 0 zero)
(at level 0): T2_scope.
Definition psi alpha beta := [alpha, beta].
Definition psi_term alpha :=
match alpha with zero ⇒ zero
| gcons a b n c ⇒ [a, b]
end.
Lemma psi_eq : ∀ a b, psi a b = [a,b].
Ltac fold_psi := rewrite <- psi_eq.
Ltac fold_psis := repeat fold_psi.
Notation one := [zero,zero].
Notation FS n := (gcons zero zero n zero).
Definition fin (n:nat) := match n with 0 ⇒ zero | S p ⇒ FS p end.
Coercion fin : nat >-> T2.
Notation omega := [zero,one].
Notation epsilon0 := [one,zero].
Definition epsilon alpha := [one, alpha].
Inductive is_finite: T2 → Set :=
zero_finite : is_finite zero
|succ_finite : ∀ n, is_finite (gcons zero zero n zero).
#[global] Hint Constructors is_finite : T2.
Fixpoint T1_to_T2 (alpha :T1) : T2 :=
match alpha with
| T1.zero ⇒ zero
| T1.cons a n b ⇒ gcons zero (T1_to_T2 a) n (T1_to_T2 b)
end.
additive principals
strict order on terms
Reserved Notation "x 't2<' y" (at level 70, no associativity).
Reserved Notation "x 't2<=' y" (at level 70, no associativity).
Reserved Notation "x 't2>=' y" (at level 70, no associativity).
Reserved Notation "x 't2>' y" (at level 70, no associativity).
Reserved Notation "x 't2<=' y 't2<=' z" (at level 70, y at next level).
Reserved Notation "x 't2<=' y 't2<' z" (at level 70, y at next level).
Reserved Notation "x 't2<' y 't2<' z" (at level 70, y at next level).
Reserved Notation "x 't2<' y 't2<=' z" (at level 70, y at next level).
Inductive lt : T2 → T2 → Prop :=
|
lt_1 : ∀ alpha beta n gamma, zero t2< gcons alpha beta n gamma
|
lt_2 : ∀ alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
alpha1 t2< alpha2 →
beta1 t2< gcons alpha2 beta2 0 zero →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha2 beta2 n2 gamma2
|
lt_3 : ∀ alpha1 beta1 beta2 n1 n2 gamma1 gamma2,
beta1 t2< beta2 →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha1 beta2 n2 gamma2
|
lt_4 : ∀ alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
alpha2 t2< alpha1 →
[alpha1, beta1] t2< beta2 →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha2 beta2 n2 gamma2
|
lt_5 : ∀ alpha1 alpha2 beta1 n1 n2 gamma1 gamma2,
alpha2 t2< alpha1 →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha2 [alpha1, beta1] n2 gamma2
|
lt_6 : ∀ alpha1 beta1 n1 n2 gamma1 gamma2,
(n1 < n2)%nat →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha1 beta1 n2 gamma2
|
lt_7 : ∀ alpha1 beta1 n1 gamma1 gamma2,
gamma1 t2< gamma2 →
gcons alpha1 beta1 n1 gamma1 t2<
gcons alpha1 beta1 n1 gamma2
where "o1 t2< o2" := (lt o1 o2): T2_scope.
#[global] Hint Constructors lt : T2.
Definition le t t' := t = t' ∨ t t2< t'.
#[global] Hint Unfold le : T2.
Notation "o1 t2<= o2" := (le o1 o2): T2_scope.
Example Ex1: 0 t2< epsilon0.
Example Ex2: omega t2< epsilon0.
Example Ex3: gcons omega 8 12 56 t2< gcons omega 8 12 57.
Example Ex4: epsilon0 t2< [2,1].
Example Ex5 : [2,1] t2< [2,3].
Example Ex6 : gcons 1 0 12 omega t2< [0,[2,1]].
Example Ex7 : gcons 2 1 42 epsilon0 t2< [1, [2,1]].
Definition gtail c := match c with
| zero ⇒ zero
| gcons a b n c ⇒ c
end.
Inductive nf : T2 → Prop :=
| zero_nf : nf zero
| single_nf : ∀ a b n,
nf a →
nf b → nf (gcons a b n zero)
| gcons_nf : ∀ a b n a' b' n' c',
[a', b'] t2< [a, b] →
nf a → nf b →
nf(gcons a' b' n' c')→
nf(gcons a b n (gcons a' b' n' c')).
#[global] Hint Constructors nf : T2.
Lemma nf_fin i : nf (fin i).
Lemma nf_omega : nf omega.
Lemma nf_epsilon0 : nf epsilon0.
Lemma nf_epsilon : ∀ alpha, nf alpha → nf (epsilon alpha).
Example Ex8: nf (gcons 2 1 42 epsilon0).
Inductive is_successor : T2 → Prop :=
finite_succ : ∀ n , is_successor (gcons zero zero n zero)
|cons_succ : ∀ a b n c, nf (gcons a b n c) → is_successor c →
is_successor (gcons a b n c).
Inductive is_limit : T2 → Prop :=
| is_limit_0 : ∀ alpha beta n, zero t2< alpha ∨ zero t2< beta →
nf alpha → nf beta →
is_limit (gcons alpha beta n zero)
| is_limit_cons : ∀ alpha beta n gamma,
is_limit gamma →
nf (gcons alpha beta n gamma) →
is_limit (gcons alpha beta n gamma).
Fixpoint succ (a:T2) : T2 :=
match a with zero ⇒ one
| gcons zero zero n c ⇒ fin (S (S n))
| gcons a b n c ⇒ gcons a b n (succ c)
end.
Fixpoint pred (a:T2) : option T2 :=
match a with zero ⇒ None
| gcons zero zero 0 zero ⇒ Some zero
| gcons zero zero (S n) zero ⇒
Some (gcons zero zero n zero)
| gcons a b n c ⇒ (match (pred c) with
Some c' ⇒ Some (gcons a b n c')
| None ⇒ None
end)
end.
Inductive lt_epsilon0 : T2 → Prop :=
zero_lt_e0 : lt_epsilon0 zero
| gcons_lt_e0 : ∀ b n c, lt_epsilon0 b →
lt_epsilon0 c →
lt_epsilon0 (gcons zero b n c).
Section on_length.
Open Scope nat_scope.
Fixpoint nbterms (t:T2) : nat :=
match t with zero ⇒ 0
| gcons a b n v ⇒ (S n) + nbterms v
end.
Fixpoint t2_length (t:T2) : nat :=
match t with zero ⇒ 0
| gcons a b n v ⇒
nbterms (gcons a b n v) +
2 × (Nat.max (t2_length a)
(Nat.max (t2_length b) (t2_length_aux v)))
end
with t2_length_aux (t:T2) : nat :=
match t with zero ⇒ 0
| gcons a b n v ⇒
Nat.max (t2_length a) (Nat.max (t2_length b) (t2_length_aux v))
end.
Lemma length_a : ∀ a b n v, t2_length a <
t2_length (gcons a b n v).
Lemma length_b : ∀ a b n v, t2_length b <
t2_length (gcons a b n v).
Lemma length_c : ∀ a b n v, t2_length v <
t2_length (gcons a b n v).
Lemma length_n : ∀ a b r n p, n < p →
t2_length (gcons a b n r) <
t2_length (gcons a b p r).
Lemma length_psi : ∀ a b n c,
t2_length [a, b] ≤ t2_length (gcons a b n c).
Lemma length_ab : ∀ a b,
t2_length a + t2_length b ≤ t2_length (gcons a b 0 zero).
Lemma length_abnc : ∀ a b n c,
t2_length a + t2_length b ≤ t2_length (gcons a b n c).
End on_length.