source: src/ASM/Util.ma @ 764

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

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

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