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

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

Minimal integration of bitvectors into Clight semantics

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