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.