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 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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 : ∀ 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.