Skip to content

Commit 091a455

Browse files
klinashkaklinashka
committed
Facts about Lists.
1 parent 22584fd commit 091a455

File tree

4 files changed

+339
-1
lines changed

4 files changed

+339
-1
lines changed

‎code/Decidability/DiscreteTypes.v‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,52 @@ Section EqualityDeciders.
9898
Qed.
9999
End EqualityDeciders.
100100

101+
Section ClosureProperties.
102+
103+
Lemma isdeceqdirprod (X : UU) (Y : UU) : (isdeceq X) → (isdeceq Y) → (isdeceq (X × Y)).
104+
Proof.
105+
intros isdx isdy [x1 x2] [y1 y2].
106+
induction (isdx x1 y1), (isdy x2 y2).
107+
- left.
108+
exact (pathsdirprod a p).
109+
- right; intros b.
110+
apply n.
111+
exact (maponpaths dirprod_pr2 b).
112+
- right; intros n.
113+
apply b.
114+
exact (maponpaths dirprod_pr1 n).
115+
- right; intros c.
116+
apply b.
117+
exact (maponpaths dirprod_pr1 c).
118+
Qed.
119+
120+
Lemma isdeceqcoprod (X : UU) (Y : UU) : (isdeceq X) → (isdeceq Y) → (isdeceq (X ⨿ Y)).
121+
Proof.
122+
intros isdx isdy [x | x] [y | y].
123+
- induction (isdx x y).
124+
+ left.
125+
exact (maponpaths inl a).
126+
+ right. intros inl.
127+
apply b.
128+
use ii1_injectivity.
129+
* exact Y.
130+
* exact inl.
131+
- exact (ii2 (@negpathsii1ii2 X Y x y)).
132+
- exact (ii2 (@negpathsii2ii1 X Y y x)).
133+
- induction (isdy x y).
134+
+ exact (ii1 (maponpaths inr a)).
135+
+ right; intros inr; apply b.
136+
use ii2_injectivity.
137+
* exact X.
138+
* exact inr.
139+
Qed.
140+
141+
142+
143+
144+
End ClosureProperties.
145+
146+
101147
Section ChoiceFunction.
102148

103149
End ChoiceFunction.

‎code/Inductive/ListProperties.v‎

