[2601] | 1 | open Preamble |
---|
| 2 | |
---|
| 3 | open Bool |
---|
| 4 | |
---|
| 5 | open Relations |
---|
| 6 | |
---|
| 7 | open Nat |
---|
| 8 | |
---|
| 9 | open Hints_declaration |
---|
| 10 | |
---|
| 11 | open Core_notation |
---|
| 12 | |
---|
| 13 | open Pts |
---|
| 14 | |
---|
| 15 | open Logic |
---|
| 16 | |
---|
| 17 | open Positive |
---|
| 18 | |
---|
| 19 | type z = |
---|
| 20 | | OZ |
---|
| 21 | | Pos of Positive.pos |
---|
| 22 | | Neg of Positive.pos |
---|
| 23 | |
---|
| 24 | (** val z_rect_Type4 : |
---|
| 25 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 26 | let rec z_rect_Type4 h_OZ h_pos h_neg = function |
---|
| 27 | | OZ -> h_OZ |
---|
[2797] | 28 | | Pos x_4656 -> h_pos x_4656 |
---|
| 29 | | Neg x_4657 -> h_neg x_4657 |
---|
[2601] | 30 | |
---|
| 31 | (** val z_rect_Type5 : |
---|
| 32 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 33 | let rec z_rect_Type5 h_OZ h_pos h_neg = function |
---|
| 34 | | OZ -> h_OZ |
---|
[2797] | 35 | | Pos x_4662 -> h_pos x_4662 |
---|
| 36 | | Neg x_4663 -> h_neg x_4663 |
---|
[2601] | 37 | |
---|
| 38 | (** val z_rect_Type3 : |
---|
| 39 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 40 | let rec z_rect_Type3 h_OZ h_pos h_neg = function |
---|
| 41 | | OZ -> h_OZ |
---|
[2797] | 42 | | Pos x_4668 -> h_pos x_4668 |
---|
| 43 | | Neg x_4669 -> h_neg x_4669 |
---|
[2601] | 44 | |
---|
| 45 | (** val z_rect_Type2 : |
---|
| 46 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 47 | let rec z_rect_Type2 h_OZ h_pos h_neg = function |
---|
| 48 | | OZ -> h_OZ |
---|
[2797] | 49 | | Pos x_4674 -> h_pos x_4674 |
---|
| 50 | | Neg x_4675 -> h_neg x_4675 |
---|
[2601] | 51 | |
---|
| 52 | (** val z_rect_Type1 : |
---|
| 53 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 54 | let rec z_rect_Type1 h_OZ h_pos h_neg = function |
---|
| 55 | | OZ -> h_OZ |
---|
[2797] | 56 | | Pos x_4680 -> h_pos x_4680 |
---|
| 57 | | Neg x_4681 -> h_neg x_4681 |
---|
[2601] | 58 | |
---|
| 59 | (** val z_rect_Type0 : |
---|
| 60 | 'a1 -> (Positive.pos -> 'a1) -> (Positive.pos -> 'a1) -> z -> 'a1 **) |
---|
| 61 | let rec z_rect_Type0 h_OZ h_pos h_neg = function |
---|
| 62 | | OZ -> h_OZ |
---|
[2797] | 63 | | Pos x_4686 -> h_pos x_4686 |
---|
| 64 | | Neg x_4687 -> h_neg x_4687 |
---|
[2601] | 65 | |
---|
| 66 | (** val z_inv_rect_Type4 : |
---|
| 67 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 68 | 'a1) -> 'a1 **) |
---|
| 69 | let z_inv_rect_Type4 hterm h1 h2 h3 = |
---|
| 70 | let hcut = z_rect_Type4 h1 h2 h3 hterm in hcut __ |
---|
| 71 | |
---|
| 72 | (** val z_inv_rect_Type3 : |
---|
| 73 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 74 | 'a1) -> 'a1 **) |
---|
| 75 | let z_inv_rect_Type3 hterm h1 h2 h3 = |
---|
| 76 | let hcut = z_rect_Type3 h1 h2 h3 hterm in hcut __ |
---|
| 77 | |
---|
| 78 | (** val z_inv_rect_Type2 : |
---|
| 79 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 80 | 'a1) -> 'a1 **) |
---|
| 81 | let z_inv_rect_Type2 hterm h1 h2 h3 = |
---|
| 82 | let hcut = z_rect_Type2 h1 h2 h3 hterm in hcut __ |
---|
| 83 | |
---|
| 84 | (** val z_inv_rect_Type1 : |
---|
| 85 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 86 | 'a1) -> 'a1 **) |
---|
| 87 | let z_inv_rect_Type1 hterm h1 h2 h3 = |
---|
| 88 | let hcut = z_rect_Type1 h1 h2 h3 hterm in hcut __ |
---|
| 89 | |
---|
| 90 | (** val z_inv_rect_Type0 : |
---|
| 91 | z -> (__ -> 'a1) -> (Positive.pos -> __ -> 'a1) -> (Positive.pos -> __ -> |
---|
| 92 | 'a1) -> 'a1 **) |
---|
| 93 | let z_inv_rect_Type0 hterm h1 h2 h3 = |
---|
| 94 | let hcut = z_rect_Type0 h1 h2 h3 hterm in hcut __ |
---|
| 95 | |
---|
| 96 | (** val z_discr : z -> z -> __ **) |
---|
| 97 | let z_discr x y = |
---|
| 98 | Logic.eq_rect_Type2 x |
---|
| 99 | (match x with |
---|
| 100 | | OZ -> Obj.magic (fun _ dH -> dH) |
---|
| 101 | | Pos a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 102 | | Neg a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
| 103 | |
---|
| 104 | (** val z_of_nat : Nat.nat -> z **) |
---|
| 105 | let z_of_nat = function |
---|
| 106 | | Nat.O -> OZ |
---|
| 107 | | Nat.S n0 -> Pos (Positive.succ_pos_of_nat n0) |
---|
| 108 | |
---|
| 109 | (** val neg_Z_of_nat : Nat.nat -> z **) |
---|
| 110 | let neg_Z_of_nat = function |
---|
| 111 | | Nat.O -> OZ |
---|
| 112 | | Nat.S n0 -> Neg (Positive.succ_pos_of_nat n0) |
---|
| 113 | |
---|
| 114 | (** val abs : z -> Nat.nat **) |
---|
| 115 | let abs = function |
---|
| 116 | | OZ -> Nat.O |
---|
| 117 | | Pos n -> Positive.nat_of_pos n |
---|
| 118 | | Neg n -> Positive.nat_of_pos n |
---|
| 119 | |
---|
| 120 | (** val oZ_test : z -> Bool.bool **) |
---|
| 121 | let oZ_test = function |
---|
| 122 | | OZ -> Bool.True |
---|
| 123 | | Pos x -> Bool.False |
---|
| 124 | | Neg x -> Bool.False |
---|
| 125 | |
---|
| 126 | (** val zsucc : z -> z **) |
---|
| 127 | let zsucc = function |
---|
| 128 | | OZ -> Pos Positive.One |
---|
| 129 | | Pos n -> Pos (Positive.succ n) |
---|
| 130 | | Neg n -> |
---|
| 131 | (match n with |
---|
| 132 | | Positive.One -> OZ |
---|
[2773] | 133 | | Positive.P1 x -> Neg (Positive.pred n) |
---|
| 134 | | Positive.P0 x -> Neg (Positive.pred n)) |
---|
[2601] | 135 | |
---|
| 136 | (** val zpred : z -> z **) |
---|
| 137 | let zpred = function |
---|
| 138 | | OZ -> Neg Positive.One |
---|
| 139 | | Pos n -> |
---|
| 140 | (match n with |
---|
| 141 | | Positive.One -> OZ |
---|
[2773] | 142 | | Positive.P1 x -> Pos (Positive.pred n) |
---|
| 143 | | Positive.P0 x -> Pos (Positive.pred n)) |
---|
[2601] | 144 | | Neg n -> Neg (Positive.succ n) |
---|
| 145 | |
---|
| 146 | (** val eqZb : z -> z -> Bool.bool **) |
---|
| 147 | let rec eqZb x y = |
---|
| 148 | match x with |
---|
| 149 | | OZ -> |
---|
| 150 | (match y with |
---|
| 151 | | OZ -> Bool.True |
---|
| 152 | | Pos q -> Bool.False |
---|
| 153 | | Neg q -> Bool.False) |
---|
| 154 | | Pos p -> |
---|
| 155 | (match y with |
---|
| 156 | | OZ -> Bool.False |
---|
[2773] | 157 | | Pos q -> Positive.eqb p q |
---|
[2601] | 158 | | Neg q -> Bool.False) |
---|
| 159 | | Neg p -> |
---|
| 160 | (match y with |
---|
| 161 | | OZ -> Bool.False |
---|
| 162 | | Pos q -> Bool.False |
---|
[2773] | 163 | | Neg q -> Positive.eqb p q) |
---|
[2601] | 164 | |
---|
| 165 | (** val z_compare : z -> z -> Positive.compare **) |
---|
| 166 | let rec z_compare x y = |
---|
| 167 | match x with |
---|
| 168 | | OZ -> |
---|
| 169 | (match y with |
---|
| 170 | | OZ -> Positive.EQ |
---|
| 171 | | Pos m -> Positive.LT |
---|
| 172 | | Neg m -> Positive.GT) |
---|
| 173 | | Pos n -> |
---|
| 174 | (match y with |
---|
| 175 | | OZ -> Positive.GT |
---|
| 176 | | Pos m -> Positive.pos_compare n m |
---|
| 177 | | Neg m -> Positive.GT) |
---|
| 178 | | Neg n -> |
---|
| 179 | (match y with |
---|
| 180 | | OZ -> Positive.LT |
---|
| 181 | | Pos m -> Positive.LT |
---|
| 182 | | Neg m -> Positive.pos_compare m n) |
---|
| 183 | |
---|
| 184 | (** val zplus : z -> z -> z **) |
---|
| 185 | let rec zplus x y = |
---|
| 186 | match x with |
---|
| 187 | | OZ -> y |
---|
| 188 | | Pos m -> |
---|
| 189 | (match y with |
---|
| 190 | | OZ -> x |
---|
[2773] | 191 | | Pos n -> Pos (Positive.plus m n) |
---|
[2601] | 192 | | Neg n -> |
---|
| 193 | (match Positive.pos_compare m n with |
---|
[2773] | 194 | | Positive.LT -> Neg (Positive.minus n m) |
---|
[2601] | 195 | | Positive.EQ -> OZ |
---|
[2773] | 196 | | Positive.GT -> Pos (Positive.minus m n))) |
---|
[2601] | 197 | | Neg m -> |
---|
| 198 | (match y with |
---|
| 199 | | OZ -> x |
---|
| 200 | | Pos n -> |
---|
| 201 | (match Positive.pos_compare m n with |
---|
[2773] | 202 | | Positive.LT -> Pos (Positive.minus n m) |
---|
[2601] | 203 | | Positive.EQ -> OZ |
---|
[2773] | 204 | | Positive.GT -> Neg (Positive.minus m n)) |
---|
| 205 | | Neg n -> Neg (Positive.plus m n)) |
---|
[2601] | 206 | |
---|
| 207 | (** val zopp : z -> z **) |
---|
| 208 | let zopp = function |
---|
| 209 | | OZ -> OZ |
---|
| 210 | | Pos n -> Neg n |
---|
| 211 | | Neg n -> Pos n |
---|
| 212 | |
---|
| 213 | (** val zminus : z -> z -> z **) |
---|
| 214 | let zminus x y = |
---|
| 215 | zplus x (zopp y) |
---|
| 216 | |
---|
| 217 | (** val z_two_power_nat : Nat.nat -> z **) |
---|
| 218 | let z_two_power_nat n = |
---|
| 219 | Pos (Positive.two_power_nat n) |
---|
| 220 | |
---|
| 221 | (** val z_two_power_pos : Positive.pos -> z **) |
---|
| 222 | let z_two_power_pos n = |
---|
| 223 | Pos (Positive.two_power_pos n) |
---|
| 224 | |
---|
| 225 | (** val two_p : z -> z **) |
---|
| 226 | let two_p = function |
---|
| 227 | | OZ -> Pos Positive.One |
---|
| 228 | | Pos p -> Pos (Positive.two_power_pos p) |
---|
| 229 | | Neg x -> OZ |
---|
| 230 | |
---|
| 231 | open Types |
---|
| 232 | |
---|
| 233 | (** val decidable_eq_Z_Type : z -> z -> (__, __) Types.sum **) |
---|
| 234 | let decidable_eq_Z_Type z1 z2 = |
---|
| 235 | (match eqZb z1 z2 with |
---|
| 236 | | Bool.True -> (fun _ -> Types.Inl __) |
---|
| 237 | | Bool.False -> (fun _ -> Types.Inr __)) __ |
---|
| 238 | |
---|
| 239 | (** val zleb : z -> z -> Bool.bool **) |
---|
| 240 | let rec zleb x y = |
---|
| 241 | match x with |
---|
| 242 | | OZ -> |
---|
| 243 | (match y with |
---|
| 244 | | OZ -> Bool.True |
---|
| 245 | | Pos m -> Bool.True |
---|
| 246 | | Neg m -> Bool.False) |
---|
| 247 | | Pos n -> |
---|
| 248 | (match y with |
---|
| 249 | | OZ -> Bool.False |
---|
[2773] | 250 | | Pos m -> Positive.leb n m |
---|
[2601] | 251 | | Neg m -> Bool.False) |
---|
| 252 | | Neg n -> |
---|
| 253 | (match y with |
---|
| 254 | | OZ -> Bool.True |
---|
| 255 | | Pos m -> Bool.True |
---|
[2773] | 256 | | Neg m -> Positive.leb m n) |
---|
[2601] | 257 | |
---|
| 258 | (** val zltb : z -> z -> Bool.bool **) |
---|
| 259 | let rec zltb x y = |
---|
| 260 | match x with |
---|
| 261 | | OZ -> |
---|
| 262 | (match y with |
---|
| 263 | | OZ -> Bool.False |
---|
| 264 | | Pos m -> Bool.True |
---|
| 265 | | Neg m -> Bool.False) |
---|
| 266 | | Pos n -> |
---|
| 267 | (match y with |
---|
| 268 | | OZ -> Bool.False |
---|
[2773] | 269 | | Pos m -> Positive.leb (Positive.succ n) m |
---|
[2601] | 270 | | Neg m -> Bool.False) |
---|
| 271 | | Neg n -> |
---|
| 272 | (match y with |
---|
| 273 | | OZ -> Bool.True |
---|
| 274 | | Pos m -> Bool.True |
---|
[2773] | 275 | | Neg m -> Positive.leb (Positive.succ m) n) |
---|
[2601] | 276 | |
---|
| 277 | (** val zleb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 278 | let zleb_elim_Type0 n m hle hnle = |
---|
| 279 | Bool.bool_rect_Type0 (fun _ -> hle __) (fun _ -> hnle __) (zleb n m) __ |
---|
| 280 | |
---|
| 281 | (** val zltb_elim_Type0 : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 282 | let zltb_elim_Type0 n m hlt hnlt = |
---|
| 283 | Bool.bool_rect_Type0 (fun _ -> hlt __) (fun _ -> hnlt __) (zltb n m) __ |
---|
| 284 | |
---|
| 285 | (** val z_times : z -> z -> z **) |
---|
| 286 | let rec z_times x y = |
---|
| 287 | match x with |
---|
| 288 | | OZ -> OZ |
---|
| 289 | | Pos n -> |
---|
| 290 | (match y with |
---|
| 291 | | OZ -> OZ |
---|
[2773] | 292 | | Pos m -> Pos (Positive.times n m) |
---|
| 293 | | Neg m -> Neg (Positive.times n m)) |
---|
[2601] | 294 | | Neg n -> |
---|
| 295 | (match y with |
---|
| 296 | | OZ -> OZ |
---|
[2773] | 297 | | Pos m -> Neg (Positive.times n m) |
---|
| 298 | | Neg m -> Pos (Positive.times n m)) |
---|
[2601] | 299 | |
---|
| 300 | (** val zmax : z -> z -> z **) |
---|
| 301 | let zmax x y = |
---|
| 302 | match z_compare x y with |
---|
| 303 | | Positive.LT -> y |
---|
| 304 | | Positive.EQ -> x |
---|
| 305 | | Positive.GT -> x |
---|
| 306 | |
---|