source: Deliverables/D3.3/id-lookup-branch/utilities/lists.ma @ 1102

Last change on this file since 1102 was 1102, checked in by campbell, 9 years ago

Tidy up branch

File size: 1.9 KB
Line 
1include "basics/list.ma".
2
3let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
4match l with
5[ nil ⇒ None ?
6| cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
7].
8
9let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
10match l with
11[ nil ⇒ True
12| cons h t ⇒ P h ∧ All A P t
13].
14
15lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
16#A #P #Q #H #l elim l normalize //
17#h #t #IH * /3/
18qed.
19
20let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
21match l with
22[ nil ⇒ false
23| cons h t ⇒ orb (p h) (exists A p t)
24].
25
26let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
27match l with
28[ nil ⇒ False
29| cons h t ⇒ (P h) ∨ (Exists A P t)
30].
31
32lemma Exists_append : ∀A,P,l1,l2.
33  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
34#A #P #l1 elim l1
35[ normalize /2/
36| #h #t #IH #l2 *
37  [ #H /3/
38  | #H cases (IH l2 H) /3/
39  ]
40] qed.
41
42lemma Exists_append_l : ∀A,P,l1,l2.
43  Exists A P l1 → Exists A P (l1@l2).
44#A #P #l1 #l2 elim l1
45[ *
46| #h #t #IH *
47  [ #H %1 @H
48  | #H %2 @IH @H
49  ]
50] qed.
51
52lemma Exists_append_r : ∀A,P,l1,l2.
53  Exists A P l2 → Exists A P (l1@l2).
54#A #P #l1 #l2 elim l1
55[ #H @H
56| #h #t #IH #H %2 @IH @H
57] qed.
58
59lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
60#A #P #l1 #x #l2 elim l1
61[ normalize #H %2 @H
62| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
63qed.
64
65lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
66#A #P #l1 #x #l2 #H elim l1
67[ %1 @H
68| #h #t #IH %2 @IH
69] qed.
70
71lemma Exists_map : ∀A,B,P,Q,f,l.
72Exists A P l →
73(∀a.P a → Q (f a)) →
74Exists B Q (map A B f l).
75#A #B #P #Q #f #l elim l //
76#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
77
78lemma map_append : ∀A,B,f,l1,l2.
79  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
80#A #B #f #l1 elim l1
81[ #l2 @refl
82| #h #t #IH #l2 normalize //
83] qed.
Note: See TracBrowser for help on using the repository browser.