source: extracted/util.ml @ 2746

Last change on this file since 2746 was 2743, checked in by sacerdot, 7 years ago

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 21.0 KB
Line 
1open Preamble
2
3open Bool
4
5open Relations
6
7open Nat
8
9open Hints_declaration
10
11open Core_notation
12
13open Pts
14
15open Logic
16
17open Types
18
19open List
20
21open Jmeq
22
23open Russell
24
25type dAEMONXXX =
26| K1DAEMONXXX
27| K2DAEMONXXX
28
29(** val dAEMONXXX_rect_Type4 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
30let rec dAEMONXXX_rect_Type4 h_K1DAEMONXXX h_K2DAEMONXXX = function
31| K1DAEMONXXX -> h_K1DAEMONXXX
32| K2DAEMONXXX -> h_K2DAEMONXXX
33
34(** val dAEMONXXX_rect_Type5 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
35let rec dAEMONXXX_rect_Type5 h_K1DAEMONXXX h_K2DAEMONXXX = function
36| K1DAEMONXXX -> h_K1DAEMONXXX
37| K2DAEMONXXX -> h_K2DAEMONXXX
38
39(** val dAEMONXXX_rect_Type3 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
40let rec dAEMONXXX_rect_Type3 h_K1DAEMONXXX h_K2DAEMONXXX = function
41| K1DAEMONXXX -> h_K1DAEMONXXX
42| K2DAEMONXXX -> h_K2DAEMONXXX
43
44(** val dAEMONXXX_rect_Type2 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
45let rec dAEMONXXX_rect_Type2 h_K1DAEMONXXX h_K2DAEMONXXX = function
46| K1DAEMONXXX -> h_K1DAEMONXXX
47| K2DAEMONXXX -> h_K2DAEMONXXX
48
49(** val dAEMONXXX_rect_Type1 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
50let rec dAEMONXXX_rect_Type1 h_K1DAEMONXXX h_K2DAEMONXXX = function
51| K1DAEMONXXX -> h_K1DAEMONXXX
52| K2DAEMONXXX -> h_K2DAEMONXXX
53
54(** val dAEMONXXX_rect_Type0 : 'a1 -> 'a1 -> dAEMONXXX -> 'a1 **)
55let rec dAEMONXXX_rect_Type0 h_K1DAEMONXXX h_K2DAEMONXXX = function
56| K1DAEMONXXX -> h_K1DAEMONXXX
57| K2DAEMONXXX -> h_K2DAEMONXXX
58
59(** val dAEMONXXX_inv_rect_Type4 :
60    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
61let dAEMONXXX_inv_rect_Type4 hterm h1 h2 =
62  let hcut = dAEMONXXX_rect_Type4 h1 h2 hterm in hcut __
63
64(** val dAEMONXXX_inv_rect_Type3 :
65    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
66let dAEMONXXX_inv_rect_Type3 hterm h1 h2 =
67  let hcut = dAEMONXXX_rect_Type3 h1 h2 hterm in hcut __
68
69(** val dAEMONXXX_inv_rect_Type2 :
70    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
71let dAEMONXXX_inv_rect_Type2 hterm h1 h2 =
72  let hcut = dAEMONXXX_rect_Type2 h1 h2 hterm in hcut __
73
74(** val dAEMONXXX_inv_rect_Type1 :
75    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
76let dAEMONXXX_inv_rect_Type1 hterm h1 h2 =
77  let hcut = dAEMONXXX_rect_Type1 h1 h2 hterm in hcut __
78
79(** val dAEMONXXX_inv_rect_Type0 :
80    dAEMONXXX -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
81let dAEMONXXX_inv_rect_Type0 hterm h1 h2 =
82  let hcut = dAEMONXXX_rect_Type0 h1 h2 hterm in hcut __
83
84(** val dAEMONXXX_discr : dAEMONXXX -> dAEMONXXX -> __ **)
85let dAEMONXXX_discr x y =
86  Logic.eq_rect_Type2 x
87    (match x with
88     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
89     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
90
91(** val dAEMONXXX_jmdiscr : dAEMONXXX -> dAEMONXXX -> __ **)
92let dAEMONXXX_jmdiscr x y =
93  Logic.eq_rect_Type2 x
94    (match x with
95     | K1DAEMONXXX -> Obj.magic (fun _ dH -> dH)
96     | K2DAEMONXXX -> Obj.magic (fun _ dH -> dH)) y
97
98(** val ltb : Nat.nat -> Nat.nat -> Bool.bool **)
99let ltb m n =
100  Nat.leb (Nat.S m) n
101
102(** val geb : Nat.nat -> Nat.nat -> Bool.bool **)
103let geb m n =
104  Nat.leb n m
105
106(** val gtb : Nat.nat -> Nat.nat -> Bool.bool **)
107let gtb m n =
108  ltb n m
109
110(** val eq_nat : Nat.nat -> Nat.nat -> Bool.bool **)
111let rec eq_nat n m =
112  match n with
113  | Nat.O ->
114    (match m with
115     | Nat.O -> Bool.True
116     | Nat.S x -> Bool.False)
117  | Nat.S n' ->
118    (match m with
119     | Nat.O -> Bool.False
120     | Nat.S m' -> eq_nat n' m')
121
122(** val forall : ('a1 -> Bool.bool) -> 'a1 List.list -> Bool.bool **)
123let rec forall f = function
124| List.Nil -> Bool.True
125| List.Cons (hd0, tl) -> Bool.andb (f hd0) (forall f tl)
126
127(** val prefix : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
128let rec prefix k = function
129| List.Nil -> List.Nil
130| List.Cons (hd0, tl) ->
131  (match k with
132   | Nat.O -> List.Nil
133   | Nat.S k' -> List.Cons (hd0, (prefix k' tl)))
134
135(** val fold_left2 :
136    ('a1 -> 'a2 -> 'a3 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a3 List.list ->
137    'a1 **)
138let rec fold_left2 f accu left right =
139  (match left with
140   | List.Nil ->
141     (fun _ ->
142       (match right with
143        | List.Nil -> (fun _ -> accu)
144        | List.Cons (hd0, tl) ->
145          (fun _ ->
146            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
147   | List.Cons (hd0, tl) ->
148     (fun _ ->
149       (match right with
150        | List.Nil ->
151          (fun _ ->
152            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
153        | List.Cons (hd', tl') ->
154          (fun _ -> fold_left2 f (f accu hd0 hd') tl tl')) __)) __
155
156(** val remove_n_first_internal :
157    Nat.nat -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
158let rec remove_n_first_internal i l n =
159  match l with
160  | List.Nil -> List.Nil
161  | List.Cons (hd0, tl) ->
162    (match eq_nat i n with
163     | Bool.True -> l
164     | Bool.False -> remove_n_first_internal (Nat.S i) tl n)
165
166(** val remove_n_first : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
167let remove_n_first n l =
168  remove_n_first_internal Nat.O l n
169
170(** val foldi_from_until_internal :
171    Nat.nat -> 'a1 List.list -> 'a1 List.list -> Nat.nat -> (Nat.nat -> 'a1
172    List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list **)
173let rec foldi_from_until_internal i res rem m f =
174  match rem with
175  | List.Nil -> res
176  | List.Cons (e0, tl) ->
177    (match geb i m with
178     | Bool.True -> res
179     | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e0) tl m f)
180
181(** val foldi_from_until :
182    Nat.nat -> Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list)
183    -> 'a1 List.list -> 'a1 List.list -> 'a1 List.list **)
184let foldi_from_until n m f a l =
185  foldi_from_until_internal Nat.O a (remove_n_first n l) m f
186
187(** val foldi_from :
188    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
189    List.list -> 'a1 List.list -> 'a1 List.list **)
190let foldi_from n f a l =
191  foldi_from_until n (List.length l) f a l
192
193(** val foldi_until :
194    Nat.nat -> (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1
195    List.list -> 'a1 List.list -> 'a1 List.list **)
196let foldi_until m f a l =
197  foldi_from_until Nat.O m f a l
198
199(** val foldi :
200    (Nat.nat -> 'a1 List.list -> 'a1 -> 'a1 List.list) -> 'a1 List.list ->
201    'a1 List.list -> 'a1 List.list **)
202let foldi f a l =
203  foldi_from_until Nat.O (List.length l) f a l
204
205(** val hd_safe : 'a1 List.list -> 'a1 **)
206let hd_safe l =
207  (match l with
208   | List.Nil -> (fun _ -> assert false (* absurd case *))
209   | List.Cons (hd0, tl) -> (fun _ -> hd0)) __
210
211(** val tail_safe : 'a1 List.list -> 'a1 List.list **)
212let tail_safe l =
213  (match l with
214   | List.Nil -> (fun _ -> assert false (* absurd case *))
215   | List.Cons (hd0, tl) -> (fun _ -> tl)) __
216
217(** val safe_split :
218    'a1 List.list -> Nat.nat -> ('a1 List.list, 'a1 List.list) Types.prod **)
219let rec safe_split l index =
220  (match index with
221   | Nat.O -> (fun _ -> { Types.fst = List.Nil; Types.snd = l })
222   | Nat.S index' ->
223     (fun _ ->
224       (match l with
225        | List.Nil -> (fun _ -> assert false (* absurd case *))
226        | List.Cons (hd0, tl) ->
227          (fun _ ->
228            let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
229            { Types.fst = (List.Cons (hd0, l1)); Types.snd = l2 })) __)) __
230
231(** val nth_safe : Nat.nat -> 'a1 List.list -> 'a1 **)
232let rec nth_safe index the_list =
233  (match index with
234   | Nat.O ->
235     (match the_list with
236      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
237      | List.Cons (hd0, tl) -> (fun _ -> hd0))
238   | Nat.S index' ->
239     (match the_list with
240      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
241      | List.Cons (hd0, tl) -> (fun _ -> nth_safe index' tl))) __
242
243(** val last_safe : 'a1 List.list -> 'a1 **)
244let last_safe the_list =
245  nth_safe (Nat.minus (List.length the_list) (Nat.S Nat.O)) the_list
246
247(** val reduce :
248    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
249    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod **)
250let rec reduce left right =
251  match left with
252  | List.Nil ->
253    { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil }; Types.snd =
254      { Types.fst = List.Nil; Types.snd = right } }
255  | List.Cons (hd0, tl) ->
256    (match right with
257     | List.Nil ->
258       { Types.fst = { Types.fst = List.Nil; Types.snd = left }; Types.snd =
259         { Types.fst = List.Nil; Types.snd = List.Nil } }
260     | List.Cons (hd', tl') ->
261       let { Types.fst = cleft; Types.snd = cright } = reduce tl tl' in
262       let { Types.fst = commonl; Types.snd = restl } = cleft in
263       let { Types.fst = commonr; Types.snd = restr } = cright in
264       { Types.fst = { Types.fst = (List.Cons (hd0, commonl)); Types.snd =
265       restl }; Types.snd = { Types.fst = (List.Cons (hd', commonr));
266       Types.snd = restr } })
267
268(** val reduce_strong :
269    'a1 List.list -> 'a2 List.list -> (('a1 List.list, 'a1 List.list)
270    Types.prod, ('a2 List.list, 'a2 List.list) Types.prod) Types.prod
271    Types.sig0 **)
272let rec reduce_strong left right =
273  (match left with
274   | List.Nil ->
275     (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = List.Nil };
276       Types.snd = { Types.fst = List.Nil; Types.snd = right } })
277   | List.Cons (hd0, tl) ->
278     (fun _ ->
279       (match right with
280        | List.Nil ->
281          (fun _ -> { Types.fst = { Types.fst = List.Nil; Types.snd = left };
282            Types.snd = { Types.fst = List.Nil; Types.snd = List.Nil } })
283        | List.Cons (hd', tl') ->
284          (fun _ ->
285            (let { Types.fst = cleft; Types.snd = cright } =
286               Types.pi1 (reduce_strong tl tl')
287             in
288            (fun _ ->
289            (let { Types.fst = commonl; Types.snd = restl } = cleft in
290            (fun _ ->
291            (let { Types.fst = commonr; Types.snd = restr } = cright in
292            (fun _ -> { Types.fst = { Types.fst = (List.Cons (hd0, commonl));
293            Types.snd = restl }; Types.snd = { Types.fst = (List.Cons (hd',
294            commonr)); Types.snd = restr } })) __)) __)) __)) __)) __
295
296(** val map2_opt :
297    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list
298    Types.option **)
299let rec map2_opt f left right =
300  match left with
301  | List.Nil ->
302    (match right with
303     | List.Nil -> Types.Some List.Nil
304     | List.Cons (x, x0) -> Types.None)
305  | List.Cons (hd0, tl) ->
306    (match right with
307     | List.Nil -> Types.None
308     | List.Cons (hd', tl') ->
309       (match map2_opt f tl tl' with
310        | Types.None -> Types.None
311        | Types.Some tail0 -> Types.Some (List.Cons ((f hd0 hd'), tail0))))
312
313(** val map2 :
314    ('a1 -> 'a2 -> 'a3) -> 'a1 List.list -> 'a2 List.list -> 'a3 List.list **)
315let rec map2 f left right =
316  (match left with
317   | List.Nil ->
318     (match right with
319      | List.Nil -> (fun _ -> List.Nil)
320      | List.Cons (x, x0) ->
321        (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length x0)) __))
322   | List.Cons (hd0, tl) ->
323     (match right with
324      | List.Nil ->
325        (fun _ -> Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
326      | List.Cons (hd', tl') ->
327        (fun _ -> List.Cons ((f hd0 hd'), (map2 f tl tl'))))) __
328
329(** val map3 :
330    ('a1 -> 'a2 -> 'a3 -> 'a4) -> 'a1 List.list -> 'a2 List.list -> 'a3
331    List.list -> 'a4 List.list **)
332let rec map3 f left centre right =
333  (match left with
334   | List.Nil ->
335     (fun _ ->
336       (match centre with
337        | List.Nil ->
338          (fun _ ->
339            (match right with
340             | List.Nil -> (fun _ -> List.Nil)
341             | List.Cons (hd0, tl) ->
342               (fun _ ->
343                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
344              __)
345        | List.Cons (hd0, tl) ->
346          (fun _ ->
347            Logic.eq_rect_Type0 (List.length centre)
348              (Logic.eq_rect_Type0 (List.length List.Nil) (fun _ ->
349                Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
350                (List.length centre)) (List.length right) __)) __)
351   | List.Cons (hd0, tl) ->
352     (fun _ ->
353       (match centre with
354        | List.Nil ->
355          (fun _ ->
356            Logic.eq_rect_Type0 (List.length centre)
357              (Logic.eq_rect_Type0 (List.length (List.Cons (hd0, tl)))
358                (fun _ ->
359                Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)
360                (List.length centre)) (List.length right) __)
361        | List.Cons (hd', tl') ->
362          (fun _ ->
363            (match right with
364             | List.Nil ->
365               (fun _ _ ->
366                 Obj.magic Nat.nat_discr (Nat.S (List.length tl')) Nat.O __)
367             | List.Cons (hd'', tl'') ->
368               (fun _ _ -> List.Cons ((f hd0 hd' hd''),
369                 (map3 f tl tl' tl'')))) __ __)) __)) __
370
371(** val eq_rect_Type0_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
372let eq_rect_Type0_r0 a h x =
373  (fun _ auto -> auto) __ h
374
375(** val safe_nth : Nat.nat -> 'a1 List.list -> 'a1 **)
376let rec safe_nth n l =
377  (match n with
378   | Nat.O ->
379     (match l with
380      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
381      | List.Cons (hd0, tl) -> (fun _ -> hd0))
382   | Nat.S n' ->
383     (match l with
384      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
385      | List.Cons (hd0, tl) -> (fun _ -> safe_nth n' tl))) __
386
387(** val nub_by_internal :
388    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> Nat.nat -> 'a1 List.list **)
389let rec nub_by_internal f l = function
390| Nat.O ->
391  (match l with
392   | List.Nil -> List.Nil
393   | List.Cons (hd0, tl) -> l)
394| Nat.S n0 ->
395  (match l with
396   | List.Nil -> List.Nil
397   | List.Cons (hd0, tl) ->
398     List.Cons (hd0,
399       (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd0)) tl) n0)))
400
401(** val nub_by :
402    ('a1 -> 'a1 -> Bool.bool) -> 'a1 List.list -> 'a1 List.list **)
403let nub_by f l =
404  nub_by_internal f l (List.length l)
405
406(** val member :
407    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 List.list -> Bool.bool **)
408let rec member eq a = function
409| List.Nil -> Bool.False
410| List.Cons (hd0, tl) -> Bool.orb (eq a hd0) (member eq a tl)
411
412(** val take : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
413let rec take n l =
414  match n with
415  | Nat.O -> List.Nil
416  | Nat.S n0 ->
417    (match l with
418     | List.Nil -> List.Nil
419     | List.Cons (hd0, tl) -> List.Cons (hd0, (take n0 tl)))
420
421(** val drop : Nat.nat -> 'a1 List.list -> 'a1 List.list **)
422let rec drop n l =
423  match n with
424  | Nat.O -> l
425  | Nat.S n0 ->
426    (match l with
427     | List.Nil -> List.Nil
428     | List.Cons (hd0, tl) -> drop n0 tl)
429
430(** val list_split :
431    Nat.nat -> 'a1 List.list -> ('a1 List.list, 'a1 List.list) Types.prod **)
432let list_split n l =
433  { Types.fst = (take n l); Types.snd = (drop n l) }
434
435(** val mapi_internal :
436    Nat.nat -> (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
437let rec mapi_internal n f = function
438| List.Nil -> List.Nil
439| List.Cons (hd0, tl) ->
440  List.Cons ((f n hd0), (mapi_internal (Nat.plus n (Nat.S Nat.O)) f tl))
441
442(** val mapi : (Nat.nat -> 'a1 -> 'a2) -> 'a1 List.list -> 'a2 List.list **)
443let mapi f l =
444  mapi_internal Nat.O f l
445
446(** val zip_pottier :
447    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
448let rec zip_pottier left right =
449  match left with
450  | List.Nil -> List.Nil
451  | List.Cons (hd0, tl) ->
452    (match right with
453     | List.Nil -> List.Nil
454     | List.Cons (hd', tl') ->
455       List.Cons ({ Types.fst = hd0; Types.snd = hd' }, (zip_pottier tl tl')))
456
457(** val zip_safe :
458    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list **)
459let rec zip_safe left right =
460  (match left with
461   | List.Nil ->
462     (fun _ ->
463       (match right with
464        | List.Nil -> (fun _ -> List.Nil)
465        | List.Cons (hd0, tl) ->
466          (fun _ ->
467            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
468   | List.Cons (hd0, tl) ->
469     (fun _ ->
470       (match right with
471        | List.Nil ->
472          (fun _ ->
473            Obj.magic Nat.nat_discr (Nat.S (List.length tl)) Nat.O __)
474        | List.Cons (hd', tl') ->
475          (fun _ -> List.Cons ({ Types.fst = hd0; Types.snd = hd' },
476            (zip_safe tl tl')))) __)) __
477
478(** val zip :
479    'a1 List.list -> 'a2 List.list -> ('a1, 'a2) Types.prod List.list
480    Types.option **)
481let rec zip l r =
482  match l with
483  | List.Nil -> Types.Some List.Nil
484  | List.Cons (hd0, tl) ->
485    (match r with
486     | List.Nil -> Types.None
487     | List.Cons (hd', tl') ->
488       (match zip tl tl' with
489        | Types.None -> Types.None
490        | Types.Some tail0 ->
491          Types.Some (List.Cons ({ Types.fst = hd0; Types.snd = hd' },
492            tail0))))
493
494(** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
495let rec foldl f a = function
496| List.Nil -> a
497| List.Cons (hd0, tl) -> foldl f (f a hd0) tl
498
499(** val rev : 'a1 List.list -> 'a1 List.list **)
500let rev l =
501  List.reverse l
502
503(** val fold_left_i_aux :
504    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
505let rec fold_left_i_aux f x i = function
506| List.Nil -> x
507| List.Cons (hd0, tl) -> fold_left_i_aux f (f i x hd0) (Nat.S i) tl
508
509(** val fold_left_i :
510    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
511let fold_left_i f x =
512  fold_left_i_aux f x Nat.O
513
514(** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
515let function_apply f a =
516  f a
517
518(** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
519let rec iterate f a = function
520| Nat.O -> a
521| Nat.S o -> f (iterate f a o)
522
523(** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
524let rec division_aux m n p =
525  match ltb n (Nat.S p) with
526  | Bool.True -> Nat.O
527  | Bool.False ->
528    (match m with
529     | Nat.O -> Nat.O
530     | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))
531
532(** val division : Nat.nat -> Nat.nat -> Nat.nat **)
533let division m = function
534| Nat.O -> Nat.S m
535| Nat.S o -> division_aux m m o
536
537(** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
538let rec modulus_aux m n p =
539  match Nat.leb n p with
540  | Bool.True -> n
541  | Bool.False ->
542    (match m with
543     | Nat.O -> n
544     | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)
545
546(** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
547let modulus m = function
548| Nat.O -> m
549| Nat.S o -> modulus_aux m m o
550
551(** val divide_with_remainder :
552    Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
553let divide_with_remainder m n =
554  { Types.fst = (division m n); Types.snd = (modulus m n) }
555
556(** val less_than_or_equal_b_elim :
557    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
558let less_than_or_equal_b_elim m n h1 h2 =
559  (match Nat.leb m n with
560   | Bool.True -> (fun _ _ -> h1 __)
561   | Bool.False -> (fun _ _ -> h2 __)) __ __
562
563open Div_and_mod
564
565(** val dpi1__o__bool_to_Prop__o__inject :
566    (Bool.bool, 'a1) Types.dPair -> __ Types.sig0 **)
567let dpi1__o__bool_to_Prop__o__inject x2 =
568  __
569
570(** val eject__o__bool_to_Prop__o__inject :
571    Bool.bool Types.sig0 -> __ Types.sig0 **)
572let eject__o__bool_to_Prop__o__inject x2 =
573  __
574
575(** val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0 **)
576let bool_to_Prop__o__inject x1 =
577  __
578
579(** val dpi1__o__bool_to_Prop_to_eq__o__inject :
580    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
581let dpi1__o__bool_to_Prop_to_eq__o__inject x0 x3 =
582  __
583
584(** val eject__o__bool_to_Prop_to_eq__o__inject :
585    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
586let eject__o__bool_to_Prop_to_eq__o__inject x0 x3 =
587  __
588
589(** val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
590let bool_to_Prop_to_eq__o__inject x0 =
591  __
592
593(** val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
594    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
595let dpi1__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
596  __
597
598(** val eject__o__not_bool_to_Prop_to_eq__o__inject :
599    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
600let eject__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
601  __
602
603(** val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
604let not_bool_to_Prop_to_eq__o__inject x0 =
605  __
606
607(** val if_then_else_safe :
608    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
609let if_then_else_safe b f g0 =
610  (match b with
611   | Bool.True -> f
612   | Bool.False -> g0) __
613
614(** val dpi1__o__not_neq_None__o__inject :
615    'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0 **)
616let dpi1__o__not_neq_None__o__inject x1 x4 =
617  __
618
619(** val eject__o__not_neq_None__o__inject :
620    'a1 Types.option -> __ Types.sig0 -> __ Types.sig0 **)
621let eject__o__not_neq_None__o__inject x1 x4 =
622  __
623
624(** val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0 **)
625let not_neq_None__o__inject x1 =
626  __
627
628(** val prod_jmdiscr :
629    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
630let prod_jmdiscr x y =
631  Logic.eq_rect_Type2 x
632    (let { Types.fst = a0; Types.snd = a10 } = x in
633    Obj.magic (fun _ dH -> dH __ __)) y
634
635(** val eq_rect_Type1_r0 : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
636let eq_rect_Type1_r0 a h x =
637  (fun _ auto -> auto) __ h
638
639(** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
640let some_Some_elim x y h =
641  h __
642
643(** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
644let pose a auto =
645  auto a __
646
647(** val eq_sum :
648    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
649    Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
650let eq_sum leq req left right =
651  match left with
652  | Types.Inl l ->
653    (match right with
654     | Types.Inl l' -> leq l l'
655     | Types.Inr x -> Bool.False)
656  | Types.Inr r ->
657    (match right with
658     | Types.Inl x -> Bool.False
659     | Types.Inr r' -> req r r')
660
661(** val eq_prod :
662    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
663    Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
664let eq_prod leq req left right =
665  let { Types.fst = l; Types.snd = r } = left in
666  let { Types.fst = l'; Types.snd = r' } = right in
667  Bool.andb (leq l l') (req r r')
668
Note: See TracBrowser for help on using the repository browser.