source: Deliverables/D3.1/C-semantics/cerco/Util.ma @ 534

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

Fix a couple of bugs with branched 4.1 stuff.

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