Lines changed: 277 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,277 @@
1+
Require Import init.imports.
2+
Require Import UniMath.Combinatorics.Lists.
3+
4+
Section Definitions.
5+
6+
Definition is_in {X : UU} (x : X) : (list X) → UU.
7+
Proof.
8+
use list_ind.
9+
- exact empty.
10+
- intros.
11+
exact (X0 ⨿ (x = x0)).
12+
Defined.
13+
14+
Definition hin {X : UU} (x : X) : (list X) → hProp := (λ l : (list X), ∥is_in x l∥).
15+
16+
Section Tests.
17+
18+
Definition l : list nat := (cons 1 (cons 2 (cons 3 (nil)))).
19+
20+
Lemma test1In : (is_in 1 l).
21+
Proof.
22+
right; apply idpath.
23+
Qed.
24+
25+
Lemma negtest4In : ¬ (is_in 4 (cons 1 nil)).
26+
Proof.
27+
intros [a | b].
28+
- exact a.
29+
- apply (negpathssx0 2).
30+
apply invmaponpathsS.
31+
exact b.
32+
Qed.
33+
End Tests.
34+
35+
End Definitions.
36+
37+
Section Length.
38+
(*Lemmas related to the length of the list*)
39+
40+
Lemma length_zero_nil {X : UU} (l : list X) (eq : 0 = length l) : l = nil.
41+
Proof.
42+
revert l eq.
43+
use list_ind.
44+
- exact (λ x, (idpath nil)).
45+
- intros x xs Ih eq.
46+
apply fromempty.
47+
apply (negpaths0sx (length xs) eq).
48+
Qed.
49+
50+
Lemma length_cons {X : UU} (l : list X) (inq : 0 < length l) : ∑ (x0 : X) (l2 : list X), l = (cons x0 l2).
51+
revert l inq.
52+
use list_ind.
53+
- intros inq.
54+
exact (fromempty (isirreflnatlth 0 inq)).
55+
- intros x xs Ih ineq.
56+
exact (x,, (xs,, (idpath (cons x xs)))).
57+
Qed.
58+
59+
Lemma length_in {X : UU} (l : list X) (x : X) (inn : is_in x l) : 0 < length l.
60+
Proof.
61+
revert l inn.
62+
use list_ind.
63+
- intros inn. apply fromempty. exact inn.
64+
- cbv beta. intros.
65+
apply idpath.
66+
Qed.
67+
68+
End Length.
69+
70+
71+
Section DistinctList.
72+
73+
Definition distinctterms {X : UU} : (list X) → UU.
74+
Proof.
75+
use list_ind.
76+
- exact unit.
77+
- intros.
78+
exact (X0 × ¬(is_in x xs)).
79+
Defined.
80+
81+
Definition hdistinct {X : UU} : (list X) → hProp := (λ l : (list X), ∥distinctterms l∥).
82+
83+
End DistinctList.
84+
85+
Section Filter.
86+
87+
Definition filter_ex_fun {X : UU} (d : isdeceq X) (x : X) : X → list X → list X.
88+
Proof.
89+
intros x0 l1.
90+
induction (d x x0).
91+
- exact l1.
92+
- exact (cons x0 l1).
93+
Defined.
94+
95+
Definition filter_ex {X : UU} (d : isdeceq X) (x : X) (l : list X) : list X :=
96+
(@foldr X (list X) (filter_ex_fun d x) nil l).
97+
98+
Definition filter_ex_nil {X : UU} (d : isdeceq X) (x : X) (l : list X) : (filter_ex d x nil) = nil.
99+
Proof.
100+
apply idpath.
101+
Qed.
102+
103+
104+
Definition filter_ex_cons1 {X : UU} (d : isdeceq X) (x : X) (l : list X) : (filter_ex d x (cons x l)) = (filter_ex d x l).
105+
Proof.
106+
set (q:= foldr_cons (filter_ex_fun d x) nil x l).
107+
unfold filter_ex; induction (pathsinv0 q).
108+
unfold filter_ex_fun; induction (d x x).
109+
- apply idpath.
110+
- apply fromempty, b, idpath.
111+
Defined.
112+
113+
Definition filter_ex_cons2 {X : UU} (d : isdeceq X) (x x0 : X) (l : list X) (nin : ¬ (x = x0)) : (filter_ex d x (cons x0 l)) = cons x0 (filter_ex d x l).
114+
Proof.
115+
set (q := foldr_cons (filter_ex_fun d x) nil x0 l).
116+
unfold filter_ex; induction (pathsinv0 q).
117+
unfold filter_ex_fun; induction (d x x0).
118+
- apply fromempty, nin, a.
119+
- apply idpath.
120+
Defined.
121+
122+
Lemma xninfilter_ex {X : UU} (d : isdeceq X) (x : X) (l : list X) : ¬ is_in x (filter_ex d x l).
123+
Proof.
124+
revert l.
125+
use list_ind.
126+
- intros is_in.
127+
exact is_in.
128+
- cbv beta.
129+
intros x0 xs Ih.
130+
induction (d x x0).
131+
+ induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)). exact Ih.
132+
+ induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)). intros [lst | elm].
133+
* exact (Ih lst).
134+
* exact (b elm).
135+
Defined.
136+
137+
Lemma filter_exltlist1 {X : UU} (d : isdeceq X) (x : X) (l : list X) : (length (filter_ex d x l)) ≤ (length l).
138+
Proof.
139+
revert l.
140+
use list_ind.
141+
- use isreflnatleh.
142+
- cbv beta. intros x0 xs Ih.
143+
induction (d x x0).
144+
+ induction a.
145+
induction (pathsinv0 (filter_ex_cons1 d x xs)).
146+
apply natlehtolehs; exact Ih.
147+
+ induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)).
148+
exact Ih.
149+
Qed.
150+
151+
Lemma istransnatlth {n m k : nat} : n < m → (m < k) → (n < k).
152+
Proof.
153+
intros inq1 inq2.
154+
apply (istransnatgth k m n).
155+
- exact inq2.
156+
- exact inq1.
157+
Qed.
158+
159+
Lemma natlthnsnmtonm {n m : nat} : (S n < m) → (n < m).
160+
Proof.
161+
intros.
162+
exact (istransnatlth (natlthnsn n) X).
163+
Qed.
164+
165+
Lemma filter_exltlist2 {X : UU} (d : isdeceq X) (x : X) (l : list X) (inn : is_in x l) : (length (filter_ex d x l)) < (length l).
166+
Proof.
167+
revert l inn.
168+
use list_ind; cbv beta.
169+
- intros. apply fromempty. exact inn.
170+
- intros x0 xs Ih inn.
171+
destruct inn as [in' | elm].
172+
+ set (q := (Ih in')).
173+
induction (d x x0).
174+
* induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)).
175+
apply natlthtolths. exact q.
176+
* induction (pathsinv0 (filter_ex_cons2 d x x0 xs b)).
177+
exact q.
178+
+ induction (pathsinv0 elm).
179+
set (ineq := (filter_exltlist1 d x0 xs)).
180+
induction (pathsinv0 (filter_ex_cons1 d x0 xs)).
181+
apply natlehtolthsn.
182+
exact ineq.
183+
Qed.
184+
185+
Lemma filter_ex_in {X : UU} (d : isdeceq X) (l : list X) (x x0 : X) (neq : ¬ (x = x0)) : (is_in x0 l) → (is_in x0 (filter_ex d x l)).
186+
Proof.
187+
revert l.
188+
use list_ind; cbv beta.
189+
- intros nn. apply fromempty. exact nn.
190+
- intros.
191+
induction (d x x1).
192+
+ induction a. induction (pathsinv0 (filter_ex_cons1 d x xs)).
193+
destruct X1 as [a | b].
194+
* exact (X0 a).
195+
* apply fromempty, neq. exact (pathsinv0 b).
196+
+ induction (pathsinv0 (filter_ex_cons2 d x x1 xs b)).
197+
destruct X1 as [a | c].
198+
* left.
199+
exact (X0 a).
200+
* induction (pathsinv0 c).
201+
right. apply idpath.
202+
Qed.
203+
204+
End Filter.
205+
206+
207+
208+
Section Properties.
209+
210+
Lemma eqdecidertomembdecider {X : UU} (d : ∏ (x1 x2 : X), decidable(x1=x2)) : ∏ (x : X) (l : list X), decidable (is_in x l).
211+
Proof.
212+
intros x.
213+
use list_ind.
214+
- right; intros inn. exact inn.
215+
- intros x0 xs dec.
216+
induction dec.
217+
+ left; left. exact a.
218+
+ induction (d x x0).
219+
* left; right. exact a.
220+
* right. intros [a | a'].
221+
-- apply b. exact a.
222+
-- apply b0. exact a'.
223+
Defined.
224+
225+
(* An induction principle for lists with distinct terms. *)
226+
Lemma distinct_list_induction {X : UU} : ∏ (P : list X → UU),
227+
(P nil) → (∏ (x : X) (xs : (list X)) (d : (distinctterms xs)), (P xs) → ¬(is_in x xs) → (P (cons x xs))) → ∏ (xs : list X) (d : distinctterms xs), (P xs).
228+
Proof.
229+
intros P Pnil Ih.
230+
use list_ind.
231+
- exact (λ d : _, Pnil).
232+
- intros x xs X0 d.
233+
destruct d as [d inn].
234+
apply Ih.
235+
+ exact d.
236+
+ exact (X0 d).
237+
+ exact inn.
238+
Defined.
239+
240+
Lemma pigeonhole_sigma {X : UU} (l1 l2 : list X) (d : ∏ (x1 x2 : X), (decidable (x1=x2))) (dist : distinctterms l2) : (length l1) < (length l2) → (∑ (x : X), (is_in x l2) × (¬ (is_in x l1))).
241+
Proof.
242+
revert l2 dist l1.
243+
use distinct_list_induction.
244+
- intros l1 ineq.
245+
apply fromempty.
246+
exact (negnatlthn0 (length l1) ineq).
247+
- cbn beta; intros x xs dt Ih nin.
248+
intros l1 ineq.
249+
induction (eqdecidertomembdecider d x l1).
250+
+ set (l' := filter_ex d x l1).
251+
assert (length l' < length xs).
252+
* apply (natlthlehtrans (length l') (length l1) (length xs)).
253+
-- exact (filter_exltlist2 d x l1 a).
254+
-- apply natlthsntoleh. exact ineq.
255+
* set (pr := (Ih l' X0)).
256+
destruct pr as [x0 [ixs il']].
257+
use tpair.
258+
-- exact x0.
259+
-- split.
260+
left.
261+
++ exact ixs.
262+
++ intros il1.
263+
apply il', filter_ex_in.
264+
** intros eq.
265+
induction eq.
266+
exact (nin ixs).
267+
** exact il1.
268+
+ use tpair.
269+
* exact x.
270+
* split.
271+
-- right. apply idpath.
272+
-- exact b.
273+
Qed.
274+
275+
276+
277+
End Properties.

‎code/Inductive/Option.v‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
(* Definition of an option as the coproduct of a type X with the unit type *)
2+
3+
Require Import init.imports.
4+
5+
Section Option.
6+
7+
Definition option {X : UU} : UU := X ⨿ unit.
8+
9+
Definition some {X : UU} (x : X) : option := (ii1 x).
10+
Definition none {X : UU} : @option X := (ii2 tt).
11+
12+
End Option.

‎code/_CoqProject‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,14 @@ COQC = coqc
22
COQDEP = coqdep
33
-R . "sem"
44

5-
-arg "-w -notation-overridden -type-in-type"
5+
-arg "-w -notation-overridden -type-in-type -noinit"
66

77
init/imports.v
88
init/all.v
99

10+
Inductive/ListProperties.v
11+
Inductive/Option.v
12+
1013
Decidability/DecidablePredicates.v
1114
Decidability/DiscreteTypes.v
1215

0 commit comments

Comments
 (0)