source: extracted/util.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 (hd, tl) -> Bool.andb (f hd) (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 (hd, tl) ->
131  (match k with
132   | Nat.O -> List.Nil
133   | Nat.S k' -> List.Cons (hd, (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 (hd, tl) ->
145          (fun _ ->
146            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
147   | List.Cons (hd, 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 hd 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 (hd, 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 (e, tl) ->
177    (match geb i m with
178     | Bool.True -> res
179     | Bool.False -> foldi_from_until_internal (Nat.S i) (f i res e) 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 (hd, tl) -> (fun _ -> hd)) __
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 (hd, 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 (hd, tl) ->
227          (fun _ ->
228            let { Types.fst = l1; Types.snd = l2 } = safe_split tl index' in
229            { Types.fst = (List.Cons (hd, 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 (hd, tl) -> (fun _ -> hd))
238   | Nat.S index' ->
239     (match the_list with
240      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
241      | List.Cons (hd, 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 (hd, 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 (hd, 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 (hd, 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 (hd, 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 (hd, 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 tail -> Types.Some (List.Cons ((f hd hd'), tail))))
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 (hd, 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 hd 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 (hd, tl) ->
342               (fun _ ->
343                 Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __))
344              __)
345        | List.Cons (hd, 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 (hd, 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 (hd, 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 hd hd' hd''), (map3 f tl tl' tl''))))
369              __ __)) __)) __
370
371(** val eq_rect_Type0_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
372let eq_rect_Type0_r 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 (hd, tl) -> (fun _ -> hd))
382   | Nat.S n' ->
383     (match l with
384      | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
385      | List.Cons (hd, 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 (hd, tl) -> l)
394| Nat.S n0 ->
395  (match l with
396   | List.Nil -> List.Nil
397   | List.Cons (hd, tl) ->
398     List.Cons (hd,
399       (nub_by_internal f (List.filter (fun y -> Bool.notb (f y hd)) 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 (hd, tl) -> Bool.orb (eq a hd) (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 (hd, tl) -> List.Cons (hd, (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 (hd, 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 (hd, tl) ->
440  List.Cons ((f n hd), (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 (hd, tl) ->
452    (match right with
453     | List.Nil -> List.Nil
454     | List.Cons (hd', tl') ->
455       List.Cons ({ Types.fst = hd; 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 (hd, tl) ->
466          (fun _ ->
467            Obj.magic Nat.nat_discr Nat.O (Nat.S (List.length tl)) __)) __)
468   | List.Cons (hd, 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 = hd; 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 (hd, 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 tail ->
491          Types.Some (List.Cons ({ Types.fst = hd; Types.snd = hd' }, tail))))
492
493(** val foldl : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
494let rec foldl f a = function
495| List.Nil -> a
496| List.Cons (hd, tl) -> foldl f (f a hd) tl
497
498(** val rev : 'a1 List.list -> 'a1 List.list **)
499let rev l =
500  List.reverse l
501
502(** val fold_left_i_aux :
503    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> Nat.nat -> 'a2 List.list -> 'a1 **)
504let rec fold_left_i_aux f x i = function
505| List.Nil -> x
506| List.Cons (hd, tl) -> fold_left_i_aux f (f i x hd) (Nat.S i) tl
507
508(** val fold_left_i :
509    (Nat.nat -> 'a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 List.list -> 'a1 **)
510let fold_left_i f x =
511  fold_left_i_aux f x Nat.O
512
513(** val function_apply : ('a1 -> 'a2) -> 'a1 -> 'a2 **)
514let function_apply f a =
515  f a
516
517(** val iterate : ('a1 -> 'a1) -> 'a1 -> Nat.nat -> 'a1 **)
518let rec iterate f a = function
519| Nat.O -> a
520| Nat.S o -> f (iterate f a o)
521
522(** val division_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
523let rec division_aux m n p =
524  match ltb n (Nat.S p) with
525  | Bool.True -> Nat.O
526  | Bool.False ->
527    (match m with
528     | Nat.O -> Nat.O
529     | Nat.S q -> Nat.S (division_aux q (Nat.minus n (Nat.S p)) p))
530
531(** val division : Nat.nat -> Nat.nat -> Nat.nat **)
532let division m = function
533| Nat.O -> Nat.S m
534| Nat.S o -> division_aux m m o
535
536(** val modulus_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
537let rec modulus_aux m n p =
538  match Nat.leb n p with
539  | Bool.True -> n
540  | Bool.False ->
541    (match m with
542     | Nat.O -> n
543     | Nat.S o -> modulus_aux o (Nat.minus n (Nat.S p)) p)
544
545(** val modulus : Nat.nat -> Nat.nat -> Nat.nat **)
546let modulus m = function
547| Nat.O -> m
548| Nat.S o -> modulus_aux m m o
549
550(** val divide_with_remainder :
551    Nat.nat -> Nat.nat -> (Nat.nat, Nat.nat) Types.prod **)
552let divide_with_remainder m n =
553  { Types.fst = (division m n); Types.snd = (modulus m n) }
554
555(** val less_than_or_equal_b_elim :
556    Nat.nat -> Nat.nat -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
557let less_than_or_equal_b_elim m n h1 h2 =
558  (match Nat.leb m n with
559   | Bool.True -> (fun _ _ -> h1 __)
560   | Bool.False -> (fun _ _ -> h2 __)) __ __
561
562open Div_and_mod
563
564(** val dpi1__o__bool_to_Prop__o__inject :
565    (Bool.bool, 'a1) Types.dPair -> __ Types.sig0 **)
566let dpi1__o__bool_to_Prop__o__inject x2 =
567  __
568
569(** val eject__o__bool_to_Prop__o__inject :
570    Bool.bool Types.sig0 -> __ Types.sig0 **)
571let eject__o__bool_to_Prop__o__inject x2 =
572  __
573
574(** val bool_to_Prop__o__inject : Bool.bool -> __ Types.sig0 **)
575let bool_to_Prop__o__inject x1 =
576  __
577
578(** val dpi1__o__bool_to_Prop_to_eq__o__inject :
579    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
580let dpi1__o__bool_to_Prop_to_eq__o__inject x0 x3 =
581  __
582
583(** val eject__o__bool_to_Prop_to_eq__o__inject :
584    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
585let eject__o__bool_to_Prop_to_eq__o__inject x0 x3 =
586  __
587
588(** val bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
589let bool_to_Prop_to_eq__o__inject x0 =
590  __
591
592(** val dpi1__o__not_bool_to_Prop_to_eq__o__inject :
593    Bool.bool -> (__, 'a1) Types.dPair -> __ Types.sig0 **)
594let dpi1__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
595  __
596
597(** val eject__o__not_bool_to_Prop_to_eq__o__inject :
598    Bool.bool -> __ Types.sig0 -> __ Types.sig0 **)
599let eject__o__not_bool_to_Prop_to_eq__o__inject x0 x3 =
600  __
601
602(** val not_bool_to_Prop_to_eq__o__inject : Bool.bool -> __ Types.sig0 **)
603let not_bool_to_Prop_to_eq__o__inject x0 =
604  __
605
606(** val if_then_else_safe :
607    Bool.bool -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
608let if_then_else_safe b f g =
609  (match b with
610   | Bool.True -> f
611   | Bool.False -> g) __
612
613(** val dpi1__o__not_neq_None__o__inject :
614    'a1 Types.option -> (__, 'a2) Types.dPair -> __ Types.sig0 **)
615let dpi1__o__not_neq_None__o__inject x1 x4 =
616  __
617
618(** val eject__o__not_neq_None__o__inject :
619    'a1 Types.option -> __ Types.sig0 -> __ Types.sig0 **)
620let eject__o__not_neq_None__o__inject x1 x4 =
621  __
622
623(** val not_neq_None__o__inject : 'a1 Types.option -> __ Types.sig0 **)
624let not_neq_None__o__inject x1 =
625  __
626
627(** val prod_jmdiscr :
628    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
629let prod_jmdiscr x y =
630  Logic.eq_rect_Type2 x
631    (let { Types.fst = a0; Types.snd = a10 } = x in
632    Obj.magic (fun _ dH -> dH __ __)) y
633
634(** val eq_rect_Type1_r : 'a1 -> 'a2 -> 'a1 -> 'a2 **)
635let eq_rect_Type1_r a h x =
636  (fun _ auto -> auto) __ h
637
638(** val some_Some_elim : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2 **)
639let some_Some_elim x y h =
640  h __
641
642(** val pose : 'a1 -> ('a1 -> __ -> 'a2) -> 'a2 **)
643let pose a auto =
644  auto a __
645
646(** val eq_sum :
647    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
648    Types.sum -> ('a1, 'a2) Types.sum -> Bool.bool **)
649let eq_sum leq req left right =
650  match left with
651  | Types.Inl l ->
652    (match right with
653     | Types.Inl l' -> leq l l'
654     | Types.Inr x -> Bool.False)
655  | Types.Inr r ->
656    (match right with
657     | Types.Inl x -> Bool.False
658     | Types.Inr r' -> req r r')
659
660(** val eq_prod :
661    ('a1 -> 'a1 -> Bool.bool) -> ('a2 -> 'a2 -> Bool.bool) -> ('a1, 'a2)
662    Types.prod -> ('a1, 'a2) Types.prod -> Bool.bool **)
663let eq_prod leq req left right =
664  let { Types.fst = l; Types.snd = r } = left in
665  let { Types.fst = l'; Types.snd = r' } = right in
666  Bool.andb (leq l l') (req r r')
667
Note: See TracBrowser for help on using the repository browser.