(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                               List_of_A.v                                *)
(****************************************************************************)

(* G. Huet 1-9-95 *)
(* Similar to List.v from LISTS, but sharing Generic_decidable_ordering *)

Require Le.
Require Generic.

(* Some programs and results about lists *)

Inductive list : Set := nil : list | cons : A -> list -> list.

Fixpoint app [l:list]: list -> list :=
[x:list]Cases l of 
           nil  => x
        | (cons a rest)  => (cons a (app rest x))
        end.

Lemma app_nil_end : (l:list)l=(app l nil).
Proof. 
Induction l; Simpl; Auto.
Induction 1; Auto.
Qed.
Hint app_nil_end.

Lemma app_ass : (l,m,n: list)(app (app l m) n)=(app l (app m n)).
Proof. 
Intros l m n; Elim l; Simpl; Auto.
Induction 1; Auto.
Qed.
Hint app_ass.

Lemma ass_app : (l,m,n: list)(app l (app m n))=(app (app l m) n).
Proof. 
Auto.
Qed.
Hint ass_app.

Definition tail := [l:list] Cases l of nil => nil | (cons _ l) => l end.

Lemma nil_cons : (a:A)(m:list)~ nil=(cons a m).
Proof.
Intros; Discriminate.
Qed.

(****************************************)
(* Length of lists                      *)
(****************************************)

Fixpoint length [l:list]: nat := 
 Cases l of
   nil => O
 | (cons _ l) => (S (length l))
 end.

(******************************)
(* Length_order of lists      *)
(******************************)

Section length_order.
Definition lel [l,m:list](le (length l) (length m)).

Variables a,b:A.
Variables l,m,n:list.

Lemma lel_refl : (lel l l).
Proof. 
Unfold lel; Auto.
Qed.

Lemma lel_trans : (lel l m)->(lel m n)->(lel l n).
Proof. 
Unfold lel; Intros.
Apply le_trans with (length m); Auto.
Qed.

Lemma lel_cons_cons : (lel l m) -> (lel (cons a l) (cons b m)).
Proof. 
Unfold lel; Simpl; Auto.
Qed.

Lemma lel_cons : (lel l m) -> (lel l (cons b m)).
Proof. 
Unfold lel; Simpl; Auto.
Qed.

Lemma lel_tail : (lel (cons a l) (cons b m)) -> (lel l m).
Proof. 
Unfold lel; Simpl; Auto.
Qed.

Lemma lel_nil : (l':list)(lel l' nil) -> nil=l'.
Proof. 
Induction l'; Auto.
Intros a' y H H0.
Absurd (le (S (length y)) O); Auto.
Qed.
End length_order.

Hint lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons.

Fixpoint In [a:A; l:list] : Prop :=
  Cases l of 
     (cons b l) => <A>b=a \/ (In a l) 
  | _ => False 
  end.

Lemma in_eq : (a:A)(l:list)(In a (cons a l)).
Proof. 
Simpl; Auto.
Qed.
Hint in_eq.

Lemma in_cons : (a,b:A)(l:list)(In b l) -> (In b (cons a l)).
Proof. 
Simpl; Auto.
Qed.
Hint in_cons.

Lemma in_app_or : (l,m:list)(a:A)(In a (app l m)) -> ((In a l) \/ (In a m)).
Proof. 
Intros l m a.
Elim l; Simpl; Auto.
Intros a0 y H H0.
Elim H0; Auto.
Intro H1.
Elim (H H1); Auto.
Qed.
Immediate in_app_or.

Lemma in_or_app : (l,m:list)(a:A)((In a l) \/ (In a m)) -> (In a (app l m)).
Proof. 
Intros l m a.
Elim l; Simpl; Intro H.
Elim H; Auto; Intro H0.
Elim H0. (* subProof completed *)
Intros y H0 H1.
Elim H1; Auto 4.
Intro H2.
Elim H2; Auto.
Qed.
Hint in_or_app.

Definition incl [l,m:list](a:A)(In a l) -> (In a m).

Hint Unfold incl.

Lemma incl_refl : (l:list)(incl l l).
Proof. 
Auto.
Qed.
Hint incl_refl.

Lemma incl_tl : (a:A)(l,m:list)(incl l m)->(incl l (cons a m)).
Proof. 
Auto.
Qed.
Immediate incl_tl.

Lemma incl_tran : (l,m,n:list)(incl l m)->(incl m n)->(incl l n).
Proof. 
Auto.
Qed.

Lemma incl_appl : (l,m,n:list)(incl l n)->(incl l (app n m)).
Proof. 
Auto.
Qed.
Immediate incl_appl.

Lemma incl_appr : (l,m,n:list)(incl l n)->(incl l (app m n)).
Proof. 
Auto.
Qed.
Immediate incl_appr.

Lemma incl_cons : (a:A)(l,m:list)(In a m)->(incl l m)->(incl (cons a l) m).
Proof. 
Unfold incl; Simpl; Intros a l m H H0 a0 H1.
Elim H1.
Induction 1; Trivial.
Auto.
Qed.
Hint incl_cons.

Lemma incl_app : (l,m,n:list)(incl l n)->(incl m n)->(incl (app l m) n).
Proof. 
Unfold incl; Simpl; Intros l m n H H0 a H1.
Elim (in_app_or l m a); Auto.
Qed.
Hint incl_app.


(* $Id: List_of_A.v,v 1.4 1998/04/30 16:45:56 mohring Exp $ *)
