Library Lambda.MyList
Require
Import
Le
.
Require
Import
Gt
.
Require
Export
List
.
Section
Listes
.
Variable
A
: Set
.
Let
List
:= list
A
.
Inductive
In
(x
: A
) : List
→ Prop
:=
| In_hd
: ∀ l
: List
, In
x
(x
:: l
)
| In_tl
: ∀ (y
: A
) (l
: List
), In
x
l
→ In
x
(y
:: l
).
Hint
Resolve
In_hd
In_tl
: coc
.
Lemma
In_app
:
∀ (x
: A
) (l1
l2
: List
), In
x
(l1
++ l2
) → In
x
l1
∨ In
x
l2
.
Definition
incl
(l1
l2
: List
) : Prop
:= ∀ x
: A
, In
x
l1
→ In
x
l2
.
Hint
Unfold
incl
: coc
.
Lemma
incl_app_sym
: ∀ l1
l2
: List
, incl
(l1
++ l2
) (l2
++ l1
).
Inductive
item
(x
: A
) : List
→ nat
→ Prop
:=
| item_hd
: ∀ l
: List
, item
x
(x
:: l
) 0
| item_tl
:
∀ (l
: List
) (n
: nat
) (y
: A
),
item
x
l
n
→ item
x
(y
:: l
) (S
n
).
Lemma
fun_item
:
∀ (u
v
: A
) (e
: List
) (n
: nat
), item
u
e
n
→ item
v
e
n
→ u
= v
.
Fixpoint
nth_def
(d
: A
) (l
: List
) {struct
l
} :
nat
→ A
:=
fun
n
: nat
⇒
match
l
, n
with
| nil
, _
⇒ d
| x
:: _
, O
⇒ x
| _
:: tl
, S
k
⇒ nth_def
d
tl
k
end
.
Lemma
nth_sound
:
∀ (x
: A
) (l
: List
) (n
: nat
),
item
x
l
n
→ ∀ d
: A
, nth_def
d
l
n
= x
.
Lemma
inv_nth_nl
: ∀ (x
: A
) (n
: nat
), ¬ item
x
nil
n
.
Lemma
inv_nth_cs
:
∀ (x
y
: A
) (l
: List
) (n
: nat
), item
x
(y
:: l
) (S
n
) → item
x
l
n
.
Inductive
insert
(x
: A
) : nat
→ List
→ List
→ Prop
:=
| insert_hd
: ∀ l
: List
, insert
x
0 l
(x
:: l
)
| insert_tl
:
∀ (n
: nat
) (l
il
: List
) (y
: A
),
insert
x
n
l
il
→ insert
x
(S
n
) (y
:: l
) (y
:: il
).
Inductive
trunc
: nat
→ List
→ List
→ Prop
:=
| trunc_O
: ∀ e
: List
, trunc
0 e
e
| trunc_S
:
∀ (k
: nat
) (e
f
: List
) (x
: A
),
trunc
k
e
f
→ trunc
(S
k
) (x
:: e
) f
.
Hint
Resolve
trunc_O
trunc_S
: coc
.
Lemma
item_trunc
:
∀ (n
: nat
) (e
: List
) (t
: A
),
item
t
e
n
→ ∃ f
: List
, trunc
(S
n
) e
f
.
Lemma
ins_le
:
∀ (k
: nat
) (f
g
: List
) (d
x
: A
),
insert
x
k
f
g
→
∀ n
: nat
, k
≤ n
→ nth_def
d
f
n
= nth_def
d
g
(S
n
).
Lemma
ins_gt
:
∀ (k
: nat
) (f
g
: List
) (d
x
: A
),
insert
x
k
f
g
→ ∀ n
: nat
, k
> n
→ nth_def
d
f
n
= nth_def
d
g
n
.
Lemma
ins_eq
:
∀ (k
: nat
) (f
g
: List
) (d
x
: A
),
insert
x
k
f
g
→ nth_def
d
g
k
= x
.
Lemma
list_item
:
∀ (e
: List
) (n
: nat
),
{t
: A
| item
t
e
n
} + {(∀ t
: A
, ¬ item
t
e
n
)}.
Definition
list_disjoint
(l1
l2
: List
) : Prop
:=
∀ x
: A
, In
x
l1
→ In
x
l2
→ False
.
Inductive
first_item
(x
: A
) : List
→ nat
→ Prop
:=
| fit_hd
: ∀ l
: List
, first_item
x
(x
:: l
) 0
| fit_tl
:
∀ (l
: List
) (y
: A
) (n
: nat
),
first_item
x
l
n
→ x
≠ y
→ first_item
x
(y
:: l
) (S
n
).
Hint
Resolve
fit_hd
fit_tl
: coc
.
Lemma
first_item_is_item
:
∀ (x
: A
) (l
: List
) (n
: nat
), first_item
x
l
n
→ item
x
l
n
.
Lemma
first_item_unique
:
∀ (x
: A
) (l
: List
) (n
: nat
),
first_item
x
l
n
→ ∀ m
: nat
, first_item
x
l
m
→ m
= n
.
Hypothesis
eq_dec
: ∀ x
y
: A
, {x
= y
} + {x
≠ y
}.
Lemma
list_index
:
∀ (x
: A
) (l
: List
), {n
: nat
| first_item
x
l
n
} + {¬ In
x
l
}.
End
Listes
.
Hint
Resolve
item_hd
item_tl
insert_hd
insert_tl
trunc_O
trunc_S
: coc
.
Hint
Resolve
In_hd
In_tl
fit_hd
fit_tl
trunc_O
trunc_S
: coc
.
Hint
Unfold
incl
: coc
.