Library MyList
Require
Import
Le
.
Require
Import
Gt
.
Require
Export
List
.
Set
Implicit
Arguments
.
Unset
Strict
Implicit
.
Section
Listes
.
Variable
A
: Set
.
Let
List
:= list
A
.
Inductive
item
(x
: A
) : List
-> nat
-> Prop
:=
| item_hd
: forall
l
, item
x
(x
:: l
) 0
| item_tl
: forall
l
n
y
, item
x
l
n
-> item
x
(y
:: l
) (S
n
).
Lemma
fun_item
: forall
u
v
e
n
, item
u
e
n
-> item
v
e
n
-> u
= v
.
simple
induction
1; intros
.
inversion_clear
H0
; auto
.
inversion_clear
H2
; auto
.
Qed
.
Fixpoint
nth_def
(d
: A
) (l
: List
) (n
: nat
) {struct
l
} : A
:=
match
l
, n
with
| nil
, _
=> d
| x
:: _
, O
=> x
| _
:: tl
, S
k
=> nth_def
d
tl
k
end
.
Lemma
nth_sound
: forall
x
l
n
d
, item
x
l
n
-> nth_def
d
l
n
= x
.
simple
induction
1; simpl
in
|- *; auto
.
Qed
.
Lemma
inv_nth_nl
: forall
x
n
, ~ item
x
nil
n
.
unfold
not
in
|- *; intros
.
inversion_clear
H
.
Qed
.
Lemma
inv_nth_cs
: forall
x
y
l
n
, item
x
(y
:: l
) (S
n
) -> item
x
l
n
.
intros
.
inversion_clear
H
; auto
.
Qed
.
Inductive
insert
(x
: A
) : nat
-> List
-> List
-> Prop
:=
| insert_hd
: forall
l
, insert
x
0 l
(x
:: l
)
| insert_tl
:
forall
n
l
il
y
, insert
x
n
l
il
-> insert
x
(S
n
) (y
:: l
) (y
:: il
).
Inductive
trunc
: nat
-> List
-> List
-> Prop
:=
| trunc_O
: forall
e
, trunc
0 e
e
| trunc_S
: forall
k
e
f
x
, trunc
k
e
f
-> trunc
(S
k
) (x
:: e
) f
.
Hint
Constructors
trunc
: core
.
Lemma
item_trunc
:
forall
n
e
t
, item
t
e
n
-> exists
f
: _
, trunc
(S
n
) e
f
.
simple
induction
n
; intros
.
inversion_clear
H
.
exists
l
; auto
.
inversion_clear
H0
.
elim
H
with
l
t
; intros
; auto
.
exists
x
; auto
.
Qed
.
Lemma
ins_le
:
forall
k
f
g
d
x
,
insert
x
k
f
g
-> forall
n
, k
<= n
-> nth_def
d
f
n
= nth_def
d
g
(S
n
).
simple
induction
1; auto
.
simple
destruct
n0
; intros
.
inversion_clear
H2
.
simpl
in
|- *; auto
with
arith
.
Qed
.
Lemma
ins_gt
:
forall
k
f
g
d
x
,
insert
x
k
f
g
-> forall
n
, k
> n
-> nth_def
d
f
n
= nth_def
d
g
n
.
simple
induction
1; auto
.
intros
.
inversion_clear
H0
.
simple
destruct
n0
; intros
.
auto
.
simpl
in
|- *; auto
with
arith
.
Qed
.
Lemma
ins_eq
: forall
k
f
g
d
x
, insert
x
k
f
g
-> nth_def
d
g
k
= x
.
simple
induction
1; simpl
in
|- *; auto
.
Qed
.
Lemma
list_item
:
forall
e
n
, {t
: _
| item
t
e
n
} + {forall
t
, ~ item
t
e
n
}.
fix
itemrec
1.
intros
e
n
.
case
e
; [ idtac
| intros
h
f
].
right
.
red
in
|- *; intros
.
inversion_clear
H
.
case
n
; [ idtac
| intros
k
].
left
.
exists
h
.
apply
item_hd
.
elim
(itemrec
f
k
).
intros
(t
, itm_t
).
left
; exists
t
.
apply
item_tl
; auto
.
intros
not_itm
.
right
; red
in
|- *; intros
.
elim
not_itm
with
t
.
inversion
H
; trivial
.
Defined
.
End
Listes
.
Hint
Constructors
item
: core
.
Hint
Constructors
insert
: core
.
Hint
Constructors
trunc
: core
.
Fixpoint
map
(A
B
: Set
) (f
: A
-> B
) (l
: list
A
) {struct
l
} : list
B
:=
match
l
with
| nil
=> nil
(A
:=B)
| x
:: t
=> f
x
:: map
f
t
end
.