Library gamma0.Gamma0_length

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

Add LoadPath "../prelude".
Add LoadPath "../rpo".
Add LoadPath "../epsilon0".

Require Import Tools.
Require Import More_nat.
Require Import AccP.
Require Import Gamma0_prelude.
Set Implicit Arguments.

Section on_length.

 Open Scope nat_scope.


Fixpoint nbterms (t:T2) : nat :=
  match t with zero => 0
             | cons a b n v => (S n) + nbterms v
  end.

Fixpoint length (t:T2) : nat :=
  match t with zero => 0
             | cons a b n v =>
                 nbterms (cons a b n v) +
                  2 * (max (length a) (max (length b) (length_aux v)))
  end
with length_aux (t:T2) : nat :=
 match t with zero => 0
            | cons a b n v =>
               max (length a) (max (length b) (length_aux v))
 end.

Lemma length_a : forall a b n v, length a <
                                 length (cons a b n v).
Proof.
 simpl.
 intros; apply le_lt_n_Sm.
 match goal with
     [ |- ?a <= ?b + ?c + ?d] => rewrite (plus_comm (b + c) d) end.
 apply le_plus_trans.
 apply le_plus_trans.
 apply le_max_l.
Qed.

Lemma length_b : forall a b n v, length b <
                                 length (cons a b n v).
Proof.
 simpl.
 intros; apply le_lt_n_Sm.
 match goal with
  [ |- ?a <= ?b + ?c + ?d] => rewrite (plus_comm (b + c) d) end.
 apply le_plus_trans.
 apply le_plus_trans.
 eapply le_trans.
 2:eapply le_max_r.
 apply le_max_l.
Qed.

Lemma length_c : forall a b n v, length v <
                                    length (cons a b n v).
Proof.
 simpl.
 intros; apply le_lt_n_Sm.
 case v.
 simpl.
 auto with arith.
 intros.
 simpl (length (cons t t0 n0 t1)).
 simpl (nbterms (cons t t0 n0 t1)).
 match goal with
  [ |- ?a <= ?b + ?c + ?d] => rewrite <- (plus_assoc b c d) end.
 simpl (length_aux (cons t t0 n0 t1)).
 match goal with [ |- ?a <= ?b + ?c ] => assert (a <= c) end.
 pattern (max (length t) (max (length t0) (length_aux t1))).
 generalize (max (length t) (max (length t0) (length_aux t1))).
 intro n1.
 simpl.
 apply le_n_S.
 apply plus_le_compat_l.
 repeat rewrite plus_0_r.
 apply plus_le_compat;
 apply le_trans with (max (length b) n1);
 apply le_max_r.
 omega.
Qed.

Lemma length_n : forall a b r n p, n < p ->
                        length (cons a b n r) <
                        length (cons a b p r).
Proof.
 induction 1.
 simpl.
 auto with arith.
 simpl;auto with arith.
Qed.

Lemma length_psi : forall a b n c,
                      length [a, b] <= length (cons a b n c).
Proof.
 simpl.
 intros; apply le_lt_n_Sm.
 match goal with
    [ |- ?a <= ?b + ?c + ?d] => rewrite (plus_comm (b + c) d) end.
 apply le_plus_trans.
 replace (max (length b) 0) with (length b).
 repeat rewrite plus_0_r.
 apply plus_le_compat;
 apply max_le_regL;
 apply le_max_l.
 rewrite max_l;auto with arith.
Qed.

Lemma length_ab : forall a b, length a + length b <= length (cons a b 0 zero).
Proof.
 simpl.
 intros.
 repeat rewrite (max_l (length b) 0);auto with arith.
 case (le_lt_dec (length a) (length b)).
 intro;repeat rewrite max_r;auto.
 omega.
 intro;repeat rewrite max_l;auto.
 omega.
 auto with arith.
Qed.

Lemma length_abnc : forall a b n c,
   length a + length b <= length (cons a b n c).
Proof.
 intros.
 eapply Le.le_trans.
 eapply length_ab.
 apply length_psi.
Qed.

End on_length.