Library Gamma0_prelude

Require Import Arith.
Require Import Omega. Require Import Compare_dec.
Require Import Relations.
Require Import Wellfounded.
Require Import Max.

Require Import Tools.
Require Import More_nat.
Require Import AccP.
Require Import not_decreasing.
Require Import EPSILON0.
Require Import More_nat.
Set Implicit Arguments.

Inductive T2 : Set :=
  zero : T2
| cons : T2 -> T2 -> nat -> T2 -> T2.

Definition psi alpha beta := cons alpha beta 0 zero.

Definition one := psi zero zero.

Definition finite p := match p with
                             0 => zero
                           | S q => cons zero zero q zero
                           end.

Notation "'F' n" := (finite n)(at level 29) : g0_scope.

Inductive is_finite: T2 -> Set :=
 zero_finite : is_finite zero
|succ_finite : forall n, is_finite (cons zero zero n zero).

Definition omega := psi zero one.

Definition epsilon0 := psi one zero.

Definition epsilon alpha := psi one alpha.

Fixpoint T1_inj (c:T1) : T2 :=
 match c with EPSILON0.zero => zero
            | EPSILON0.cons a n b => cons zero (T1_inj a) n (T1_inj b)
 end.

Inductive ap : T2 -> Prop :=
ap_intro : forall alpha beta, ap (cons alpha beta 0 zero).

Inductive lt : T2 -> T2 -> Prop :=
|  lt_1 : forall alpha beta n gamma, lt zero (cons alpha beta n gamma)
|  lt_2 : forall alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
               lt alpha1 alpha2 ->
               lt beta1 (cons alpha2 beta2 0 zero) ->
               lt (cons alpha1 beta1 n1 gamma1)
                  (cons alpha2 beta2 n2 gamma2)
|  lt_3 : forall alpha1 beta1 beta2 n1 n2 gamma1 gamma2,
               lt beta1 beta2 ->
               lt (cons alpha1 beta1 n1 gamma1)
                  (cons alpha1 beta2 n2 gamma2)

|  lt_4 : forall alpha1 alpha2 beta1 beta2 n1 n2 gamma1 gamma2,
               lt alpha2 alpha1 ->
               lt (cons alpha1 beta1 0 zero) beta2 ->
                  lt (cons alpha1 beta1 n1 gamma1)
                     (cons alpha2 beta2 n2 gamma2)

| lt_5 : forall alpha1 alpha2 beta1 n1 n2 gamma1 gamma2,
               lt alpha2 alpha1 ->
               lt (cons alpha1 beta1 n1 gamma1)
                  (cons alpha2 (cons alpha1 beta1 0 zero) n2 gamma2)

| lt_6 : forall alpha1 beta1 n1 n2 gamma1 gamma2, (n1 < n2)%nat ->
                                    lt (cons alpha1 beta1 n1 gamma1)
                                       (cons alpha1 beta1 n2 gamma2)

|   lt_7 : forall alpha1 beta1 n1 gamma1 gamma2, lt gamma1 gamma2 ->
                                    lt (cons alpha1 beta1 n1 gamma1)
                                       (cons alpha1 beta1 n1 gamma2).

Hint Constructors lt.

Notation "o1 < o2" := (lt o1 o2): g0_scope.

Open Scope g0_scope.

Definition le t t' := t = t' \/ t < t'.
Hint Unfold le.

Notation "o1 <= o2" := (le o1 o2): g0_scope.

Definition tail c := match c with | zero => zero
                                  | cons a b n c => c
                             end.
Inductive nf : T2 -> Prop :=
| zero_nf : nf zero
| single_nf : forall a b n, nf a -> nf b -> nf (cons a b n zero)
| cons_nf : forall a b n a' b' n' c',
                             psi a' b' < psi a b ->
                             nf a -> nf b ->
                             nf(cons a' b' n' c')->
                             nf(cons a b n (cons a' b' n' c')).
Hint Resolve zero_nf single_nf cons_nf .

Fixpoint succ (a:T2) : T2 :=
 match a with zero => finite 1
             | cons zero zero n c => finite (S (S n))
             | cons a b n c => cons a b n (succ c)
 end.

Fixpoint pred (a:T2) : option T2 :=
 match a with zero => None
             | cons zero zero 0 zero => Some zero
             | cons zero zero (S n) zero =>
                  Some (cons zero zero n zero)
             | cons a b n c => (match (pred c) with
                                   Some c' => Some (cons a b n c')
                                  | None => None
                                  end)
 end.

Inductive lt_epsilon0 : T2 -> Prop :=
  zero_lt_e0 : lt_epsilon0 zero
| cons_lt_e0 : forall b n c, lt_epsilon0 b ->
                                lt_epsilon0 c ->
                                lt_epsilon0 (cons zero b n c).

 

Index
This page has been generated by coqdoc