Skip to content

Commit 95c181f

Browse files
klinashkaklinashka
authored
Merge pull request #2 from UniMath/lists
Lists
2 parents 70b331f + 37eccfc commit 95c181f

File tree

5 files changed

+495
-57
lines changed

5 files changed

+495
-57
lines changed

‎code/Decidability/DiscreteTypes.v

Lines changed: 1 addition & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -141,57 +141,4 @@ Section ClosureProperties.
141141
* exact inr.
142142
Qed.
143143

144-
Definition nopathsnilcons {X : UU} (a : X) (l : list X) : ¬ (nil = (cons a l)).
145-
Proof.
146-
intros eq.
147-
set (P := (@list_ind X (λ _, UU) unit (λ _ _ _, empty))).
148-
exact (@transportf (list X) P nil (cons a l) eq tt).
149-
Qed.
150-
151-
Definition nopathsconsnil {X : UU} (a : X) (l : list X) : ¬ ((cons a l) = nil).
152-
Proof.
153-
intros eq.
154-
set (P := (@list_ind X (λ _, UU) empty (λ _ _ _, unit))).
155-
exact (@transportf (list X) P (cons a l) nil eq tt).
156-
Qed.
157-
158-
Lemma isdeceqlist (X : UU) : (isdeceq X) → (isdeceq (list X)).
159-
Proof.
160-
intros isdx.
161-
use list_ind; cbv beta.
162-
- use list_ind; cbv beta.
163-
+ left; apply idpath.
164-
+ intros. right.
165-
apply nopathsnilcons.
166-
- intros x xs Ih.
167-
use list_ind; cbv beta.
168-
+ right. apply nopathsconsnil.
169-
+ intros x0 xs0 deceq.
170-
induction (Ih xs0), (isdx x x0).
171-
* induction a, p.
172-
left. apply idpath.
173-
* right. intros eq.
174-
exact (n (cons_inj1 x x0 xs xs0 eq)).
175-
* right. intros eq.
176-
exact (b (cons_inj2 x x0 xs xs0 eq)).
177-
* right. intros eq.
178-
exact (b (cons_inj2 x x0 xs xs0 eq)).
179-
Qed.
180-
181-
Lemma isdeceqoption (X : UU) : (isdeceq X) → (isdeceq (@option X)).
182-
Proof.
183-
intros isdx.
184-
intros o1 o2.
185-
induction o1, o2.
186-
- induction (isdx a x).
187-
+ induction a0. left. apply idpath.
188-
+ right. intros eq. apply b, some_injectivity. exact eq.
189-
- right. induction u. apply nopathssomenone.
190-
- right; induction b. apply nopathsnonesome.
191-
- left; induction u, b. apply idpath.
192-
Qed.
193-
End ClosureProperties.
194-
195-
Section ChoiceFunction.
196-
197-
End ChoiceFunction.
144+
End ClosureProperties.

‎code/Inductive/ListProperties.v

Lines changed: 274 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,274 @@
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+
End Properties.

‎code/Inductive/Option.v

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
2+
(* Definition of an option as the coproduct of a type X with the unit type *)
13
Require Import init.imports.
24

35
Section Option.
@@ -28,4 +30,3 @@ Section PathProperties.
2830

2931

3032
End PathProperties.
31-

0 commit comments

Comments
 (0)