extracted/extranat.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 Jmeq
  20
  21 open Russell
  22
  23 open List
  24
  25 open Setoids
  26
  27 open Monad
  28
  29 open Option
  30
  31 (** val nat_bound_opt : Nat.nat -> Nat.nat -> __ Types.option **)
  32 let rec nat_bound_opt n n0 =
  33   match n with
  34   | Nat.O -> Types.None
  35   | Nat.S n' ->
  36     (match n0 with
  37      | Nat.O -> Obj.magic (Monad.m_return0 (Monad.max_def Option.option) __)
  38      | Nat.S n'0 ->
  39        Obj.magic
  40          (Monad.m_bind0 (Monad.max_def Option.option)
  41            (Obj.magic (nat_bound_opt n' n'0)) (fun _ ->
  42            Monad.m_return0 (Monad.max_def Option.option) __)))
  43
  44 type nat_compared =
  45 | Nat_lt of Nat.nat * Nat.nat
  46 | Nat_eq of Nat.nat
  47 | Nat_gt of Nat.nat * Nat.nat
  48
  49 (** val nat_compared_rect_Type4 :
  50     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  51     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  52 let rec nat_compared_rect_Type4 h_nat_lt h_nat_eq h_nat_gt x_1125 x_1124 = function
  53 | Nat_lt (n, m) -> h_nat_lt n m
  54 | Nat_eq n -> h_nat_eq n
  55 | Nat_gt (n, m) -> h_nat_gt n m
  56
  57 (** val nat_compared_rect_Type5 :
  58     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  59     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  60 let rec nat_compared_rect_Type5 h_nat_lt h_nat_eq h_nat_gt x_1131 x_1130 = function
  61 | Nat_lt (n, m) -> h_nat_lt n m
  62 | Nat_eq n -> h_nat_eq n
  63 | Nat_gt (n, m) -> h_nat_gt n m
  64
  65 (** val nat_compared_rect_Type3 :
  66     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  67     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  68 let rec nat_compared_rect_Type3 h_nat_lt h_nat_eq h_nat_gt x_1137 x_1136 = function
  69 | Nat_lt (n, m) -> h_nat_lt n m
  70 | Nat_eq n -> h_nat_eq n
  71 | Nat_gt (n, m) -> h_nat_gt n m
  72
  73 (** val nat_compared_rect_Type2 :
  74     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  75     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  76 let rec nat_compared_rect_Type2 h_nat_lt h_nat_eq h_nat_gt x_1143 x_1142 = function
  77 | Nat_lt (n, m) -> h_nat_lt n m
  78 | Nat_eq n -> h_nat_eq n
  79 | Nat_gt (n, m) -> h_nat_gt n m
  80
  81 (** val nat_compared_rect_Type1 :
  82     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  83     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  84 let rec nat_compared_rect_Type1 h_nat_lt h_nat_eq h_nat_gt x_1149 x_1148 = function
  85 | Nat_lt (n, m) -> h_nat_lt n m
  86 | Nat_eq n -> h_nat_eq n
  87 | Nat_gt (n, m) -> h_nat_gt n m
  88
  89 (** val nat_compared_rect_Type0 :
  90     (Nat.nat -> Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> (Nat.nat -> Nat.nat ->
  91     'a1) -> Nat.nat -> Nat.nat -> nat_compared -> 'a1 **)
  92 let rec nat_compared_rect_Type0 h_nat_lt h_nat_eq h_nat_gt x_1155 x_1154 = function
  93 | Nat_lt (n, m) -> h_nat_lt n m
  94 | Nat_eq n -> h_nat_eq n
  95 | Nat_gt (n, m) -> h_nat_gt n m
  96
  97 (** val nat_compared_inv_rect_Type4 :
  98     Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
  99     __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
 100     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 101 let nat_compared_inv_rect_Type4 x1 x2 hterm h1 h2 h3 =
 102   let hcut = nat_compared_rect_Type4 h1 h2 h3 x1 x2 hterm in hcut __ __ __
 103
 104 (** val nat_compared_inv_rect_Type3 :
 105     Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
 106     __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
 107     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 108 let nat_compared_inv_rect_Type3 x1 x2 hterm h1 h2 h3 =
 109   let hcut = nat_compared_rect_Type3 h1 h2 h3 x1 x2 hterm in hcut __ __ __
 110
 111 (** val nat_compared_inv_rect_Type2 :
 112     Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
 113     __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
 114     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 115 let nat_compared_inv_rect_Type2 x1 x2 hterm h1 h2 h3 =
 116   let hcut = nat_compared_rect_Type2 h1 h2 h3 x1 x2 hterm in hcut __ __ __
 117
 118 (** val nat_compared_inv_rect_Type1 :
 119     Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
 120     __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
 121     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 122 let nat_compared_inv_rect_Type1 x1 x2 hterm h1 h2 h3 =
 123   let hcut = nat_compared_rect_Type1 h1 h2 h3 x1 x2 hterm in hcut __ __ __
 124
 125 (** val nat_compared_inv_rect_Type0 :
 126     Nat.nat -> Nat.nat -> nat_compared -> (Nat.nat -> Nat.nat -> __ -> __ ->
 127     __ -> 'a1) -> (Nat.nat -> __ -> __ -> __ -> 'a1) -> (Nat.nat -> Nat.nat
 128     -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 129 let nat_compared_inv_rect_Type0 x1 x2 hterm h1 h2 h3 =
 130   let hcut = nat_compared_rect_Type0 h1 h2 h3 x1 x2 hterm in hcut __ __ __
 131
 132 (** val nat_compared_discr :
 133     Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
 134 let nat_compared_discr a1 a2 x y =
 135   Logic.eq_rect_Type2 x
 136     (match x with
 137      | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 138      | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
 139      | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 140
 141 (** val nat_compared_jmdiscr :
 142     Nat.nat -> Nat.nat -> nat_compared -> nat_compared -> __ **)
 143 let nat_compared_jmdiscr a1 a2 x y =
 144   Logic.eq_rect_Type2 x
 145     (match x with
 146      | Nat_lt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)
 147      | Nat_eq a0 -> Obj.magic (fun _ dH -> dH __)
 148      | Nat_gt (a0, a10) -> Obj.magic (fun _ dH -> dH __ __)) y
 149
 150 (** val nat_compare : Nat.nat -> Nat.nat -> nat_compared **)
 151 let rec nat_compare n m =
 152   match n with
 153   | Nat.O ->
 154     (match m with
 155      | Nat.O -> Nat_eq Nat.O
 156      | Nat.S m' -> Nat_lt (Nat.O, m'))
 157   | Nat.S n' ->
 158     (match m with
 159      | Nat.O -> Nat_gt (n', Nat.O)
 160      | Nat.S m' ->
 161        (match nat_compare n' m' with
 162         | Nat_lt (x, y) -> Nat_lt ((Nat.S x), y)
 163         | Nat_eq x -> Nat_eq (Nat.S x)
 164         | Nat_gt (x, y) -> Nat_gt (x, (Nat.S y))))
 165
 166 (** val eq_nat_dec : Nat.nat -> Nat.nat -> (__, __) Types.sum **)
 167 let rec eq_nat_dec n m =
 168   match n with
 169   | Nat.O ->
 170     (match m with
 171      | Nat.O -> Types.Inl __
 172      | Nat.S m' -> Types.Inr __)
 173   | Nat.S n' ->
 174     (match m with
 175      | Nat.O -> Types.Inr __
 176      | Nat.S m' ->
 177        (match eq_nat_dec n' m' with
 178         | Types.Inl _ -> Types.Inl __
 179         | Types.Inr _ -> Types.Inr __))
 180