extracted/div_and_mod.ml

   1 open Preamble
   2
   3 open Bool
   4
   5 open Hints_declaration
   6
   7 open Core_notation
   8
   9 open Pts
  10
  11 open Logic
  12
  13 open Relations
  14
  15 open Nat
  16
  17 (** val mod_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
  18 let rec mod_aux p m n =
  19   match p with
  20   | Nat.O -> m
  21   | Nat.S q ->
  22     (match Nat.leb m n with
  23      | Bool.True -> m
  24      | Bool.False -> mod_aux q (Nat.minus m (Nat.S n)) n)
  25
  26 (** val mod0 : Nat.nat -> Nat.nat -> Nat.nat **)
  27 let mod0 n = function
  28 | Nat.O -> n
  29 | Nat.S p -> mod_aux n n p
  30
  31 (** val div_aux : Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat **)
  32 let rec div_aux p m n =
  33   match p with
  34   | Nat.O -> Nat.O
  35   | Nat.S q ->
  36     (match Nat.leb m n with
  37      | Bool.True -> Nat.O
  38      | Bool.False -> Nat.S (div_aux q (Nat.minus m (Nat.S n)) n))
  39
  40 (** val div : Nat.nat -> Nat.nat -> Nat.nat **)
  41 let div n = function
  42 | Nat.O -> Nat.S n
  43 | Nat.S p -> div_aux n n p
  44
  45 (** val div_mod_spec_rect_Type4 :
  46     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  47 let rec div_mod_spec_rect_Type4 n m q r h_div_mod_spec_intro =
  48   h_div_mod_spec_intro __ __
  49
  50 (** val div_mod_spec_rect_Type5 :
  51     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  52 let rec div_mod_spec_rect_Type5 n m q r h_div_mod_spec_intro =
  53   h_div_mod_spec_intro __ __
  54
  55 (** val div_mod_spec_rect_Type3 :
  56     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  57 let rec div_mod_spec_rect_Type3 n m q r h_div_mod_spec_intro =
  58   h_div_mod_spec_intro __ __
  59
  60 (** val div_mod_spec_rect_Type2 :
  61     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  62 let rec div_mod_spec_rect_Type2 n m q r h_div_mod_spec_intro =
  63   h_div_mod_spec_intro __ __
  64
  65 (** val div_mod_spec_rect_Type1 :
  66     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  67 let rec div_mod_spec_rect_Type1 n m q r h_div_mod_spec_intro =
  68   h_div_mod_spec_intro __ __
  69
  70 (** val div_mod_spec_rect_Type0 :
  71     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> 'a1) -> 'a1 **)
  72 let rec div_mod_spec_rect_Type0 n m q r h_div_mod_spec_intro =
  73   h_div_mod_spec_intro __ __
  74
  75 (** val div_mod_spec_inv_rect_Type4 :
  76     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
  77     'a1 **)
  78 let div_mod_spec_inv_rect_Type4 x1 x2 x3 x4 h1 =
  79   let hcut = div_mod_spec_rect_Type4 x1 x2 x3 x4 h1 in hcut __
  80
  81 (** val div_mod_spec_inv_rect_Type3 :
  82     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
  83     'a1 **)
  84 let div_mod_spec_inv_rect_Type3 x1 x2 x3 x4 h1 =
  85   let hcut = div_mod_spec_rect_Type3 x1 x2 x3 x4 h1 in hcut __
  86
  87 (** val div_mod_spec_inv_rect_Type2 :
  88     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
  89     'a1 **)
  90 let div_mod_spec_inv_rect_Type2 x1 x2 x3 x4 h1 =
  91   let hcut = div_mod_spec_rect_Type2 x1 x2 x3 x4 h1 in hcut __
  92
  93 (** val div_mod_spec_inv_rect_Type1 :
  94     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
  95     'a1 **)
  96 let div_mod_spec_inv_rect_Type1 x1 x2 x3 x4 h1 =
  97   let hcut = div_mod_spec_rect_Type1 x1 x2 x3 x4 h1 in hcut __
  98
  99 (** val div_mod_spec_inv_rect_Type0 :
 100     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> (__ -> __ -> __ -> 'a1) ->
 101     'a1 **)
 102 let div_mod_spec_inv_rect_Type0 x1 x2 x3 x4 h1 =
 103   let hcut = div_mod_spec_rect_Type0 x1 x2 x3 x4 h1 in hcut __
 104
 105 (** val div_mod_spec_discr :
 106     Nat.nat -> Nat.nat -> Nat.nat -> Nat.nat -> __ **)
 107 let div_mod_spec_discr a1 a2 a3 a4 =
 108   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
 109