source: driver/extracted/bigops.ml @ 3106

Last change on this file since 3106 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: 11.9 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Div_and_mod
20
21(** val prodF :
22    (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
23    Types.prod **)
24let prodF f g m x =
25  { Types.fst = (f (Div_and_mod.div x m)); Types.snd =
26    (g (Div_and_mod.mod0 x m)) }
27
28(** val bigop :
29    Nat.nat -> (Nat.nat -> Bool.bool) -> 'a1 -> ('a1 -> 'a1 -> 'a1) ->
30    (Nat.nat -> 'a1) -> 'a1 **)
31let rec bigop n p nil op f =
32  match n with
33  | Nat.O -> nil
34  | Nat.S k ->
35    (match p k with
36     | Bool.True -> op (f k) (bigop k p nil op f)
37     | Bool.False -> bigop k p nil op f)
38
39type 'a aop =
40  'a -> 'a -> 'a
41  (* singleton inductive, whose constructor was mk_Aop *)
42
43(** val aop_rect_Type4 :
44    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
45let rec aop_rect_Type4 nil h_mk_Aop x_969 =
46  let op = x_969 in h_mk_Aop op __ __ __
47
48(** val aop_rect_Type5 :
49    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
50let rec aop_rect_Type5 nil h_mk_Aop x_971 =
51  let op = x_971 in h_mk_Aop op __ __ __
52
53(** val aop_rect_Type3 :
54    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
55let rec aop_rect_Type3 nil h_mk_Aop x_973 =
56  let op = x_973 in h_mk_Aop op __ __ __
57
58(** val aop_rect_Type2 :
59    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
60let rec aop_rect_Type2 nil h_mk_Aop x_975 =
61  let op = x_975 in h_mk_Aop op __ __ __
62
63(** val aop_rect_Type1 :
64    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
65let rec aop_rect_Type1 nil h_mk_Aop x_977 =
66  let op = x_977 in h_mk_Aop op __ __ __
67
68(** val aop_rect_Type0 :
69    'a1 -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> 'a2) -> 'a1 aop -> 'a2 **)
70let rec aop_rect_Type0 nil h_mk_Aop x_979 =
71  let op = x_979 in h_mk_Aop op __ __ __
72
73(** val op : 'a1 -> 'a1 aop -> 'a1 -> 'a1 -> 'a1 **)
74let rec op nil xxx =
75  let yyy = xxx in yyy
76
77(** val aop_inv_rect_Type4 :
78    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
79    'a2 **)
80let aop_inv_rect_Type4 x2 hterm h1 =
81  let hcut = aop_rect_Type4 x2 h1 hterm in hcut __
82
83(** val aop_inv_rect_Type3 :
84    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
85    'a2 **)
86let aop_inv_rect_Type3 x2 hterm h1 =
87  let hcut = aop_rect_Type3 x2 h1 hterm in hcut __
88
89(** val aop_inv_rect_Type2 :
90    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
91    'a2 **)
92let aop_inv_rect_Type2 x2 hterm h1 =
93  let hcut = aop_rect_Type2 x2 h1 hterm in hcut __
94
95(** val aop_inv_rect_Type1 :
96    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
97    'a2 **)
98let aop_inv_rect_Type1 x2 hterm h1 =
99  let hcut = aop_rect_Type1 x2 h1 hterm in hcut __
100
101(** val aop_inv_rect_Type0 :
102    'a1 -> 'a1 aop -> (('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ -> __ -> 'a2) ->
103    'a2 **)
104let aop_inv_rect_Type0 x2 hterm h1 =
105  let hcut = aop_rect_Type0 x2 h1 hterm in hcut __
106
107(** val aop_discr : 'a1 -> 'a1 aop -> 'a1 aop -> __ **)
108let aop_discr a2 x y =
109  Logic.eq_rect_Type2 x
110    (let a0 = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y
111
112(** val dpi1__o__op :
113    'a1 -> ('a1 aop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
114let dpi1__o__op x1 x3 =
115  op x1 x3.Types.dpi1
116
117type 'a aCop =
118  'a aop
119  (* singleton inductive, whose constructor was mk_ACop *)
120
121(** val aCop_rect_Type4 :
122    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
123let rec aCop_rect_Type4 nil h_mk_ACop x_997 =
124  let aop0 = x_997 in h_mk_ACop aop0 __
125
126(** val aCop_rect_Type5 :
127    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
128let rec aCop_rect_Type5 nil h_mk_ACop x_999 =
129  let aop0 = x_999 in h_mk_ACop aop0 __
130
131(** val aCop_rect_Type3 :
132    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
133let rec aCop_rect_Type3 nil h_mk_ACop x_1001 =
134  let aop0 = x_1001 in h_mk_ACop aop0 __
135
136(** val aCop_rect_Type2 :
137    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
138let rec aCop_rect_Type2 nil h_mk_ACop x_1003 =
139  let aop0 = x_1003 in h_mk_ACop aop0 __
140
141(** val aCop_rect_Type1 :
142    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
143let rec aCop_rect_Type1 nil h_mk_ACop x_1005 =
144  let aop0 = x_1005 in h_mk_ACop aop0 __
145
146(** val aCop_rect_Type0 :
147    'a1 -> ('a1 aop -> __ -> 'a2) -> 'a1 aCop -> 'a2 **)
148let rec aCop_rect_Type0 nil h_mk_ACop x_1007 =
149  let aop0 = x_1007 in h_mk_ACop aop0 __
150
151(** val aop0 : 'a1 -> 'a1 aCop -> 'a1 aop **)
152let rec aop0 nil xxx =
153  let yyy = xxx in yyy
154
155(** val aCop_inv_rect_Type4 :
156    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
157let aCop_inv_rect_Type4 x2 hterm h1 =
158  let hcut = aCop_rect_Type4 x2 h1 hterm in hcut __
159
160(** val aCop_inv_rect_Type3 :
161    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
162let aCop_inv_rect_Type3 x2 hterm h1 =
163  let hcut = aCop_rect_Type3 x2 h1 hterm in hcut __
164
165(** val aCop_inv_rect_Type2 :
166    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
167let aCop_inv_rect_Type2 x2 hterm h1 =
168  let hcut = aCop_rect_Type2 x2 h1 hterm in hcut __
169
170(** val aCop_inv_rect_Type1 :
171    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
172let aCop_inv_rect_Type1 x2 hterm h1 =
173  let hcut = aCop_rect_Type1 x2 h1 hterm in hcut __
174
175(** val aCop_inv_rect_Type0 :
176    'a1 -> 'a1 aCop -> ('a1 aop -> __ -> __ -> 'a2) -> 'a2 **)
177let aCop_inv_rect_Type0 x2 hterm h1 =
178  let hcut = aCop_rect_Type0 x2 h1 hterm in hcut __
179
180(** val aCop_discr : 'a1 -> 'a1 aCop -> 'a1 aCop -> __ **)
181let aCop_discr a2 x y =
182  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
183
184(** val dpi1__o__aop__o__op :
185    'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 -> 'a1 -> 'a1 **)
186let dpi1__o__aop__o__op x1 x3 =
187  op x1 (aop0 x1 x3.Types.dpi1)
188
189(** val aop__o__op : 'a1 -> 'a1 aCop -> 'a1 -> 'a1 -> 'a1 **)
190let aop__o__op x1 x2 =
191  op x1 (aop0 x1 x2)
192
193(** val dpi1__o__aop : 'a1 -> ('a1 aCop, 'a2) Types.dPair -> 'a1 aop **)
194let dpi1__o__aop x1 x3 =
195  aop0 x1 x3.Types.dpi1
196
197type 'a range = { enum : (Nat.nat -> 'a); upto : Nat.nat;
198                  filter : (Nat.nat -> Bool.bool) }
199
200(** val range_rect_Type4 :
201    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
202    range -> 'a2 **)
203let rec range_rect_Type4 h_mk_range x_1023 =
204  let { enum = enum0; upto = upto0; filter = filter0 } = x_1023 in
205  h_mk_range enum0 upto0 filter0
206
207(** val range_rect_Type5 :
208    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
209    range -> 'a2 **)
210let rec range_rect_Type5 h_mk_range x_1025 =
211  let { enum = enum0; upto = upto0; filter = filter0 } = x_1025 in
212  h_mk_range enum0 upto0 filter0
213
214(** val range_rect_Type3 :
215    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
216    range -> 'a2 **)
217let rec range_rect_Type3 h_mk_range x_1027 =
218  let { enum = enum0; upto = upto0; filter = filter0 } = x_1027 in
219  h_mk_range enum0 upto0 filter0
220
221(** val range_rect_Type2 :
222    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
223    range -> 'a2 **)
224let rec range_rect_Type2 h_mk_range x_1029 =
225  let { enum = enum0; upto = upto0; filter = filter0 } = x_1029 in
226  h_mk_range enum0 upto0 filter0
227
228(** val range_rect_Type1 :
229    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
230    range -> 'a2 **)
231let rec range_rect_Type1 h_mk_range x_1031 =
232  let { enum = enum0; upto = upto0; filter = filter0 } = x_1031 in
233  h_mk_range enum0 upto0 filter0
234
235(** val range_rect_Type0 :
236    ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> 'a2) -> 'a1
237    range -> 'a2 **)
238let rec range_rect_Type0 h_mk_range x_1033 =
239  let { enum = enum0; upto = upto0; filter = filter0 } = x_1033 in
240  h_mk_range enum0 upto0 filter0
241
242(** val enum : 'a1 range -> Nat.nat -> 'a1 **)
243let rec enum xxx =
244  xxx.enum
245
246(** val upto : 'a1 range -> Nat.nat **)
247let rec upto xxx =
248  xxx.upto
249
250(** val filter : 'a1 range -> Nat.nat -> Bool.bool **)
251let rec filter xxx =
252  xxx.filter
253
254(** val range_inv_rect_Type4 :
255    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
256    -> 'a2) -> 'a2 **)
257let range_inv_rect_Type4 hterm h1 =
258  let hcut = range_rect_Type4 h1 hterm in hcut __
259
260(** val range_inv_rect_Type3 :
261    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
262    -> 'a2) -> 'a2 **)
263let range_inv_rect_Type3 hterm h1 =
264  let hcut = range_rect_Type3 h1 hterm in hcut __
265
266(** val range_inv_rect_Type2 :
267    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
268    -> 'a2) -> 'a2 **)
269let range_inv_rect_Type2 hterm h1 =
270  let hcut = range_rect_Type2 h1 hterm in hcut __
271
272(** val range_inv_rect_Type1 :
273    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
274    -> 'a2) -> 'a2 **)
275let range_inv_rect_Type1 hterm h1 =
276  let hcut = range_rect_Type1 h1 hterm in hcut __
277
278(** val range_inv_rect_Type0 :
279    'a1 range -> ((Nat.nat -> 'a1) -> Nat.nat -> (Nat.nat -> Bool.bool) -> __
280    -> 'a2) -> 'a2 **)
281let range_inv_rect_Type0 hterm h1 =
282  let hcut = range_rect_Type0 h1 hterm in hcut __
283
284(** val range_discr : 'a1 range -> 'a1 range -> __ **)
285let range_discr x y =
286  Logic.eq_rect_Type2 x
287    (let { enum = a0; upto = a10; filter = a2 } = x in
288    Obj.magic (fun _ dH -> dH __ __ __)) y
289
290type 'a dop = { sum0 : 'a aCop; prod0 : ('a -> 'a -> 'a) }
291
292(** val dop_rect_Type4 :
293    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
294    'a2 **)
295let rec dop_rect_Type4 nil h_mk_Dop x_1051 =
296  let { sum0 = sum1; prod0 = prod1 } = x_1051 in h_mk_Dop sum1 prod1 __ __
297
298(** val dop_rect_Type5 :
299    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
300    'a2 **)
301let rec dop_rect_Type5 nil h_mk_Dop x_1053 =
302  let { sum0 = sum1; prod0 = prod1 } = x_1053 in h_mk_Dop sum1 prod1 __ __
303
304(** val dop_rect_Type3 :
305    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
306    'a2 **)
307let rec dop_rect_Type3 nil h_mk_Dop x_1055 =
308  let { sum0 = sum1; prod0 = prod1 } = x_1055 in h_mk_Dop sum1 prod1 __ __
309
310(** val dop_rect_Type2 :
311    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
312    'a2 **)
313let rec dop_rect_Type2 nil h_mk_Dop x_1057 =
314  let { sum0 = sum1; prod0 = prod1 } = x_1057 in h_mk_Dop sum1 prod1 __ __
315
316(** val dop_rect_Type1 :
317    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
318    'a2 **)
319let rec dop_rect_Type1 nil h_mk_Dop x_1059 =
320  let { sum0 = sum1; prod0 = prod1 } = x_1059 in h_mk_Dop sum1 prod1 __ __
321
322(** val dop_rect_Type0 :
323    'a1 -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> 'a2) -> 'a1 dop ->
324    'a2 **)
325let rec dop_rect_Type0 nil h_mk_Dop x_1061 =
326  let { sum0 = sum1; prod0 = prod1 } = x_1061 in h_mk_Dop sum1 prod1 __ __
327
328(** val sum0 : 'a1 -> 'a1 dop -> 'a1 aCop **)
329let rec sum0 nil xxx =
330  xxx.sum0
331
332(** val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1 **)
333let rec prod0 nil xxx =
334  xxx.prod0
335
336(** val dop_inv_rect_Type4 :
337    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
338    'a2) -> 'a2 **)
339let dop_inv_rect_Type4 x2 hterm h1 =
340  let hcut = dop_rect_Type4 x2 h1 hterm in hcut __
341
342(** val dop_inv_rect_Type3 :
343    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
344    'a2) -> 'a2 **)
345let dop_inv_rect_Type3 x2 hterm h1 =
346  let hcut = dop_rect_Type3 x2 h1 hterm in hcut __
347
348(** val dop_inv_rect_Type2 :
349    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
350    'a2) -> 'a2 **)
351let dop_inv_rect_Type2 x2 hterm h1 =
352  let hcut = dop_rect_Type2 x2 h1 hterm in hcut __
353
354(** val dop_inv_rect_Type1 :
355    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
356    'a2) -> 'a2 **)
357let dop_inv_rect_Type1 x2 hterm h1 =
358  let hcut = dop_rect_Type1 x2 h1 hterm in hcut __
359
360(** val dop_inv_rect_Type0 :
361    'a1 -> 'a1 dop -> ('a1 aCop -> ('a1 -> 'a1 -> 'a1) -> __ -> __ -> __ ->
362    'a2) -> 'a2 **)
363let dop_inv_rect_Type0 x2 hterm h1 =
364  let hcut = dop_rect_Type0 x2 h1 hterm in hcut __
365
366(** val dop_discr : 'a1 -> 'a1 dop -> 'a1 dop -> __ **)
367let dop_discr a2 x y =
368  Logic.eq_rect_Type2 x
369    (let { sum0 = a0; prod0 = a10 } = x in
370    Obj.magic (fun _ dH -> dH __ __ __ __)) y
371
Note: See TracBrowser for help on using the repository browser.