source: src/ASM/Util.ma @ 712

Last change on this file since 712 was 712, checked in by mulligan, 9 years ago

Changes to get things to typecheck.

File size: 5.0 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   
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
45lemma eq_rect_Type0_r :
46  ∀A: Type[0].
47  ∀a:A.
48  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
49  #A #a #P #H #x #p
50  generalize in match H
51  generalize in match P
52  cases p
53  //
54qed.
55
56
57notation "hvbox(t⌈o ↦ h⌉)"
58  with precedence 45
59  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
60
61definition function_apply ≝
62  λA, B: Type[0].
63  λf: A → B.
64  λa: A.
65    f a.
66   
67notation "f break $ x"
68  left associative with precedence 99
69  for @{ 'function_apply $f $x }.
70 
71interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
72
73let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
74  match n with
75    [ O ⇒ a
76    | S o ⇒ f (iterate A f a o)
77    ].
78   
79notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
80 with precedence 10
81for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
82
83notation "⊥" with precedence 90
84  for @{ match ? in False with [ ] }.
85
86let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
87  match b with
88    [ true ⇒
89      match c with
90        [ false ⇒ true
91        | true ⇒ false
92        ]
93    | false ⇒
94      match c with
95        [ false ⇒ false
96        | true ⇒ true
97        ]
98    ].
99   
100definition ltb ≝
101  λm, n: nat.
102    leb (S m) n.
103   
104definition geb ≝
105  λm, n: nat.
106    ltb n m.
107
108definition gtb ≝
109  λm, n: nat.
110    leb n m.
111
112(* dpm: conflicts with library definitions
113interpretation "Nat less than" 'lt m n = (ltb m n).
114interpretation "Nat greater than" 'gt m n = (gtb m n).
115interpretation "Nat greater than eq" 'geq m n = (geb m n).
116*)
117
118let rec division_aux (m: nat) (n : nat) (p: nat) ≝
119  match ltb n (S p) with
120    [ true ⇒ O
121    | false ⇒
122      match m with
123        [ O ⇒ O
124        | (S q) ⇒ S (division_aux q (n - (S p)) p)
125        ]
126    ].
127   
128definition division ≝
129  λm, n: nat.
130    match n with
131      [ O ⇒ S m
132      | S o ⇒ division_aux m m o
133      ].
134     
135notation "hvbox(n break ÷ m)"
136  right associative with precedence 47
137  for @{ 'division $n $m }.
138 
139interpretation "Nat division" 'division n m = (division n m).
140
141let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
142  match leb n p with
143    [ true ⇒ n
144    | false ⇒
145      match m with
146        [ O ⇒ n
147        | S o ⇒ modulus_aux o (n - (S p)) p
148        ]
149    ].
150   
151definition modulus ≝
152  λm, n: nat.
153    match n with
154      [ O ⇒ m
155      | S o ⇒ modulus_aux m m o
156      ].
157   
158notation "hvbox(n break 'mod' m)"
159  right associative with precedence 47
160  for @{ 'modulus $n $m }.
161 
162interpretation "Nat modulus" 'modulus m n = (modulus m n).
163
164definition divide_with_remainder ≝
165  λm, n: nat.
166    pair ? ? (m ÷ n) (modulus m n).
167   
168let rec exponential (m: nat) (n: nat) on n ≝
169  match n with
170    [ O ⇒ S O
171    | S o ⇒ m * exponential m o
172    ].
173
174interpretation "Nat exponential" 'exp n m = (exponential n m).
175   
176notation "hvbox(a break ⊎ b)"
177 left associative with precedence 50
178for @{ 'disjoint_union $a $b }.
179interpretation "sum" 'disjoint_union A B = (Sum A B).
180
181theorem less_than_or_equal_monotone:
182  ∀m, n: nat.
183    m ≤ n → (S m) ≤ (S n).
184 #m #n #H
185 elim H
186 /2/
187qed.
188
189theorem less_than_or_equal_b_complete:
190  ∀m, n: nat.
191    leb m n = false → ¬(m ≤ n).
192 #m;
193 elim m;
194 normalize
195 [ #n #H
196   destruct
197 | #y #H1 #z
198   cases z
199   normalize
200   [ #H
201     /2/
202   | /3/
203   ]
204 ]
205qed.
206
207theorem less_than_or_equal_b_correct:
208  ∀m, n: nat.
209    leb m n = true → m ≤ n.
210 #m
211 elim m
212 //
213 #y #H1 #z
214 cases z
215 normalize
216 [ #H
217   destruct
218 | #n #H lapply (H1 … H) /2/
219 ]
220qed.
221
222definition less_than_or_equal_b_elim:
223 ∀m, n: nat.
224 ∀P: bool → Type[0].
225   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
226 #m #n #P #H1 #H2;
227 lapply (less_than_or_equal_b_correct m n)
228 lapply (less_than_or_equal_b_complete m n)
229 cases (leb m n)
230 /3/
231qed.
Note: See TracBrowser for help on using the repository browser.