extracted/positive.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 Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 type compare =
  18 | LT
  19 | EQ
  20 | GT
  21
  22 (** val compare_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  23 let rec compare_rect_Type4 h_LT h_EQ h_GT = function
  24 | LT -> h_LT
  25 | EQ -> h_EQ
  26 | GT -> h_GT
  27
  28 (** val compare_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  29 let rec compare_rect_Type5 h_LT h_EQ h_GT = function
  30 | LT -> h_LT
  31 | EQ -> h_EQ
  32 | GT -> h_GT
  33
  34 (** val compare_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  35 let rec compare_rect_Type3 h_LT h_EQ h_GT = function
  36 | LT -> h_LT
  37 | EQ -> h_EQ
  38 | GT -> h_GT
  39
  40 (** val compare_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  41 let rec compare_rect_Type2 h_LT h_EQ h_GT = function
  42 | LT -> h_LT
  43 | EQ -> h_EQ
  44 | GT -> h_GT
  45
  46 (** val compare_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  47 let rec compare_rect_Type1 h_LT h_EQ h_GT = function
  48 | LT -> h_LT
  49 | EQ -> h_EQ
  50 | GT -> h_GT
  51
  52 (** val compare_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> compare -> 'a1 **)
  53 let rec compare_rect_Type0 h_LT h_EQ h_GT = function
  54 | LT -> h_LT
  55 | EQ -> h_EQ
  56 | GT -> h_GT
  57
  58 (** val compare_inv_rect_Type4 :
  59     compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  60 let compare_inv_rect_Type4 hterm h1 h2 h3 =
  61   let hcut = compare_rect_Type4 h1 h2 h3 hterm in hcut __
  62
  63 (** val compare_inv_rect_Type3 :
  64     compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  65 let compare_inv_rect_Type3 hterm h1 h2 h3 =
  66   let hcut = compare_rect_Type3 h1 h2 h3 hterm in hcut __
  67
  68 (** val compare_inv_rect_Type2 :
  69     compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  70 let compare_inv_rect_Type2 hterm h1 h2 h3 =
  71   let hcut = compare_rect_Type2 h1 h2 h3 hterm in hcut __
  72
  73 (** val compare_inv_rect_Type1 :
  74     compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  75 let compare_inv_rect_Type1 hterm h1 h2 h3 =
  76   let hcut = compare_rect_Type1 h1 h2 h3 hterm in hcut __
  77
  78 (** val compare_inv_rect_Type0 :
  79     compare -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  80 let compare_inv_rect_Type0 hterm h1 h2 h3 =
  81   let hcut = compare_rect_Type0 h1 h2 h3 hterm in hcut __
  82
  83 (** val compare_discr : compare -> compare -> __ **)
  84 let compare_discr x y =
  85   Logic.eq_rect_Type2 x
  86     (match x with
  87      | LT -> Obj.magic (fun _ dH -> dH)
  88      | EQ -> Obj.magic (fun _ dH -> dH)
  89      | GT -> Obj.magic (fun _ dH -> dH)) y
  90
  91 (** val compare_invert : compare -> compare **)
  92 let compare_invert = function
  93 | LT -> GT
  94 | EQ -> EQ
  95 | GT -> LT
  96
  97 type pos =
  98 | One
  99 | P1 of pos
 100 | P0 of pos
 101
 102 (** val pos_rect_Type4 :
 103     'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
 104 let rec pos_rect_Type4 h_one h_p1 h_p0 = function
 105 | One -> h_one
 106 | P1 x_1606 -> h_p1 x_1606 (pos_rect_Type4 h_one h_p1 h_p0 x_1606)
 107 | P0 x_1607 -> h_p0 x_1607 (pos_rect_Type4 h_one h_p1 h_p0 x_1607)
 108
 109 (** val pos_rect_Type3 :
 110     'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
 111 let rec pos_rect_Type3 h_one h_p1 h_p0 = function
 112 | One -> h_one
 113 | P1 x_1618 -> h_p1 x_1618 (pos_rect_Type3 h_one h_p1 h_p0 x_1618)
 114 | P0 x_1619 -> h_p0 x_1619 (pos_rect_Type3 h_one h_p1 h_p0 x_1619)
 115
 116 (** val pos_rect_Type2 :
 117     'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
 118 let rec pos_rect_Type2 h_one h_p1 h_p0 = function
 119 | One -> h_one
 120 | P1 x_1624 -> h_p1 x_1624 (pos_rect_Type2 h_one h_p1 h_p0 x_1624)
 121 | P0 x_1625 -> h_p0 x_1625 (pos_rect_Type2 h_one h_p1 h_p0 x_1625)
 122
 123 (** val pos_rect_Type1 :
 124     'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
 125 let rec pos_rect_Type1 h_one h_p1 h_p0 = function
 126 | One -> h_one
 127 | P1 x_1630 -> h_p1 x_1630 (pos_rect_Type1 h_one h_p1 h_p0 x_1630)
 128 | P0 x_1631 -> h_p0 x_1631 (pos_rect_Type1 h_one h_p1 h_p0 x_1631)
 129
 130 (** val pos_rect_Type0 :
 131     'a1 -> (pos -> 'a1 -> 'a1) -> (pos -> 'a1 -> 'a1) -> pos -> 'a1 **)
 132 let rec pos_rect_Type0 h_one h_p1 h_p0 = function
 133 | One -> h_one
 134 | P1 x_1636 -> h_p1 x_1636 (pos_rect_Type0 h_one h_p1 h_p0 x_1636)
 135 | P0 x_1637 -> h_p0 x_1637 (pos_rect_Type0 h_one h_p1 h_p0 x_1637)
 136
 137 (** val pos_inv_rect_Type4 :
 138     pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
 139     'a1) -> __ -> 'a1) -> 'a1 **)
 140 let pos_inv_rect_Type4 hterm h1 h2 h3 =
 141   let hcut = pos_rect_Type4 h1 h2 h3 hterm in hcut __
 142
 143 (** val pos_inv_rect_Type3 :
 144     pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
 145     'a1) -> __ -> 'a1) -> 'a1 **)
 146 let pos_inv_rect_Type3 hterm h1 h2 h3 =
 147   let hcut = pos_rect_Type3 h1 h2 h3 hterm in hcut __
 148
 149 (** val pos_inv_rect_Type2 :
 150     pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
 151     'a1) -> __ -> 'a1) -> 'a1 **)
 152 let pos_inv_rect_Type2 hterm h1 h2 h3 =
 153   let hcut = pos_rect_Type2 h1 h2 h3 hterm in hcut __
 154
 155 (** val pos_inv_rect_Type1 :
 156     pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
 157     'a1) -> __ -> 'a1) -> 'a1 **)
 158 let pos_inv_rect_Type1 hterm h1 h2 h3 =
 159   let hcut = pos_rect_Type1 h1 h2 h3 hterm in hcut __
 160
 161 (** val pos_inv_rect_Type0 :
 162     pos -> (__ -> 'a1) -> (pos -> (__ -> 'a1) -> __ -> 'a1) -> (pos -> (__ ->
 163     'a1) -> __ -> 'a1) -> 'a1 **)
 164 let pos_inv_rect_Type0 hterm h1 h2 h3 =
 165   let hcut = pos_rect_Type0 h1 h2 h3 hterm in hcut __
 166
 167 (** val pos_discr : pos -> pos -> __ **)
 168 let pos_discr x y =
 169   Logic.eq_rect_Type2 x
 170     (match x with
 171      | One -> Obj.magic (fun _ dH -> dH)
 172      | P1 a0 -> Obj.magic (fun _ dH -> dH __)
 173      | P0 a0 -> Obj.magic (fun _ dH -> dH __)) y
 174
 175 (** val pred : pos -> pos **)
 176 let rec pred = function
 177 | One -> One
 178 | P1 ps -> P0 ps
 179 | P0 ps ->
 180   (match ps with
 181    | One -> One
 182    | P1 x -> P1 (pred ps)
 183    | P0 x -> P1 (pred ps))
 184
 185 (** val succ : pos -> pos **)
 186 let rec succ = function
 187 | One -> P0 One
 188 | P1 ps -> P0 (succ ps)
 189 | P0 ps -> P1 ps
 190
 191 (** val nat_of_pos : pos -> Nat.nat **)
 192 let rec nat_of_pos = function
 193 | One -> Nat.S Nat.O
 194 | P1 ps -> Nat.S (Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps))
 195 | P0 ps -> Nat.times (Nat.S (Nat.S Nat.O)) (nat_of_pos ps)
 196
 197 (** val succ_pos_of_nat : Nat.nat -> pos **)
 198 let rec succ_pos_of_nat = function
 199 | Nat.O -> One
 200 | Nat.S n' -> succ (succ_pos_of_nat n')
 201
 202 (** val plus : pos -> pos -> pos **)
 203 let rec plus n m =
 204   match n with
 205   | One -> succ m
 206   | P1 n' ->
 207     (match m with
 208      | One -> succ n
 209      | P1 m' -> P0 (succ (plus n' m'))
 210      | P0 m' -> P1 (plus n' m'))
 211   | P0 n' ->
 212     (match m with
 213      | One -> P1 n'
 214      | P1 m' -> P1 (plus n' m')
 215      | P0 m' -> P0 (plus n' m'))
 216
 217 (** val times : pos -> pos -> pos **)
 218 let rec times n m =
 219   match n with
 220   | One -> m
 221   | P1 n' -> plus m (P0 (times n' m))
 222   | P0 n' -> P0 (times n' m)
 223
 224 type minusresult =
 225 | MinusNeg
 226 | MinusZero
 227 | MinusPos of pos
 228
 229 (** val minusresult_rect_Type4 :
 230     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 231 let rec minusresult_rect_Type4 h_MinusNeg h_MinusZero h_MinusPos = function
 232 | MinusNeg -> h_MinusNeg
 233 | MinusZero -> h_MinusZero
 234 | MinusPos x_1813 -> h_MinusPos x_1813
 235
 236 (** val minusresult_rect_Type5 :
 237     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 238 let rec minusresult_rect_Type5 h_MinusNeg h_MinusZero h_MinusPos = function
 239 | MinusNeg -> h_MinusNeg
 240 | MinusZero -> h_MinusZero
 241 | MinusPos x_1818 -> h_MinusPos x_1818
 242
 243 (** val minusresult_rect_Type3 :
 244     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 245 let rec minusresult_rect_Type3 h_MinusNeg h_MinusZero h_MinusPos = function
 246 | MinusNeg -> h_MinusNeg
 247 | MinusZero -> h_MinusZero
 248 | MinusPos x_1823 -> h_MinusPos x_1823
 249
 250 (** val minusresult_rect_Type2 :
 251     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 252 let rec minusresult_rect_Type2 h_MinusNeg h_MinusZero h_MinusPos = function
 253 | MinusNeg -> h_MinusNeg
 254 | MinusZero -> h_MinusZero
 255 | MinusPos x_1828 -> h_MinusPos x_1828
 256
 257 (** val minusresult_rect_Type1 :
 258     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 259 let rec minusresult_rect_Type1 h_MinusNeg h_MinusZero h_MinusPos = function
 260 | MinusNeg -> h_MinusNeg
 261 | MinusZero -> h_MinusZero
 262 | MinusPos x_1833 -> h_MinusPos x_1833
 263
 264 (** val minusresult_rect_Type0 :
 265     'a1 -> 'a1 -> (pos -> 'a1) -> minusresult -> 'a1 **)
 266 let rec minusresult_rect_Type0 h_MinusNeg h_MinusZero h_MinusPos = function
 267 | MinusNeg -> h_MinusNeg
 268 | MinusZero -> h_MinusZero
 269 | MinusPos x_1838 -> h_MinusPos x_1838
 270
 271 (** val minusresult_inv_rect_Type4 :
 272     minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
 273 let minusresult_inv_rect_Type4 hterm h1 h2 h3 =
 274   let hcut = minusresult_rect_Type4 h1 h2 h3 hterm in hcut __
 275
 276 (** val minusresult_inv_rect_Type3 :
 277     minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
 278 let minusresult_inv_rect_Type3 hterm h1 h2 h3 =
 279   let hcut = minusresult_rect_Type3 h1 h2 h3 hterm in hcut __
 280
 281 (** val minusresult_inv_rect_Type2 :
 282     minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
 283 let minusresult_inv_rect_Type2 hterm h1 h2 h3 =
 284   let hcut = minusresult_rect_Type2 h1 h2 h3 hterm in hcut __
 285
 286 (** val minusresult_inv_rect_Type1 :
 287     minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
 288 let minusresult_inv_rect_Type1 hterm h1 h2 h3 =
 289   let hcut = minusresult_rect_Type1 h1 h2 h3 hterm in hcut __
 290
 291 (** val minusresult_inv_rect_Type0 :
 292     minusresult -> (__ -> 'a1) -> (__ -> 'a1) -> (pos -> __ -> 'a1) -> 'a1 **)
 293 let minusresult_inv_rect_Type0 hterm h1 h2 h3 =
 294   let hcut = minusresult_rect_Type0 h1 h2 h3 hterm in hcut __
 295
 296 (** val minusresult_discr : minusresult -> minusresult -> __ **)
 297 let minusresult_discr x y =
 298   Logic.eq_rect_Type2 x
 299     (match x with
 300      | MinusNeg -> Obj.magic (fun _ dH -> dH)
 301      | MinusZero -> Obj.magic (fun _ dH -> dH)
 302      | MinusPos a0 -> Obj.magic (fun _ dH -> dH __)) y
 303
 304 (** val partial_minus : pos -> pos -> minusresult **)
 305 let rec partial_minus n m =
 306   match n with
 307   | One ->
 308     (match m with
 309      | One -> MinusZero
 310      | P1 x -> MinusNeg
 311      | P0 x -> MinusNeg)
 312   | P1 n' ->
 313     (match m with
 314      | One -> MinusPos (P0 n')
 315      | P1 m' ->
 316        (match partial_minus n' m' with
 317         | MinusNeg -> MinusNeg
 318         | MinusZero -> MinusZero
 319         | MinusPos p -> MinusPos (P0 p))
 320      | P0 m' ->
 321        (match partial_minus n' m' with
 322         | MinusNeg -> MinusNeg
 323         | MinusZero -> MinusPos One
 324         | MinusPos p -> MinusPos (P1 p)))
 325   | P0 n' ->
 326     (match m with
 327      | One -> MinusPos (pred n)
 328      | P1 m' ->
 329        (match partial_minus n' m' with
 330         | MinusNeg -> MinusNeg
 331         | MinusZero -> MinusNeg
 332         | MinusPos p -> MinusPos (pred (P0 p)))
 333      | P0 m' ->
 334        (match partial_minus n' m' with
 335         | MinusNeg -> MinusNeg
 336         | MinusZero -> MinusZero
 337         | MinusPos p -> MinusPos (P0 p)))
 338
 339 (** val minus : pos -> pos -> pos **)
 340 let minus n m =
 341   match partial_minus n m with
 342   | MinusNeg -> One
 343   | MinusZero -> One
 344   | MinusPos p -> p
 345
 346 (** val eqb : pos -> pos -> Bool.bool **)
 347 let rec eqb n m =
 348   match n with
 349   | One ->
 350     (match m with
 351      | One -> Bool.True
 352      | P1 x -> Bool.False
 353      | P0 x -> Bool.False)
 354   | P1 p ->
 355     (match m with
 356      | One -> Bool.False
 357      | P1 q -> eqb p q
 358      | P0 x -> Bool.False)
 359   | P0 p ->
 360     (match m with
 361      | One -> Bool.False
 362      | P1 x -> Bool.False
 363      | P0 q -> eqb p q)
 364
 365 (** val eqb_elim : pos -> pos -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 366 let eqb_elim n m x x0 =
 367   pos_rect_Type1 (fun m0 ->
 368     match m0 with
 369     | One -> (fun _ auto auto' -> auto __)
 370     | P1 m' -> (fun _ t f -> f __)
 371     | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
 372     match m0 with
 373     | One -> (fun _ t f -> f __)
 374     | P1 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))
 375     | P0 m' -> (fun _ t f -> f __)) (fun n' iH m0 ->
 376     match m0 with
 377     | One -> (fun _ t f -> f __)
 378     | P1 m' -> (fun _ t f -> f __)
 379     | P0 m' -> (fun _ t f -> iH m' __ (fun _ -> t __) (fun _ -> f __))) n m
 380     __ x x0
 381
 382 (** val leb : pos -> pos -> Bool.bool **)
 383 let rec leb n m =
 384   match partial_minus n m with
 385   | MinusNeg -> Bool.True
 386   | MinusZero -> Bool.True
 387   | MinusPos x -> Bool.False
 388
 389 (** val pos_compare : pos -> pos -> compare **)
 390 let pos_compare n m =
 391   match partial_minus n m with
 392   | MinusNeg -> LT
 393   | MinusZero -> EQ
 394   | MinusPos x -> GT
 395
 396 (** val two_power_nat : Nat.nat -> pos **)
 397 let rec two_power_nat = function
 398 | Nat.O -> One
 399 | Nat.S n' -> P0 (two_power_nat n')
 400
 401 (** val two_power_pos : pos -> pos **)
 402 let two_power_pos p =
 403   two_power_nat (nat_of_pos p)
 404
 405 (** val max : pos -> pos -> pos **)
 406 let max n m =
 407   match leb n m with
 408   | Bool.True -> m
 409   | Bool.False -> n
 410