-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathMyList.v
140 lines (101 loc) · 2.84 KB
/
MyList.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
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.