source: src/ASM/Util.ma @ 704

Last change on this file since 704 was 704, checked in by sacerdot, 9 years ago

Minor speedup in one theorem (less automation).

File size: 5.1 KB
Line 
1include "arithmetics/nat.ma".
2include "basics/list.ma".
3include "basics/types.ma".
4
5let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
6  match l with
7  [ nil ⇒ a
8  | cons hd tl ⇒ foldl A B f (f a hd) tl
9  ].
10
11definition flatten ≝
12  λA: Type[0].
13  λl: list (list A).
14    foldl ? ? (append ?) [ ] l.
15
16definition if_then_else ≝
17  λA: Type[0].
18  λb: bool.
19  λt: A.
20  λf: A.
21  match b with
22  [ true ⇒ t
23  | false ⇒ f
24  ].
25   
26(*
27notation "hvbox('if' b 'then' t 'else' f)"
28  non associative with precedence 83
29  for @{ 'if_then_else $b $t $f }.
30*)
31notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
32notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
33
34interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
35
36let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
37                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
38  match l with
39    [ nil ⇒ x
40    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
41    ].
42
43definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
44
45let rec revapp (T:Type[0]) (l:list T) (r:list T) on l : list T ≝
46match l with
47[ nil ⇒ r
48| cons h t ⇒ revapp T t (h::r)
49].
50
51definition rev ≝ λT:Type[0].λl. revapp T l [ ].
52
53lemma eq_rect_Type0_r :
54  ∀A: Type[0].
55  ∀a:A.
56  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
57  #A #a #P #H #x #p
58  generalize in match H
59  generalize in match P
60  cases p
61  //
62qed.
63
64
65notation "hvbox(t⌈o ↦ h⌉)"
66  with precedence 45
67  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
68
69definition function_apply ≝
70  λA, B: Type[0].
71  λf: A → B.
72  λa: A.
73    f a.
74   
75notation "f break $ x"
76  left associative with precedence 99
77  for @{ 'function_apply $f $x }.
78 
79interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
80
81let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
82  match n with
83    [ O ⇒ a
84    | S o ⇒ f (iterate A f a o)
85    ].
86   
87notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
88 with precedence 10
89for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
90
91notation "⊥" with precedence 90
92  for @{ match ? in False with [ ] }.
93
94let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
95  match b with
96    [ true ⇒
97      match c with
98        [ false ⇒ true
99        | true ⇒ false
100        ]
101    | false ⇒
102      match c with
103        [ false ⇒ false
104        | true ⇒ true
105        ]
106    ].
107
108definition ltb ≝
109  λm, n: nat.
110    leb (S m) n.
111   
112definition geb ≝
113  λm, n: nat.
114    ltb n m.
115
116definition gtb ≝
117  λm, n: nat.
118    leb n m.
119
120interpretation "Nat less than" 'lt m n = (ltb m n).
121interpretation "Nat greater than" 'gt m n = (gtb m n).
122interpretation "Nat greater than eq" 'geq m n = (geb m n).
123
124let rec division_aux (m: nat) (n : nat) (p: nat) ≝
125  match ltb n (S p) with
126    [ true ⇒ O
127    | false ⇒
128      match m with
129        [ O ⇒ O
130        | (S q) ⇒ S (division_aux q (n - (S p)) p)
131        ]
132    ].
133   
134definition division ≝
135  λm, n: nat.
136    match n with
137      [ O ⇒ S m
138      | S o ⇒ division_aux m m o
139      ].
140     
141notation "hvbox(n break ÷ m)"
142  right associative with precedence 47
143  for @{ 'division $n $m }.
144 
145interpretation "Nat division" 'division n m = (division n m).
146
147let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
148  match leb n p with
149    [ true ⇒ n
150    | false ⇒
151      match m with
152        [ O ⇒ n
153        | S o ⇒ modulus_aux o (n - (S p)) p
154        ]
155    ].
156   
157definition modulus ≝
158  λm, n: nat.
159    match n with
160      [ O ⇒ m
161      | S o ⇒ modulus_aux m m o
162      ].
163   
164notation "hvbox(n break 'mod' m)"
165  right associative with precedence 47
166  for @{ 'modulus $n $m }.
167 
168interpretation "Nat modulus" 'modulus m n = (modulus m n).
169
170definition divide_with_remainder ≝
171  λm, n: nat.
172    pair ? ? (m ÷ n) (modulus m n).
173   
174let rec exponential (m: nat) (n: nat) on n ≝
175  match n with
176    [ O ⇒ S O
177    | S o ⇒ m * exponential m o
178    ].
179
180interpretation "Nat exponential" 'exp n m = (exponential n m).
181   
182notation "hvbox(a break ⊎ b)"
183 left associative with precedence 50
184for @{ 'disjoint_union $a $b }.
185interpretation "sum" 'disjoint_union A B = (Sum A B).
186
187theorem less_than_or_equal_monotone:
188  ∀m, n: nat.
189    m ≤ n → (S m) ≤ (S n).
190 #m #n #H
191 elim H
192 /2/
193qed.
194
195theorem less_than_or_equal_b_complete:
196  ∀m, n: nat.
197    leb m n = false → ¬(m ≤ n).
198 #m;
199 elim m;
200 normalize
201 [ #n #H
202   destruct
203 | #y #H1 #z
204   cases z
205   normalize
206   [ #H
207     /2/
208   | /3/
209   ]
210 ]
211qed.
212
213theorem less_than_or_equal_b_correct:
214  ∀m, n: nat.
215    leb m n = true → m ≤ n.
216 #m
217 elim m
218 //
219 #y #H1 #z
220 cases z
221 normalize
222 [ #H
223   destruct
224 | #n #H lapply (H1 … H) /2/
225 ]
226qed.
227
228definition less_than_or_equal_b_elim:
229 ∀m, n: nat.
230 ∀P: bool → Type[0].
231   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
232 #m #n #P #H1 #H2;
233 lapply (less_than_or_equal_b_correct m n)
234 lapply (less_than_or_equal_b_complete m n)
235 cases (leb m n)
236 /3/
237qed.
Note: See TracBrowser for help on using the repository browser.