Library Coq.Lists.MonoList
THIS IS A OLD CONTRIB. IT IS NO LONGER MAINTAINED
Require Import Le.
Parameter List_Dom : Set.
Definition A := List_Dom.
Inductive list : Set :=
| nil : list
| cons : A -> list -> list.
Fixpoint app (l m:list) {struct l} : list :=
match l return list with
| nil => m
| cons a l1 => cons a (app l1 m)
end.
Lemma app_nil_end : forall l:list, l = app l nil.
Hint Resolve app_nil_end: list v62.
Lemma app_ass : forall l m n:list, app (app l m) n = app l (app m n).
Hint Resolve app_ass: list v62.
Lemma ass_app : forall l m n:list, app l (app m n) = app (app l m) n.
Hint Resolve ass_app: list v62.
Definition tail (l:list) : list :=
match l return list with
| cons _ m => m
| _ => nil
end.
Lemma nil_cons : forall (a:A) (m:list), nil <> cons a m.
Fixpoint length (l:list) : nat :=
match l return nat with
| cons _ m => S (length m)
| _ => 0
end.
Section length_order.
Definition lel (l m:list) := length l <= length m.
Hint Unfold lel: list.
Variables a b : A.
Variables l m n : list.
Lemma lel_refl : lel l l.
Lemma lel_trans : lel l m -> lel m n -> lel l n.
Lemma lel_cons_cons : lel l m -> lel (cons a l) (cons b m).
Lemma lel_cons : lel l m -> lel l (cons b m).
Lemma lel_tail : lel (cons a l) (cons b m) -> lel l m.
Lemma lel_nil : forall l':list, lel l' nil -> nil = l'.
End length_order.
Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: list
v62.
Fixpoint In (a:A) (l:list) {struct l} : Prop :=
match l with
| nil => False
| cons b m => b = a \/ In a m
end.
Lemma in_eq : forall (a:A) (l:list), In a (cons a l).
Hint Resolve in_eq: list v62.
Lemma in_cons : forall (a b:A) (l:list), In b l -> In b (cons a l).
Hint Resolve in_cons: list v62.
Lemma in_app_or : forall (l m:list) (a:A), In a (app l m) -> In a l \/ In a m.
Hint Immediate in_app_or: list v62.
Lemma in_or_app : forall (l m:list) (a:A), In a l \/ In a m -> In a (app l m).
Hint Resolve in_or_app: list v62.
Definition incl (l m:list) := forall a:A, In a l -> In a m.
Hint Unfold incl: list v62.
Lemma incl_refl : forall l:list, incl l l.
Hint Resolve incl_refl: list v62.
Lemma incl_tl : forall (a:A) (l m:list), incl l m -> incl l (cons a m).
Hint Immediate incl_tl: list v62.
Lemma incl_tran : forall l m n:list, incl l m -> incl m n -> incl l n.
Lemma incl_appl : forall l m n:list, incl l n -> incl l (app n m).
Hint Immediate incl_appl: list v62.
Lemma incl_appr : forall l m n:list, incl l n -> incl l (app m n).
Hint Immediate incl_appr: list v62.
Lemma incl_cons :
forall (a:A) (l m:list), In a m -> incl l m -> incl (cons a l) m.
Hint Resolve incl_cons: list v62.
Lemma incl_app : forall l m n:list, incl l n -> incl m n -> incl (app l m) n.
Hint Resolve incl_app: list v62.