source: src/utilities/lists.ma @ 1451

Last change on this file since 1451 was 1451, checked in by sacerdot, 8 years ago
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File size: 3.1 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
20lemma All_nth : ∀A,P,n,l.
21  All A P l →
22  ∀a.
23  nth_opt A n l = Some A a →
24  P a.
25#A #P #n elim n
26[ * [ #_ #a #E whd in E:(??%?); destruct
27    | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
28    ]
29| #m #IH *
30  [ #_ #a #E whd in E:(??%?); destruct
31  | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH
32  ]
33] qed.
34
35let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
36match l with
37[ nil ⇒ false
38| cons h t ⇒ orb (p h) (exists A p t)
39].
40
41let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
42match l with
43[ nil ⇒ False
44| cons h t ⇒ (P h) ∨ (Exists A P t)
45].
46
47lemma Exists_append : ∀A,P,l1,l2.
48  Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
49#A #P #l1 elim l1
50[ normalize /2/
51| #h #t #IH #l2 *
52  [ #H /3/
53  | #H cases (IH l2 H) /3/
54  ]
55] qed.
56
57lemma Exists_append_l : ∀A,P,l1,l2.
58  Exists A P l1 → Exists A P (l1@l2).
59#A #P #l1 #l2 elim l1
60[ *
61| #h #t #IH *
62  [ #H %1 @H
63  | #H %2 @IH @H
64  ]
65] qed.
66
67lemma Exists_append_r : ∀A,P,l1,l2.
68  Exists A P l2 → Exists A P (l1@l2).
69#A #P #l1 #l2 elim l1
70[ #H @H
71| #h #t #IH #H %2 @IH @H
72] qed.
73
74lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
75#A #P #l1 #x #l2 elim l1
76[ normalize #H %2 @H
77| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
78qed.
79
80lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
81#A #P #l1 #x #l2 #H elim l1
82[ %1 @H
83| #h #t #IH %2 @IH
84] qed.
85
86lemma Exists_map : ∀A,B,P,Q,f,l.
87Exists A P l →
88(∀a.P a → Q (f a)) →
89Exists B Q (map A B f l).
90#A #B #P #Q #f #l elim l //
91#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
92
93lemma Exists_exists : ∀A,P,l.
94  Exists A P l →
95  ∃x. P x.
96#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
97qed.
98
99lemma Exists_All : ∀A,P,Q,l.
100  Exists A P l →
101  All A Q l →
102  ∃x. P x ∧ Q x.
103#A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
104qed.
105
106lemma map_append : ∀A,B,f,l1,l2.
107  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
108#A #B #f #l1 elim l1
109[ #l2 @refl
110| #h #t #IH #l2 normalize //
111] qed.
112
113let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
114match l with
115[ nil ⇒ None B
116| cons h t ⇒
117    match f h with
118    [ None ⇒ find A B f t
119    | Some b ⇒ Some B b
120    ]
121].
122
123let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
124match l with
125[ nil ⇒ None ?
126| cons h t ⇒
127   match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
128
129definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
130 λA,found,l. position_of_aux A found l 0.
Note: See TracBrowser for help on using the repository browser.