extracted/bigops.ml

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open Div_and_mod
  20
  21 (** val prodF :
  22     (Nat.nat -> 'a1) -> (Nat.nat -> 'a2) -> Nat.nat -> Nat.nat -> ('a1, 'a2)
  23     Types.prod **)
  24 let 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 **)
  31 let 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
  39 type '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 **)
  45 let 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 **)
  50 let 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 **)
  55 let 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 **)
  60 let 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 **)
  65 let 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 **)
  70 let 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 **)
  74 let 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 **)
  80 let 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 **)
  86 let 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 **)
  92 let 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 **)
  98 let 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 **)
 104 let 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 -> __ **)
 108 let 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 **)
 114 let dpi1__o__op x1 x3 =
 115   op x1 x3.Types.dpi1
 116
 117 type '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 **)
 123 let 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 **)
 128 let 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 **)
 133 let 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 **)
 138 let 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 **)
 143 let 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 **)
 148 let 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 **)
 152 let 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 **)
 157 let 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 **)
 162 let 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 **)
 167 let 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 **)
 172 let 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 **)
 177 let 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 -> __ **)
 181 let 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 **)
 186 let 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 **)
 190 let 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 **)
 194 let dpi1__o__aop x1 x3 =
 195   aop0 x1 x3.Types.dpi1
 196
 197 type '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 **)
 203 let 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 **)
 210 let 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 **)
 217 let 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 **)
 224 let 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 **)
 231 let 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 **)
 238 let 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 **)
 243 let rec enum xxx =
 244   xxx.enum
 245
 246 (** val upto : 'a1 range -> Nat.nat **)
 247 let rec upto xxx =
 248   xxx.upto
 249
 250 (** val filter : 'a1 range -> Nat.nat -> Bool.bool **)
 251 let 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 **)
 257 let 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 **)
 263 let 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 **)
 269 let 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 **)
 275 let 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 **)
 281 let 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 -> __ **)
 285 let 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
 290 type '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 **)
 295 let 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 **)
 301 let 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 **)
 307 let 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 **)
 313 let 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 **)
 319 let 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 **)
 325 let 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 **)
 329 let rec sum0 nil xxx =
 330   xxx.sum0
 331
 332 (** val prod0 : 'a1 -> 'a1 dop -> 'a1 -> 'a1 -> 'a1 **)
 333 let 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 **)
 339 let 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 **)
 345 let 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 **)
 351 let 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 **)
 357 let 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 **)
 363 let 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 -> __ **)
 367 let 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