From 7da3e3d85c88eb42e932230048cb0db255474b5d Mon Sep 17 00:00:00 2001 From: fbesson Date: Fri, 20 May 2011 17:01:54 +0000 Subject: added support to handle division by a constant over R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/micromega.ml | 3371 ++++++++++++++++++++++++++++++++++------ 1 file changed, 2856 insertions(+), 515 deletions(-) (limited to 'plugins/micromega/micromega.ml') diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml index 39b6cd2a3..564126d24 100644 --- a/plugins/micromega/micromega.ml +++ b/plugins/micromega/micromega.ml @@ -1,3 +1,6 @@ +type __ = Obj.t +let __ = let rec f _ = Obj.repr f in Obj.repr f + (** val negb : bool -> bool **) let negb = function @@ -8,6 +11,23 @@ type nat = | O | S of nat +(** val fst : ('a1 * 'a2) -> 'a1 **) + +let fst = function +| x,y -> x + +(** val snd : ('a1 * 'a2) -> 'a2 **) + +let snd = function +| x,y -> y + +(** val app : 'a1 list -> 'a1 list -> 'a1 list **) + +let rec app l m = + match l with + | [] -> m + | a::l1 -> a::(app l1 m) + type comparison = | Eq | Lt @@ -20,12 +40,28 @@ let compOpp = function | Lt -> Gt | Gt -> Lt -(** val app : 'a1 list -> 'a1 list -> 'a1 list **) +type compareSpecT = +| CompEqT +| CompLtT +| CompGtT -let rec app l m = - match l with - | [] -> m - | a::l1 -> a::(app l1 m) +(** val compareSpec2Type : comparison -> compareSpecT **) + +let compareSpec2Type = function +| Eq -> CompEqT +| Lt -> CompLtT +| Gt -> CompGtT + +type 'a compSpecT = compareSpecT + +(** val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT **) + +let compSpec2Type x y c = + compareSpec2Type c + +type 'a sig0 = + 'a + (* singleton inductive, whose constructor was exist *) (** val plus : nat -> nat -> nat **) @@ -34,181 +70,1927 @@ let rec plus n0 m = | O -> m | S p -> S (plus p m) +(** val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) + +let rec nat_iter n0 f x = + match n0 with + | O -> x + | S n' -> f (nat_iter n' f x) + type positive = | XI of positive | XO of positive | XH -(** val psucc : positive -> positive **) - -let rec psucc = function -| XI p -> XO (psucc p) -| XO p -> XI p -| XH -> XO XH - -(** val pplus : positive -> positive -> positive **) - -let rec pplus x y = - match x with - | XI p -> - (match y with - | XI q0 -> XO (pplus_carry p q0) - | XO q0 -> XI (pplus p q0) - | XH -> XO (psucc p)) - | XO p -> - (match y with - | XI q0 -> XI (pplus p q0) - | XO q0 -> XO (pplus p q0) - | XH -> XI p) - | XH -> - (match y with - | XI q0 -> XO (psucc q0) - | XO q0 -> XI q0 - | XH -> XO XH) - -(** val pplus_carry : positive -> positive -> positive **) - -and pplus_carry x y = - match x with - | XI p -> - (match y with - | XI q0 -> XI (pplus_carry p q0) - | XO q0 -> XO (pplus_carry p q0) - | XH -> XI (psucc p)) - | XO p -> - (match y with - | XI q0 -> XO (pplus_carry p q0) - | XO q0 -> XI (pplus p q0) - | XH -> XO (psucc p)) - | XH -> - (match y with - | XI q0 -> XI (psucc q0) - | XO q0 -> XO (psucc q0) - | XH -> XI XH) - -(** val p_of_succ_nat : nat -> positive **) - -let rec p_of_succ_nat = function -| O -> XH -| S x -> psucc (p_of_succ_nat x) - -(** val pdouble_minus_one : positive -> positive **) - -let rec pdouble_minus_one = function -| XI p -> XI (XO p) -| XO p -> XI (pdouble_minus_one p) -| XH -> XH - -type positive_mask = -| IsNul -| IsPos of positive -| IsNeg - -(** val pdouble_plus_one_mask : positive_mask -> positive_mask **) - -let pdouble_plus_one_mask = function -| IsNul -> IsPos XH -| IsPos p -> IsPos (XI p) -| IsNeg -> IsNeg - -(** val pdouble_mask : positive_mask -> positive_mask **) - -let pdouble_mask = function -| IsPos p -> IsPos (XO p) -| x0 -> x0 - -(** val pdouble_minus_two : positive -> positive_mask **) - -let pdouble_minus_two = function -| XI p -> IsPos (XO (XO p)) -| XO p -> IsPos (XO (pdouble_minus_one p)) -| XH -> IsNul - -(** val pminus_mask : positive -> positive -> positive_mask **) - -let rec pminus_mask x y = - match x with - | XI p -> - (match y with - | XI q0 -> pdouble_mask (pminus_mask p q0) - | XO q0 -> pdouble_plus_one_mask (pminus_mask p q0) - | XH -> IsPos (XO p)) - | XO p -> - (match y with - | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_mask (pminus_mask p q0) - | XH -> IsPos (pdouble_minus_one p)) - | XH -> - (match y with - | XH -> IsNul - | _ -> IsNeg) - -(** val pminus_mask_carry : positive -> positive -> positive_mask **) - -and pminus_mask_carry x y = - match x with - | XI p -> - (match y with - | XI q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_mask (pminus_mask p q0) - | XH -> IsPos (pdouble_minus_one p)) - | XO p -> - (match y with - | XI q0 -> pdouble_mask (pminus_mask_carry p q0) - | XO q0 -> pdouble_plus_one_mask (pminus_mask_carry p q0) - | XH -> pdouble_minus_two p) - | XH -> IsNeg - -(** val pminus : positive -> positive -> positive **) - -let pminus x y = - match pminus_mask x y with - | IsPos z0 -> z0 - | _ -> XH - -(** val pmult : positive -> positive -> positive **) - -let rec pmult x y = - match x with - | XI p -> pplus y (XO (pmult p y)) - | XO p -> XO (pmult p y) - | XH -> y - -(** val psize : positive -> nat **) - -let rec psize = function -| XI p2 -> S (psize p2) -| XO p2 -> S (psize p2) -| XH -> S O - -(** val pcompare : positive -> positive -> comparison -> comparison **) - -let rec pcompare x y r = - match x with - | XI p -> - (match y with - | XI q0 -> pcompare p q0 r - | XO q0 -> pcompare p q0 Gt - | XH -> Gt) - | XO p -> - (match y with - | XI q0 -> pcompare p q0 Lt - | XO q0 -> pcompare p q0 r - | XH -> Gt) - | XH -> - (match y with - | XH -> r - | _ -> Lt) - type n = | N0 | Npos of positive -(** val n_of_nat : nat -> n **) +type z = +| Z0 +| Zpos of positive +| Zneg of positive -let n_of_nat = function -| O -> N0 -| S n' -> Npos (p_of_succ_nat n') +module type TotalOrder' = + sig + type t + end + +module MakeOrderTac = + functor (O:TotalOrder') -> + struct + + end + +module MaxLogicalProperties = + functor (O:TotalOrder') -> + functor (M:sig + val max : O.t -> O.t -> O.t + end) -> + struct + module T = MakeOrderTac(O) + end + +module Pos = + struct + type t = positive + + (** val succ : positive -> positive **) + + let rec succ = function + | XI p -> XO (succ p) + | XO p -> XI p + | XH -> XO XH + + (** val add : positive -> positive -> positive **) + + let rec add x y = + match x with + | XI p -> + (match y with + | XI q0 -> XO (add_carry p q0) + | XO q0 -> XI (add p q0) + | XH -> XO (succ p)) + | XO p -> + (match y with + | XI q0 -> XI (add p q0) + | XO q0 -> XO (add p q0) + | XH -> XI p) + | XH -> + (match y with + | XI q0 -> XO (succ q0) + | XO q0 -> XI q0 + | XH -> XO XH) + + (** val add_carry : positive -> positive -> positive **) + + and add_carry x y = + match x with + | XI p -> + (match y with + | XI q0 -> XI (add_carry p q0) + | XO q0 -> XO (add_carry p q0) + | XH -> XI (succ p)) + | XO p -> + (match y with + | XI q0 -> XO (add_carry p q0) + | XO q0 -> XI (add p q0) + | XH -> XO (succ p)) + | XH -> + (match y with + | XI q0 -> XI (succ q0) + | XO q0 -> XO (succ q0) + | XH -> XI XH) + + (** val pred_double : positive -> positive **) + + let rec pred_double = function + | XI p -> XI (XO p) + | XO p -> XI (pred_double p) + | XH -> XH + + (** val pred : positive -> positive **) + + let pred = function + | XI p -> XO p + | XO p -> pred_double p + | XH -> XH + + (** val pred_N : positive -> n **) + + let pred_N = function + | XI p -> Npos (XO p) + | XO p -> Npos (pred_double p) + | XH -> N0 + + type mask = + | IsNul + | IsPos of positive + | IsNeg + + (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) + + let mask_rect f f0 f1 = function + | IsNul -> f + | IsPos x -> f0 x + | IsNeg -> f1 + + (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) + + let mask_rec f f0 f1 = function + | IsNul -> f + | IsPos x -> f0 x + | IsNeg -> f1 + + (** val succ_double_mask : mask -> mask **) + + let succ_double_mask = function + | IsNul -> IsPos XH + | IsPos p -> IsPos (XI p) + | IsNeg -> IsNeg + + (** val double_mask : mask -> mask **) + + let double_mask = function + | IsPos p -> IsPos (XO p) + | x0 -> x0 + + (** val double_pred_mask : positive -> mask **) + + let double_pred_mask = function + | XI p -> IsPos (XO (XO p)) + | XO p -> IsPos (XO (pred_double p)) + | XH -> IsNul + + (** val pred_mask : mask -> mask **) + + let pred_mask = function + | IsPos q0 -> + (match q0 with + | XH -> IsNul + | _ -> IsPos (pred q0)) + | _ -> IsNeg + + (** val sub_mask : positive -> positive -> mask **) + + let rec sub_mask x y = + match x with + | XI p -> + (match y with + | XI q0 -> double_mask (sub_mask p q0) + | XO q0 -> succ_double_mask (sub_mask p q0) + | XH -> IsPos (XO p)) + | XO p -> + (match y with + | XI q0 -> succ_double_mask (sub_mask_carry p q0) + | XO q0 -> double_mask (sub_mask p q0) + | XH -> IsPos (pred_double p)) + | XH -> + (match y with + | XH -> IsNul + | _ -> IsNeg) + + (** val sub_mask_carry : positive -> positive -> mask **) + + and sub_mask_carry x y = + match x with + | XI p -> + (match y with + | XI q0 -> succ_double_mask (sub_mask_carry p q0) + | XO q0 -> double_mask (sub_mask p q0) + | XH -> IsPos (pred_double p)) + | XO p -> + (match y with + | XI q0 -> double_mask (sub_mask_carry p q0) + | XO q0 -> succ_double_mask (sub_mask_carry p q0) + | XH -> double_pred_mask p) + | XH -> IsNeg + + (** val sub : positive -> positive -> positive **) + + let sub x y = + match sub_mask x y with + | IsPos z0 -> z0 + | _ -> XH + + (** val mul : positive -> positive -> positive **) + + let rec mul x y = + match x with + | XI p -> add y (XO (mul p y)) + | XO p -> XO (mul p y) + | XH -> y + + (** val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) + + let rec iter n0 f x = + match n0 with + | XI n' -> f (iter n' f (iter n' f x)) + | XO n' -> iter n' f (iter n' f x) + | XH -> f x + + (** val pow : positive -> positive -> positive **) + + let pow x y = + iter y (mul x) XH + + (** val div2 : positive -> positive **) + + let div2 = function + | XI p2 -> p2 + | XO p2 -> p2 + | XH -> XH + + (** val div2_up : positive -> positive **) + + let div2_up = function + | XI p2 -> succ p2 + | XO p2 -> p2 + | XH -> XH + + (** val size_nat : positive -> nat **) + + let rec size_nat = function + | XI p2 -> S (size_nat p2) + | XO p2 -> S (size_nat p2) + | XH -> S O + + (** val size : positive -> positive **) + + let rec size = function + | XI p2 -> succ (size p2) + | XO p2 -> succ (size p2) + | XH -> XH + + (** val compare_cont : positive -> positive -> comparison -> comparison **) + + let rec compare_cont x y r = + match x with + | XI p -> + (match y with + | XI q0 -> compare_cont p q0 r + | XO q0 -> compare_cont p q0 Gt + | XH -> Gt) + | XO p -> + (match y with + | XI q0 -> compare_cont p q0 Lt + | XO q0 -> compare_cont p q0 r + | XH -> Gt) + | XH -> + (match y with + | XH -> r + | _ -> Lt) + + (** val compare : positive -> positive -> comparison **) + + let compare x y = + compare_cont x y Eq + + (** val min : positive -> positive -> positive **) + + let min p p' = + match compare p p' with + | Gt -> p' + | _ -> p + + (** val max : positive -> positive -> positive **) + + let max p p' = + match compare p p' with + | Gt -> p + | _ -> p' + + (** val eqb : positive -> positive -> bool **) + + let rec eqb p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> eqb p2 q1 + | _ -> false) + | XO p2 -> + (match q0 with + | XO q1 -> eqb p2 q1 + | _ -> false) + | XH -> + (match q0 with + | XH -> true + | _ -> false) + + (** val leb : positive -> positive -> bool **) + + let leb x y = + match compare x y with + | Gt -> false + | _ -> true + + (** val ltb : positive -> positive -> bool **) + + let ltb x y = + match compare x y with + | Lt -> true + | _ -> false + + (** val sqrtrem_step : + (positive -> positive) -> (positive -> positive) -> (positive * mask) + -> positive * mask **) + + let sqrtrem_step f g = function + | s,y -> + (match y with + | IsPos r -> + let s' = XI (XO s) in + let r' = g (f r) in + if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r') + | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH)))) + + (** val sqrtrem : positive -> positive * mask **) + + let rec sqrtrem = function + | XI p2 -> + (match p2 with + | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3) + | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3) + | XH -> XH,(IsPos (XO XH))) + | XO p2 -> + (match p2 with + | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3) + | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3) + | XH -> XH,(IsPos XH)) + | XH -> XH,IsNul + + (** val sqrt : positive -> positive **) + + let sqrt p = + fst (sqrtrem p) + + (** val gcdn : nat -> positive -> positive -> positive **) + + let rec gcdn n0 a b = + match n0 with + | O -> XH + | S n1 -> + (match a with + | XI a' -> + (match b with + | XI b' -> + (match compare a' b' with + | Eq -> a + | Lt -> gcdn n1 (sub b' a') a + | Gt -> gcdn n1 (sub a' b') b) + | XO b0 -> gcdn n1 a b0 + | XH -> XH) + | XO a0 -> + (match b with + | XI p -> gcdn n1 a0 b + | XO b0 -> XO (gcdn n1 a0 b0) + | XH -> XH) + | XH -> XH) + + (** val gcd : positive -> positive -> positive **) + + let gcd a b = + gcdn (plus (size_nat a) (size_nat b)) a b + + (** val ggcdn : + nat -> positive -> positive -> positive * (positive * positive) **) + + let rec ggcdn n0 a b = + match n0 with + | O -> XH,(a,b) + | S n1 -> + (match a with + | XI a' -> + (match b with + | XI b' -> + (match compare a' b' with + | Eq -> a,(XH,XH) + | Lt -> + let g,p = ggcdn n1 (sub b' a') a in + let ba,aa = p in g,(aa,(add aa (XO ba))) + | Gt -> + let g,p = ggcdn n1 (sub a' b') b in + let ab,bb = p in g,((add bb (XO ab)),bb)) + | XO b0 -> + let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb)) + | XH -> XH,(a,XH)) + | XO a0 -> + (match b with + | XI p -> + let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb) + | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p + | XH -> XH,(a,XH)) + | XH -> XH,(XH,b)) + + (** val ggcd : positive -> positive -> positive * (positive * positive) **) + + let ggcd a b = + ggcdn (plus (size_nat a) (size_nat b)) a b + + (** val coq_Nsucc_double : n -> n **) + + let coq_Nsucc_double = function + | N0 -> Npos XH + | Npos p -> Npos (XI p) + + (** val coq_Ndouble : n -> n **) + + let coq_Ndouble = function + | N0 -> N0 + | Npos p -> Npos (XO p) + + (** val coq_lor : positive -> positive -> positive **) + + let rec coq_lor p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> XI (coq_lor p2 q1) + | XO q1 -> XI (coq_lor p2 q1) + | XH -> p) + | XO p2 -> + (match q0 with + | XI q1 -> XI (coq_lor p2 q1) + | XO q1 -> XO (coq_lor p2 q1) + | XH -> XI p2) + | XH -> + (match q0 with + | XO q1 -> XI q1 + | _ -> q0) + + (** val coq_land : positive -> positive -> n **) + + let rec coq_land p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Nsucc_double (coq_land p2 q1) + | XO q1 -> coq_Ndouble (coq_land p2 q1) + | XH -> Npos XH) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (coq_land p2 q1) + | XO q1 -> coq_Ndouble (coq_land p2 q1) + | XH -> N0) + | XH -> + (match q0 with + | XO q1 -> N0 + | _ -> Npos XH) + + (** val ldiff : positive -> positive -> n **) + + let rec ldiff p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (ldiff p2 q1) + | XO q1 -> coq_Nsucc_double (ldiff p2 q1) + | XH -> Npos (XO p2)) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (ldiff p2 q1) + | XO q1 -> coq_Ndouble (ldiff p2 q1) + | XH -> Npos p) + | XH -> + (match q0 with + | XO q1 -> Npos XH + | _ -> N0) + + (** val coq_lxor : positive -> positive -> n **) + + let rec coq_lxor p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (coq_lxor p2 q1) + | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1) + | XH -> Npos (XO p2)) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1) + | XO q1 -> coq_Ndouble (coq_lxor p2 q1) + | XH -> Npos (XI p2)) + | XH -> + (match q0 with + | XI q1 -> Npos (XO q1) + | XO q1 -> Npos (XI q1) + | XH -> N0) + + (** val shiftl_nat : positive -> nat -> positive **) + + let shiftl_nat p n0 = + nat_iter n0 (fun x -> XO x) p + + (** val shiftr_nat : positive -> nat -> positive **) + + let shiftr_nat p n0 = + nat_iter n0 div2 p + + (** val shiftl : positive -> n -> positive **) + + let shiftl p = function + | N0 -> p + | Npos n1 -> iter n1 (fun x -> XO x) p + + (** val shiftr : positive -> n -> positive **) + + let shiftr p = function + | N0 -> p + | Npos n1 -> iter n1 div2 p + + (** val testbit_nat : positive -> nat -> bool **) + + let rec testbit_nat p n0 = + match p with + | XI p2 -> + (match n0 with + | O -> true + | S n' -> testbit_nat p2 n') + | XO p2 -> + (match n0 with + | O -> false + | S n' -> testbit_nat p2 n') + | XH -> + (match n0 with + | O -> true + | S n1 -> false) + + (** val testbit : positive -> n -> bool **) + + let rec testbit p n0 = + match p with + | XI p2 -> + (match n0 with + | N0 -> true + | Npos n1 -> testbit p2 (pred_N n1)) + | XO p2 -> + (match n0 with + | N0 -> false + | Npos n1 -> testbit p2 (pred_N n1)) + | XH -> + (match n0 with + | N0 -> true + | Npos p2 -> false) + + (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **) + + let rec iter_op op p a = + match p with + | XI p2 -> op a (iter_op op p2 (op a a)) + | XO p2 -> iter_op op p2 (op a a) + | XH -> a + + (** val to_nat : positive -> nat **) + + let to_nat x = + iter_op plus x (S O) + + (** val of_nat : nat -> positive **) + + let rec of_nat = function + | O -> XH + | S x -> + (match x with + | O -> XH + | S n1 -> succ (of_nat x)) + + (** val of_succ_nat : nat -> positive **) + + let rec of_succ_nat = function + | O -> XH + | S x -> succ (of_succ_nat x) + end + +module Coq_Pos = + struct + module Coq__1 = struct + type t = positive + end + type t = Coq__1.t + + (** val succ : positive -> positive **) + + let rec succ = function + | XI p -> XO (succ p) + | XO p -> XI p + | XH -> XO XH + + (** val add : positive -> positive -> positive **) + + let rec add x y = + match x with + | XI p -> + (match y with + | XI q0 -> XO (add_carry p q0) + | XO q0 -> XI (add p q0) + | XH -> XO (succ p)) + | XO p -> + (match y with + | XI q0 -> XI (add p q0) + | XO q0 -> XO (add p q0) + | XH -> XI p) + | XH -> + (match y with + | XI q0 -> XO (succ q0) + | XO q0 -> XI q0 + | XH -> XO XH) + + (** val add_carry : positive -> positive -> positive **) + + and add_carry x y = + match x with + | XI p -> + (match y with + | XI q0 -> XI (add_carry p q0) + | XO q0 -> XO (add_carry p q0) + | XH -> XI (succ p)) + | XO p -> + (match y with + | XI q0 -> XO (add_carry p q0) + | XO q0 -> XI (add p q0) + | XH -> XO (succ p)) + | XH -> + (match y with + | XI q0 -> XI (succ q0) + | XO q0 -> XO (succ q0) + | XH -> XI XH) + + (** val pred_double : positive -> positive **) + + let rec pred_double = function + | XI p -> XI (XO p) + | XO p -> XI (pred_double p) + | XH -> XH + + (** val pred : positive -> positive **) + + let pred = function + | XI p -> XO p + | XO p -> pred_double p + | XH -> XH + + (** val pred_N : positive -> n **) + + let pred_N = function + | XI p -> Npos (XO p) + | XO p -> Npos (pred_double p) + | XH -> N0 + + type mask = Pos.mask = + | IsNul + | IsPos of positive + | IsNeg + + (** val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) + + let mask_rect f f0 f1 = function + | IsNul -> f + | IsPos x -> f0 x + | IsNeg -> f1 + + (** val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 **) + + let mask_rec f f0 f1 = function + | IsNul -> f + | IsPos x -> f0 x + | IsNeg -> f1 + + (** val succ_double_mask : mask -> mask **) + + let succ_double_mask = function + | IsNul -> IsPos XH + | IsPos p -> IsPos (XI p) + | IsNeg -> IsNeg + + (** val double_mask : mask -> mask **) + + let double_mask = function + | IsPos p -> IsPos (XO p) + | x0 -> x0 + + (** val double_pred_mask : positive -> mask **) + + let double_pred_mask = function + | XI p -> IsPos (XO (XO p)) + | XO p -> IsPos (XO (pred_double p)) + | XH -> IsNul + + (** val pred_mask : mask -> mask **) + + let pred_mask = function + | IsPos q0 -> + (match q0 with + | XH -> IsNul + | _ -> IsPos (pred q0)) + | _ -> IsNeg + + (** val sub_mask : positive -> positive -> mask **) + + let rec sub_mask x y = + match x with + | XI p -> + (match y with + | XI q0 -> double_mask (sub_mask p q0) + | XO q0 -> succ_double_mask (sub_mask p q0) + | XH -> IsPos (XO p)) + | XO p -> + (match y with + | XI q0 -> succ_double_mask (sub_mask_carry p q0) + | XO q0 -> double_mask (sub_mask p q0) + | XH -> IsPos (pred_double p)) + | XH -> + (match y with + | XH -> IsNul + | _ -> IsNeg) + + (** val sub_mask_carry : positive -> positive -> mask **) + + and sub_mask_carry x y = + match x with + | XI p -> + (match y with + | XI q0 -> succ_double_mask (sub_mask_carry p q0) + | XO q0 -> double_mask (sub_mask p q0) + | XH -> IsPos (pred_double p)) + | XO p -> + (match y with + | XI q0 -> double_mask (sub_mask_carry p q0) + | XO q0 -> succ_double_mask (sub_mask_carry p q0) + | XH -> double_pred_mask p) + | XH -> IsNeg + + (** val sub : positive -> positive -> positive **) + + let sub x y = + match sub_mask x y with + | IsPos z0 -> z0 + | _ -> XH + + (** val mul : positive -> positive -> positive **) + + let rec mul x y = + match x with + | XI p -> add y (XO (mul p y)) + | XO p -> XO (mul p y) + | XH -> y + + (** val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) + + let rec iter n0 f x = + match n0 with + | XI n' -> f (iter n' f (iter n' f x)) + | XO n' -> iter n' f (iter n' f x) + | XH -> f x + + (** val pow : positive -> positive -> positive **) + + let pow x y = + iter y (mul x) XH + + (** val div2 : positive -> positive **) + + let div2 = function + | XI p2 -> p2 + | XO p2 -> p2 + | XH -> XH + + (** val div2_up : positive -> positive **) + + let div2_up = function + | XI p2 -> succ p2 + | XO p2 -> p2 + | XH -> XH + + (** val size_nat : positive -> nat **) + + let rec size_nat = function + | XI p2 -> S (size_nat p2) + | XO p2 -> S (size_nat p2) + | XH -> S O + + (** val size : positive -> positive **) + + let rec size = function + | XI p2 -> succ (size p2) + | XO p2 -> succ (size p2) + | XH -> XH + + (** val compare_cont : positive -> positive -> comparison -> comparison **) + + let rec compare_cont x y r = + match x with + | XI p -> + (match y with + | XI q0 -> compare_cont p q0 r + | XO q0 -> compare_cont p q0 Gt + | XH -> Gt) + | XO p -> + (match y with + | XI q0 -> compare_cont p q0 Lt + | XO q0 -> compare_cont p q0 r + | XH -> Gt) + | XH -> + (match y with + | XH -> r + | _ -> Lt) + + (** val compare : positive -> positive -> comparison **) + + let compare x y = + compare_cont x y Eq + + (** val min : positive -> positive -> positive **) + + let min p p' = + match compare p p' with + | Gt -> p' + | _ -> p + + (** val max : positive -> positive -> positive **) + + let max p p' = + match compare p p' with + | Gt -> p + | _ -> p' + + (** val eqb : positive -> positive -> bool **) + + let rec eqb p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> eqb p2 q1 + | _ -> false) + | XO p2 -> + (match q0 with + | XO q1 -> eqb p2 q1 + | _ -> false) + | XH -> + (match q0 with + | XH -> true + | _ -> false) + + (** val leb : positive -> positive -> bool **) + + let leb x y = + match compare x y with + | Gt -> false + | _ -> true + + (** val ltb : positive -> positive -> bool **) + + let ltb x y = + match compare x y with + | Lt -> true + | _ -> false + + (** val sqrtrem_step : + (positive -> positive) -> (positive -> positive) -> (positive * mask) + -> positive * mask **) + + let sqrtrem_step f g = function + | s,y -> + (match y with + | IsPos r -> + let s' = XI (XO s) in + let r' = g (f r) in + if leb s' r' then (XI s),(sub_mask r' s') else (XO s),(IsPos r') + | _ -> (XO s),(sub_mask (g (f XH)) (XO (XO XH)))) + + (** val sqrtrem : positive -> positive * mask **) + + let rec sqrtrem = function + | XI p2 -> + (match p2 with + | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XI x) (sqrtrem p3) + | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XI x) (sqrtrem p3) + | XH -> XH,(IsPos (XO XH))) + | XO p2 -> + (match p2 with + | XI p3 -> sqrtrem_step (fun x -> XI x) (fun x -> XO x) (sqrtrem p3) + | XO p3 -> sqrtrem_step (fun x -> XO x) (fun x -> XO x) (sqrtrem p3) + | XH -> XH,(IsPos XH)) + | XH -> XH,IsNul + + (** val sqrt : positive -> positive **) + + let sqrt p = + fst (sqrtrem p) + + (** val gcdn : nat -> positive -> positive -> positive **) + + let rec gcdn n0 a b = + match n0 with + | O -> XH + | S n1 -> + (match a with + | XI a' -> + (match b with + | XI b' -> + (match compare a' b' with + | Eq -> a + | Lt -> gcdn n1 (sub b' a') a + | Gt -> gcdn n1 (sub a' b') b) + | XO b0 -> gcdn n1 a b0 + | XH -> XH) + | XO a0 -> + (match b with + | XI p -> gcdn n1 a0 b + | XO b0 -> XO (gcdn n1 a0 b0) + | XH -> XH) + | XH -> XH) + + (** val gcd : positive -> positive -> positive **) + + let gcd a b = + gcdn (plus (size_nat a) (size_nat b)) a b + + (** val ggcdn : + nat -> positive -> positive -> positive * (positive * positive) **) + + let rec ggcdn n0 a b = + match n0 with + | O -> XH,(a,b) + | S n1 -> + (match a with + | XI a' -> + (match b with + | XI b' -> + (match compare a' b' with + | Eq -> a,(XH,XH) + | Lt -> + let g,p = ggcdn n1 (sub b' a') a in + let ba,aa = p in g,(aa,(add aa (XO ba))) + | Gt -> + let g,p = ggcdn n1 (sub a' b') b in + let ab,bb = p in g,((add bb (XO ab)),bb)) + | XO b0 -> + let g,p = ggcdn n1 a b0 in let aa,bb = p in g,(aa,(XO bb)) + | XH -> XH,(a,XH)) + | XO a0 -> + (match b with + | XI p -> + let g,p2 = ggcdn n1 a0 b in let aa,bb = p2 in g,((XO aa),bb) + | XO b0 -> let g,p = ggcdn n1 a0 b0 in (XO g),p + | XH -> XH,(a,XH)) + | XH -> XH,(XH,b)) + + (** val ggcd : positive -> positive -> positive * (positive * positive) **) + + let ggcd a b = + ggcdn (plus (size_nat a) (size_nat b)) a b + + (** val coq_Nsucc_double : n -> n **) + + let coq_Nsucc_double = function + | N0 -> Npos XH + | Npos p -> Npos (XI p) + + (** val coq_Ndouble : n -> n **) + + let coq_Ndouble = function + | N0 -> N0 + | Npos p -> Npos (XO p) + + (** val coq_lor : positive -> positive -> positive **) + + let rec coq_lor p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> XI (coq_lor p2 q1) + | XO q1 -> XI (coq_lor p2 q1) + | XH -> p) + | XO p2 -> + (match q0 with + | XI q1 -> XI (coq_lor p2 q1) + | XO q1 -> XO (coq_lor p2 q1) + | XH -> XI p2) + | XH -> + (match q0 with + | XO q1 -> XI q1 + | _ -> q0) + + (** val coq_land : positive -> positive -> n **) + + let rec coq_land p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Nsucc_double (coq_land p2 q1) + | XO q1 -> coq_Ndouble (coq_land p2 q1) + | XH -> Npos XH) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (coq_land p2 q1) + | XO q1 -> coq_Ndouble (coq_land p2 q1) + | XH -> N0) + | XH -> + (match q0 with + | XO q1 -> N0 + | _ -> Npos XH) + + (** val ldiff : positive -> positive -> n **) + + let rec ldiff p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (ldiff p2 q1) + | XO q1 -> coq_Nsucc_double (ldiff p2 q1) + | XH -> Npos (XO p2)) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (ldiff p2 q1) + | XO q1 -> coq_Ndouble (ldiff p2 q1) + | XH -> Npos p) + | XH -> + (match q0 with + | XO q1 -> Npos XH + | _ -> N0) + + (** val coq_lxor : positive -> positive -> n **) + + let rec coq_lxor p q0 = + match p with + | XI p2 -> + (match q0 with + | XI q1 -> coq_Ndouble (coq_lxor p2 q1) + | XO q1 -> coq_Nsucc_double (coq_lxor p2 q1) + | XH -> Npos (XO p2)) + | XO p2 -> + (match q0 with + | XI q1 -> coq_Nsucc_double (coq_lxor p2 q1) + | XO q1 -> coq_Ndouble (coq_lxor p2 q1) + | XH -> Npos (XI p2)) + | XH -> + (match q0 with + | XI q1 -> Npos (XO q1) + | XO q1 -> Npos (XI q1) + | XH -> N0) + + (** val shiftl_nat : positive -> nat -> positive **) + + let shiftl_nat p n0 = + nat_iter n0 (fun x -> XO x) p + + (** val shiftr_nat : positive -> nat -> positive **) + + let shiftr_nat p n0 = + nat_iter n0 div2 p + + (** val shiftl : positive -> n -> positive **) + + let shiftl p = function + | N0 -> p + | Npos n1 -> iter n1 (fun x -> XO x) p + + (** val shiftr : positive -> n -> positive **) + + let shiftr p = function + | N0 -> p + | Npos n1 -> iter n1 div2 p + + (** val testbit_nat : positive -> nat -> bool **) + + let rec testbit_nat p n0 = + match p with + | XI p2 -> + (match n0 with + | O -> true + | S n' -> testbit_nat p2 n') + | XO p2 -> + (match n0 with + | O -> false + | S n' -> testbit_nat p2 n') + | XH -> + (match n0 with + | O -> true + | S n1 -> false) + + (** val testbit : positive -> n -> bool **) + + let rec testbit p n0 = + match p with + | XI p2 -> + (match n0 with + | N0 -> true + | Npos n1 -> testbit p2 (pred_N n1)) + | XO p2 -> + (match n0 with + | N0 -> false + | Npos n1 -> testbit p2 (pred_N n1)) + | XH -> + (match n0 with + | N0 -> true + | Npos p2 -> false) + + (** val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 **) + + let rec iter_op op p a = + match p with + | XI p2 -> op a (iter_op op p2 (op a a)) + | XO p2 -> iter_op op p2 (op a a) + | XH -> a + + (** val to_nat : positive -> nat **) + + let to_nat x = + iter_op plus x (S O) + + (** val of_nat : nat -> positive **) + + let rec of_nat = function + | O -> XH + | S x -> + (match x with + | O -> XH + | S n1 -> succ (of_nat x)) + + (** val of_succ_nat : nat -> positive **) + + let rec of_succ_nat = function + | O -> XH + | S x -> succ (of_succ_nat x) + + (** val eq_dec : positive -> positive -> bool **) + + let rec eq_dec p y0 = + match p with + | XI p2 -> + (match y0 with + | XI p3 -> eq_dec p2 p3 + | _ -> false) + | XO p2 -> + (match y0 with + | XO p3 -> eq_dec p2 p3 + | _ -> false) + | XH -> + (match y0 with + | XH -> true + | _ -> false) + + (** val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **) + + let rec peano_rect a f p = + let f2 = peano_rect (f XH a) (fun p2 x -> f (succ (XO p2)) (f (XO p2) x)) + in + (match p with + | XI q0 -> f (XO q0) (f2 q0) + | XO q0 -> f2 q0 + | XH -> a) + + (** val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 **) + + let peano_rec = + peano_rect + + type coq_PeanoView = + | PeanoOne + | PeanoSucc of positive * coq_PeanoView + + (** val coq_PeanoView_rect : + 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> + coq_PeanoView -> 'a1 **) + + let rec coq_PeanoView_rect f f0 p = function + | PeanoOne -> f + | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rect f f0 p3 p4) + + (** val coq_PeanoView_rec : + 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> + coq_PeanoView -> 'a1 **) + + let rec coq_PeanoView_rec f f0 p = function + | PeanoOne -> f + | PeanoSucc (p3, p4) -> f0 p3 p4 (coq_PeanoView_rec f f0 p3 p4) + + (** val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView **) + + let rec peanoView_xO p = function + | PeanoOne -> PeanoSucc (XH, PeanoOne) + | PeanoSucc (p2, q1) -> + PeanoSucc ((succ (XO p2)), (PeanoSucc ((XO p2), (peanoView_xO p2 q1)))) + + (** val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView **) + + let rec peanoView_xI p = function + | PeanoOne -> PeanoSucc ((succ XH), (PeanoSucc (XH, PeanoOne))) + | PeanoSucc (p2, q1) -> + PeanoSucc ((succ (XI p2)), (PeanoSucc ((XI p2), (peanoView_xI p2 q1)))) + + (** val peanoView : positive -> coq_PeanoView **) + + let rec peanoView = function + | XI p2 -> peanoView_xI p2 (peanoView p2) + | XO p2 -> peanoView_xO p2 (peanoView p2) + | XH -> PeanoOne + + (** val coq_PeanoView_iter : + 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1 **) + + let rec coq_PeanoView_iter a f p = function + | PeanoOne -> a + | PeanoSucc (p2, q1) -> f p2 (coq_PeanoView_iter a f p2 q1) + + (** val switch_Eq : comparison -> comparison -> comparison **) + + let switch_Eq c = function + | Eq -> c + | x -> x + + (** val mask2cmp : mask -> comparison **) + + let mask2cmp = function + | IsNul -> Eq + | IsPos p2 -> Gt + | IsNeg -> Lt + + module T = + struct + + end + + module ORev = + struct + type t = Coq__1.t + end + + module MRev = + struct + (** val max : t -> t -> t **) + + let max x y = + min y x + end + + module MPRev = MaxLogicalProperties(ORev)(MRev) + + module P = + struct + (** val max_case_strong : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let max_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat n0 (max n0 m) __ (hl __) + | _ -> compat m (max n0 m) __ (hr __)) + + (** val max_case : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 x1 = + max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val max_dec : t -> t -> bool **) + + let max_dec n0 m = + max_case n0 m (fun x y _ h0 -> h0) true false + + (** val min_case_strong : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let min_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat m (min n0 m) __ (hr __) + | _ -> compat n0 (min n0 m) __ (hl __)) + + (** val min_case : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 x1 = + min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val min_dec : t -> t -> bool **) + + let min_dec n0 m = + min_case n0 m (fun x y _ h0 -> h0) true false + end + + (** val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let max_case_strong n0 m x x0 = + P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val max_case : t -> t -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 = + max_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val max_dec : t -> t -> bool **) + + let max_dec = + P.max_dec + + (** val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let min_case_strong n0 m x x0 = + P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val min_case : t -> t -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 = + min_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val min_dec : t -> t -> bool **) + + let min_dec = + P.min_dec + end + +module N = + struct + type t = n + + (** val zero : n **) + + let zero = + N0 + + (** val one : n **) + + let one = + Npos XH + + (** val two : n **) + + let two = + Npos (XO XH) + + (** val succ_double : n -> n **) + + let succ_double = function + | N0 -> Npos XH + | Npos p -> Npos (XI p) + + (** val double : n -> n **) + + let double = function + | N0 -> N0 + | Npos p -> Npos (XO p) + + (** val succ : n -> n **) + + let succ = function + | N0 -> Npos XH + | Npos p -> Npos (Coq_Pos.succ p) + + (** val pred : n -> n **) + + let pred = function + | N0 -> N0 + | Npos p -> Coq_Pos.pred_N p + + (** val succ_pos : n -> positive **) + + let succ_pos = function + | N0 -> XH + | Npos p -> Coq_Pos.succ p + + (** val add : n -> n -> n **) + + let add n0 m = + match n0 with + | N0 -> m + | Npos p -> + (match m with + | N0 -> n0 + | Npos q0 -> Npos (Coq_Pos.add p q0)) + + (** val sub : n -> n -> n **) + + let sub n0 m = + match n0 with + | N0 -> N0 + | Npos n' -> + (match m with + | N0 -> n0 + | Npos m' -> + (match Coq_Pos.sub_mask n' m' with + | Coq_Pos.IsPos p -> Npos p + | _ -> N0)) + + (** val mul : n -> n -> n **) + + let mul n0 m = + match n0 with + | N0 -> N0 + | Npos p -> + (match m with + | N0 -> N0 + | Npos q0 -> Npos (Coq_Pos.mul p q0)) + + (** val compare : n -> n -> comparison **) + + let compare n0 m = + match n0 with + | N0 -> + (match m with + | N0 -> Eq + | Npos m' -> Lt) + | Npos n' -> + (match m with + | N0 -> Gt + | Npos m' -> Coq_Pos.compare n' m') + + (** val eqb : n -> n -> bool **) + + let rec eqb n0 m = + match n0 with + | N0 -> + (match m with + | N0 -> true + | Npos p -> false) + | Npos p -> + (match m with + | N0 -> false + | Npos q0 -> Coq_Pos.eqb p q0) + + (** val leb : n -> n -> bool **) + + let leb x y = + match compare x y with + | Gt -> false + | _ -> true + + (** val ltb : n -> n -> bool **) + + let ltb x y = + match compare x y with + | Lt -> true + | _ -> false + + (** val min : n -> n -> n **) + + let min n0 n' = + match compare n0 n' with + | Gt -> n' + | _ -> n0 + + (** val max : n -> n -> n **) + + let max n0 n' = + match compare n0 n' with + | Gt -> n0 + | _ -> n' + + (** val div2 : n -> n **) + + let div2 = function + | N0 -> N0 + | Npos p2 -> + (match p2 with + | XI p -> Npos p + | XO p -> Npos p + | XH -> N0) + + (** val even : n -> bool **) + + let even = function + | N0 -> true + | Npos p -> + (match p with + | XO p2 -> true + | _ -> false) + + (** val odd : n -> bool **) + + let odd n0 = + negb (even n0) + + (** val pow : n -> n -> n **) + + let pow n0 = function + | N0 -> Npos XH + | Npos p2 -> + (match n0 with + | N0 -> N0 + | Npos q0 -> Npos (Coq_Pos.pow q0 p2)) + + (** val log2 : n -> n **) + + let log2 = function + | N0 -> N0 + | Npos p2 -> + (match p2 with + | XI p -> Npos (Coq_Pos.size p) + | XO p -> Npos (Coq_Pos.size p) + | XH -> N0) + + (** val size : n -> n **) + + let size = function + | N0 -> N0 + | Npos p -> Npos (Coq_Pos.size p) + + (** val size_nat : n -> nat **) + + let size_nat = function + | N0 -> O + | Npos p -> Coq_Pos.size_nat p + + (** val pos_div_eucl : positive -> n -> n * n **) + + let rec pos_div_eucl a b = + match a with + | XI a' -> + let q0,r = pos_div_eucl a' b in + let r' = succ_double r in + if leb b r' then (succ_double q0),(sub r' b) else (double q0),r' + | XO a' -> + let q0,r = pos_div_eucl a' b in + let r' = double r in + if leb b r' then (succ_double q0),(sub r' b) else (double q0),r' + | XH -> + (match b with + | N0 -> N0,(Npos XH) + | Npos p -> + (match p with + | XH -> (Npos XH),N0 + | _ -> N0,(Npos XH))) + + (** val div_eucl : n -> n -> n * n **) + + let div_eucl a b = + match a with + | N0 -> N0,N0 + | Npos na -> + (match b with + | N0 -> N0,a + | Npos p -> pos_div_eucl na b) + + (** val div : n -> n -> n **) + + let div a b = + fst (div_eucl a b) + + (** val modulo : n -> n -> n **) + + let modulo a b = + snd (div_eucl a b) + + (** val gcd : n -> n -> n **) + + let gcd a b = + match a with + | N0 -> b + | Npos p -> + (match b with + | N0 -> a + | Npos q0 -> Npos (Coq_Pos.gcd p q0)) + + (** val ggcd : n -> n -> n * (n * n) **) + + let ggcd a b = + match a with + | N0 -> b,(N0,(Npos XH)) + | Npos p -> + (match b with + | N0 -> a,((Npos XH),N0) + | Npos q0 -> + let g,p2 = Coq_Pos.ggcd p q0 in + let aa,bb = p2 in (Npos g),((Npos aa),(Npos bb))) + + (** val sqrtrem : n -> n * n **) + + let sqrtrem = function + | N0 -> N0,N0 + | Npos p -> + let s,m = Coq_Pos.sqrtrem p in + (match m with + | Coq_Pos.IsPos r -> (Npos s),(Npos r) + | _ -> (Npos s),N0) + + (** val sqrt : n -> n **) + + let sqrt = function + | N0 -> N0 + | Npos p -> Npos (Coq_Pos.sqrt p) + + (** val coq_lor : n -> n -> n **) + + let coq_lor n0 m = + match n0 with + | N0 -> m + | Npos p -> + (match m with + | N0 -> n0 + | Npos q0 -> Npos (Coq_Pos.coq_lor p q0)) + + (** val coq_land : n -> n -> n **) + + let coq_land n0 m = + match n0 with + | N0 -> N0 + | Npos p -> + (match m with + | N0 -> N0 + | Npos q0 -> Coq_Pos.coq_land p q0) + + (** val ldiff : n -> n -> n **) + + let rec ldiff n0 m = + match n0 with + | N0 -> N0 + | Npos p -> + (match m with + | N0 -> n0 + | Npos q0 -> Coq_Pos.ldiff p q0) + + (** val coq_lxor : n -> n -> n **) + + let coq_lxor n0 m = + match n0 with + | N0 -> m + | Npos p -> + (match m with + | N0 -> n0 + | Npos q0 -> Coq_Pos.coq_lxor p q0) + + (** val shiftl_nat : n -> nat -> n **) + + let shiftl_nat a n0 = + nat_iter n0 double a + + (** val shiftr_nat : n -> nat -> n **) + + let shiftr_nat a n0 = + nat_iter n0 div2 a + + (** val shiftl : n -> n -> n **) + + let shiftl a n0 = + match a with + | N0 -> N0 + | Npos a0 -> Npos (Coq_Pos.shiftl a0 n0) + + (** val shiftr : n -> n -> n **) + + let shiftr a = function + | N0 -> a + | Npos p -> Coq_Pos.iter p div2 a + + (** val testbit_nat : n -> nat -> bool **) + + let testbit_nat = function + | N0 -> (fun x -> false) + | Npos p -> Coq_Pos.testbit_nat p + + (** val testbit : n -> n -> bool **) + + let testbit a n0 = + match a with + | N0 -> false + | Npos p -> Coq_Pos.testbit p n0 + + (** val to_nat : n -> nat **) + + let to_nat = function + | N0 -> O + | Npos p -> Coq_Pos.to_nat p + + (** val of_nat : nat -> n **) + + let of_nat = function + | O -> N0 + | S n' -> Npos (Coq_Pos.of_succ_nat n') + + (** val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) + + let iter n0 f x = + match n0 with + | N0 -> x + | Npos p -> Coq_Pos.iter p f x + + (** val eq_dec : n -> n -> bool **) + + let eq_dec n0 m = + match n0 with + | N0 -> + (match m with + | N0 -> true + | Npos p -> false) + | Npos x -> + (match m with + | N0 -> false + | Npos p2 -> Coq_Pos.eq_dec x p2) + + (** val discr : n -> positive option **) + + let discr = function + | N0 -> None + | Npos p -> Some p + + (** val binary_rect : + 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) + + let binary_rect f0 f2 fS2 n0 = + let f2' = fun p -> f2 (Npos p) in + let fS2' = fun p -> fS2 (Npos p) in + (match n0 with + | N0 -> f0 + | Npos p -> + let rec f = function + | XI p3 -> fS2' p3 (f p3) + | XO p3 -> f2' p3 (f p3) + | XH -> fS2 N0 f0 + in f p) + + (** val binary_rec : + 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) + + let binary_rec = + binary_rect + + (** val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) + + let peano_rect f0 f n0 = + let f' = fun p -> f (Npos p) in + (match n0 with + | N0 -> f0 + | Npos p -> Coq_Pos.peano_rect (f N0 f0) f' p) + + (** val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) + + let peano_rec = + peano_rect + + module BootStrap = + struct + + end + + (** val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 **) + + let recursion x = + peano_rect x + + module OrderElts = + struct + type t = n + end + + module OrderTac = MakeOrderTac(OrderElts) + + module NZPowP = + struct + + end + + module NZSqrtP = + struct + + end + + (** val sqrt_up : n -> n **) + + let sqrt_up a = + match compare N0 a with + | Lt -> succ (sqrt (pred a)) + | _ -> N0 + + (** val log2_up : n -> n **) + + let log2_up a = + match compare (Npos XH) a with + | Lt -> succ (log2 (pred a)) + | _ -> N0 + + module NZDivP = + struct + + end + + (** val lcm : n -> n -> n **) + + let lcm a b = + mul a (div b (gcd a b)) + + (** val b2n : bool -> n **) + + let b2n = function + | true -> Npos XH + | false -> N0 + + (** val setbit : n -> n -> n **) + + let setbit a n0 = + coq_lor a (shiftl (Npos XH) n0) + + (** val clearbit : n -> n -> n **) + + let clearbit a n0 = + ldiff a (shiftl (Npos XH) n0) + + (** val ones : n -> n **) + + let ones n0 = + pred (shiftl (Npos XH) n0) + + (** val lnot : n -> n -> n **) + + let lnot a n0 = + coq_lxor a (ones n0) + + module T = + struct + + end + + module ORev = + struct + type t = n + end + + module MRev = + struct + (** val max : n -> n -> n **) + + let max x y = + min y x + end + + module MPRev = MaxLogicalProperties(ORev)(MRev) + + module P = + struct + (** val max_case_strong : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let max_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat n0 (max n0 m) __ (hl __) + | _ -> compat m (max n0 m) __ (hr __)) + + (** val max_case : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 x1 = + max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val max_dec : n -> n -> bool **) + + let max_dec n0 m = + max_case n0 m (fun x y _ h0 -> h0) true false + + (** val min_case_strong : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let min_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat m (min n0 m) __ (hr __) + | _ -> compat n0 (min n0 m) __ (hl __)) + + (** val min_case : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 x1 = + min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val min_dec : n -> n -> bool **) + + let min_dec n0 m = + min_case n0 m (fun x y _ h0 -> h0) true false + end + + (** val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let max_case_strong n0 m x x0 = + P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val max_case : n -> n -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 = + max_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val max_dec : n -> n -> bool **) + + let max_dec = + P.max_dec + + (** val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let min_case_strong n0 m x x0 = + P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val min_case : n -> n -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 = + min_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val min_dec : n -> n -> bool **) + + let min_dec = + P.min_dec + end (** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **) @@ -228,268 +2010,773 @@ let rec nth n0 l default = | S m -> (match l with | [] -> default - | x::t0 -> nth m t0 default) + | x::t1 -> nth m t1 default) (** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **) let rec map f = function | [] -> [] -| a::t0 -> (f a)::(map f t0) +| a::t1 -> (f a)::(map f t1) (** val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 **) let rec fold_right f a0 = function | [] -> a0 -| b::t0 -> f b (fold_right f a0 t0) - -type z = -| Z0 -| Zpos of positive -| Zneg of positive - -(** val zdouble_plus_one : z -> z **) - -let zdouble_plus_one = function -| Z0 -> Zpos XH -| Zpos p -> Zpos (XI p) -| Zneg p -> Zneg (pdouble_minus_one p) - -(** val zdouble_minus_one : z -> z **) - -let zdouble_minus_one = function -| Z0 -> Zneg XH -| Zpos p -> Zpos (pdouble_minus_one p) -| Zneg p -> Zneg (XI p) - -(** val zdouble : z -> z **) - -let zdouble = function -| Z0 -> Z0 -| Zpos p -> Zpos (XO p) -| Zneg p -> Zneg (XO p) - -(** val zPminus : positive -> positive -> z **) - -let rec zPminus x y = - match x with - | XI p -> - (match y with - | XI q0 -> zdouble (zPminus p q0) - | XO q0 -> zdouble_plus_one (zPminus p q0) - | XH -> Zpos (XO p)) - | XO p -> - (match y with - | XI q0 -> zdouble_minus_one (zPminus p q0) - | XO q0 -> zdouble (zPminus p q0) - | XH -> Zpos (pdouble_minus_one p)) - | XH -> - (match y with - | XI q0 -> Zneg (XO q0) - | XO q0 -> Zneg (pdouble_minus_one q0) - | XH -> Z0) - -(** val zplus : z -> z -> z **) - -let zplus x y = - match x with - | Z0 -> y - | Zpos x' -> - (match y with - | Z0 -> Zpos x' - | Zpos y' -> Zpos (pplus x' y') - | Zneg y' -> - (match pcompare x' y' Eq with - | Eq -> Z0 - | Lt -> Zneg (pminus y' x') - | Gt -> Zpos (pminus x' y'))) - | Zneg x' -> - (match y with - | Z0 -> Zneg x' - | Zpos y' -> - (match pcompare x' y' Eq with - | Eq -> Z0 - | Lt -> Zpos (pminus y' x') - | Gt -> Zneg (pminus x' y')) - | Zneg y' -> Zneg (pplus x' y')) - -(** val zopp : z -> z **) - -let zopp = function -| Z0 -> Z0 -| Zpos x0 -> Zneg x0 -| Zneg x0 -> Zpos x0 - -(** val zminus : z -> z -> z **) - -let zminus m n0 = - zplus m (zopp n0) - -(** val zmult : z -> z -> z **) - -let zmult x y = - match x with +| b::t1 -> f b (fold_right f a0 t1) + +module Z = + struct + type t = z + + (** val zero : z **) + + let zero = + Z0 + + (** val one : z **) + + let one = + Zpos XH + + (** val two : z **) + + let two = + Zpos (XO XH) + + (** val double : z -> z **) + + let double = function | Z0 -> Z0 - | Zpos x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zpos (pmult x' y') - | Zneg y' -> Zneg (pmult x' y')) - | Zneg x' -> - (match y with - | Z0 -> Z0 - | Zpos y' -> Zneg (pmult x' y') - | Zneg y' -> Zpos (pmult x' y')) - -(** val zcompare : z -> z -> comparison **) - -let zcompare x y = - match x with - | Z0 -> - (match y with - | Z0 -> Eq - | Zpos y' -> Lt - | Zneg y' -> Gt) - | Zpos x' -> - (match y with - | Zpos y' -> pcompare x' y' Eq - | _ -> Gt) - | Zneg x' -> - (match y with - | Zneg y' -> compOpp (pcompare x' y' Eq) - | _ -> Lt) - -(** val zmax : z -> z -> z **) - -let zmax n0 m = - match zcompare n0 m with - | Lt -> m - | _ -> n0 - -(** val zabs : z -> z **) - -let zabs = function -| Zneg p -> Zpos p -| x -> x - -(** val zle_bool : z -> z -> bool **) - -let zle_bool x y = - match zcompare x y with - | Gt -> false - | _ -> true - -(** val zge_bool : z -> z -> bool **) - -let zge_bool x y = - match zcompare x y with - | Lt -> false - | _ -> true - -(** val zgt_bool : z -> z -> bool **) - -let zgt_bool x y = - match zcompare x y with - | Gt -> true - | _ -> false + | Zpos p -> Zpos (XO p) + | Zneg p -> Zneg (XO p) + + (** val succ_double : z -> z **) + + let succ_double = function + | Z0 -> Zpos XH + | Zpos p -> Zpos (XI p) + | Zneg p -> Zneg (Coq_Pos.pred_double p) + + (** val pred_double : z -> z **) + + let pred_double = function + | Z0 -> Zneg XH + | Zpos p -> Zpos (Coq_Pos.pred_double p) + | Zneg p -> Zneg (XI p) + + (** val pos_sub : positive -> positive -> z **) + + let rec pos_sub x y = + match x with + | XI p -> + (match y with + | XI q0 -> double (pos_sub p q0) + | XO q0 -> succ_double (pos_sub p q0) + | XH -> Zpos (XO p)) + | XO p -> + (match y with + | XI q0 -> pred_double (pos_sub p q0) + | XO q0 -> double (pos_sub p q0) + | XH -> Zpos (Coq_Pos.pred_double p)) + | XH -> + (match y with + | XI q0 -> Zneg (XO q0) + | XO q0 -> Zneg (Coq_Pos.pred_double q0) + | XH -> Z0) + + (** val add : z -> z -> z **) + + let add x y = + match x with + | Z0 -> y + | Zpos x' -> + (match y with + | Z0 -> x + | Zpos y' -> Zpos (Coq_Pos.add x' y') + | Zneg y' -> pos_sub x' y') + | Zneg x' -> + (match y with + | Z0 -> x + | Zpos y' -> pos_sub y' x' + | Zneg y' -> Zneg (Coq_Pos.add x' y')) + + (** val opp : z -> z **) + + let opp = function + | Z0 -> Z0 + | Zpos x0 -> Zneg x0 + | Zneg x0 -> Zpos x0 + + (** val succ : z -> z **) + + let succ x = + add x (Zpos XH) + + (** val pred : z -> z **) + + let pred x = + add x (Zneg XH) + + (** val sub : z -> z -> z **) + + let sub m n0 = + add m (opp n0) + + (** val mul : z -> z -> z **) + + let mul x y = + match x with + | Z0 -> Z0 + | Zpos x' -> + (match y with + | Z0 -> Z0 + | Zpos y' -> Zpos (Coq_Pos.mul x' y') + | Zneg y' -> Zneg (Coq_Pos.mul x' y')) + | Zneg x' -> + (match y with + | Z0 -> Z0 + | Zpos y' -> Zneg (Coq_Pos.mul x' y') + | Zneg y' -> Zpos (Coq_Pos.mul x' y')) + + (** val pow_pos : z -> positive -> z **) + + let pow_pos z0 n0 = + Coq_Pos.iter n0 (mul z0) (Zpos XH) + + (** val pow : z -> z -> z **) + + let pow x = function + | Z0 -> Zpos XH + | Zpos p -> pow_pos x p + | Zneg p -> Z0 + + (** val compare : z -> z -> comparison **) + + let compare x y = + match x with + | Z0 -> + (match y with + | Z0 -> Eq + | Zpos y' -> Lt + | Zneg y' -> Gt) + | Zpos x' -> + (match y with + | Zpos y' -> Coq_Pos.compare x' y' + | _ -> Gt) + | Zneg x' -> + (match y with + | Zneg y' -> compOpp (Coq_Pos.compare x' y') + | _ -> Lt) + + (** val sgn : z -> z **) + + let sgn = function + | Z0 -> Z0 + | Zpos p -> Zpos XH + | Zneg p -> Zneg XH + + (** val leb : z -> z -> bool **) + + let leb x y = + match compare x y with + | Gt -> false + | _ -> true + + (** val geb : z -> z -> bool **) + + let geb x y = + match compare x y with + | Lt -> false + | _ -> true + + (** val ltb : z -> z -> bool **) + + let ltb x y = + match compare x y with + | Lt -> true + | _ -> false + + (** val gtb : z -> z -> bool **) + + let gtb x y = + match compare x y with + | Gt -> true + | _ -> false + + (** val eqb : z -> z -> bool **) + + let rec eqb x y = + match x with + | Z0 -> + (match y with + | Z0 -> true + | _ -> false) + | Zpos p -> + (match y with + | Zpos q0 -> Coq_Pos.eqb p q0 + | _ -> false) + | Zneg p -> + (match y with + | Zneg q0 -> Coq_Pos.eqb p q0 + | _ -> false) + + (** val max : z -> z -> z **) + + let max n0 m = + match compare n0 m with + | Lt -> m + | _ -> n0 + + (** val min : z -> z -> z **) + + let min n0 m = + match compare n0 m with + | Gt -> m + | _ -> n0 + + (** val abs : z -> z **) + + let abs = function + | Zneg p -> Zpos p + | x -> x + + (** val abs_nat : z -> nat **) + + let abs_nat = function + | Z0 -> O + | Zpos p -> Coq_Pos.to_nat p + | Zneg p -> Coq_Pos.to_nat p + + (** val abs_N : z -> n **) + + let abs_N = function + | Z0 -> N0 + | Zpos p -> Npos p + | Zneg p -> Npos p + + (** val to_nat : z -> nat **) + + let to_nat = function + | Zpos p -> Coq_Pos.to_nat p + | _ -> O + + (** val to_N : z -> n **) + + let to_N = function + | Zpos p -> Npos p + | _ -> N0 + + (** val of_nat : nat -> z **) + + let of_nat = function + | O -> Z0 + | S n1 -> Zpos (Coq_Pos.of_succ_nat n1) + + (** val of_N : n -> z **) + + let of_N = function + | N0 -> Z0 + | Npos p -> Zpos p + + (** val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1 **) + + let iter n0 f x = + match n0 with + | Zpos p -> Coq_Pos.iter p f x + | _ -> x + + (** val pos_div_eucl : positive -> z -> z * z **) + + let rec pos_div_eucl a b = + match a with + | XI a' -> + let q0,r = pos_div_eucl a' b in + let r' = add (mul (Zpos (XO XH)) r) (Zpos XH) in + if gtb b r' + then (mul (Zpos (XO XH)) q0),r' + else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b) + | XO a' -> + let q0,r = pos_div_eucl a' b in + let r' = mul (Zpos (XO XH)) r in + if gtb b r' + then (mul (Zpos (XO XH)) q0),r' + else (add (mul (Zpos (XO XH)) q0) (Zpos XH)),(sub r' b) + | XH -> if geb b (Zpos (XO XH)) then Z0,(Zpos XH) else (Zpos XH),Z0 + + (** val div_eucl : z -> z -> z * z **) + + let div_eucl a b = + match a with + | Z0 -> Z0,Z0 + | Zpos a' -> + (match b with + | Z0 -> Z0,Z0 + | Zpos p -> pos_div_eucl a' b + | Zneg b' -> + let q0,r = pos_div_eucl a' (Zpos b') in + (match r with + | Z0 -> (opp q0),Z0 + | _ -> (opp (add q0 (Zpos XH))),(add b r))) + | Zneg a' -> + (match b with + | Z0 -> Z0,Z0 + | Zpos p -> + let q0,r = pos_div_eucl a' b in + (match r with + | Z0 -> (opp q0),Z0 + | _ -> (opp (add q0 (Zpos XH))),(sub b r)) + | Zneg b' -> let q0,r = pos_div_eucl a' (Zpos b') in q0,(opp r)) + + (** val div : z -> z -> z **) + + let div a b = + let q0,x = div_eucl a b in q0 + + (** val modulo : z -> z -> z **) + + let modulo a b = + let x,r = div_eucl a b in r + + (** val quotrem : z -> z -> z * z **) + + let quotrem a b = + match a with + | Z0 -> Z0,Z0 + | Zpos a0 -> + (match b with + | Z0 -> Z0,a + | Zpos b0 -> + let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(of_N r) + | Zneg b0 -> + let q0,r = N.pos_div_eucl a0 (Npos b0) in (opp (of_N q0)),(of_N r)) + | Zneg a0 -> + (match b with + | Z0 -> Z0,a + | Zpos b0 -> + let q0,r = N.pos_div_eucl a0 (Npos b0) in + (opp (of_N q0)),(opp (of_N r)) + | Zneg b0 -> + let q0,r = N.pos_div_eucl a0 (Npos b0) in (of_N q0),(opp (of_N r))) + + (** val quot : z -> z -> z **) + + let quot a b = + fst (quotrem a b) + + (** val rem : z -> z -> z **) + + let rem a b = + snd (quotrem a b) + + (** val even : z -> bool **) + + let even = function + | Z0 -> true + | Zpos p -> + (match p with + | XO p2 -> true + | _ -> false) + | Zneg p -> + (match p with + | XO p2 -> true + | _ -> false) + + (** val odd : z -> bool **) + + let odd = function + | Z0 -> false + | Zpos p -> + (match p with + | XO p2 -> false + | _ -> true) + | Zneg p -> + (match p with + | XO p2 -> false + | _ -> true) + + (** val div2 : z -> z **) + + let div2 = function + | Z0 -> Z0 + | Zpos p -> + (match p with + | XH -> Z0 + | _ -> Zpos (Coq_Pos.div2 p)) + | Zneg p -> Zneg (Coq_Pos.div2_up p) + + (** val quot2 : z -> z **) + + let quot2 = function + | Z0 -> Z0 + | Zpos p -> + (match p with + | XH -> Z0 + | _ -> Zpos (Coq_Pos.div2 p)) + | Zneg p -> + (match p with + | XH -> Z0 + | _ -> Zneg (Coq_Pos.div2 p)) + + (** val log2 : z -> z **) + + let log2 = function + | Zpos p2 -> + (match p2 with + | XI p -> Zpos (Coq_Pos.size p) + | XO p -> Zpos (Coq_Pos.size p) + | XH -> Z0) + | _ -> Z0 + + (** val sqrtrem : z -> z * z **) + + let sqrtrem = function + | Zpos p -> + let s,m = Coq_Pos.sqrtrem p in + (match m with + | Coq_Pos.IsPos r -> (Zpos s),(Zpos r) + | _ -> (Zpos s),Z0) + | _ -> Z0,Z0 + + (** val sqrt : z -> z **) + + let sqrt = function + | Zpos p -> Zpos (Coq_Pos.sqrt p) + | _ -> Z0 + + (** val gcd : z -> z -> z **) + + let gcd a b = + match a with + | Z0 -> abs b + | Zpos a0 -> + (match b with + | Z0 -> abs a + | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0) + | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) + | Zneg a0 -> + (match b with + | Z0 -> abs a + | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0) + | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0)) + + (** val ggcd : z -> z -> z * (z * z) **) + + let ggcd a b = + match a with + | Z0 -> (abs b),(Z0,(sgn b)) + | Zpos a0 -> + (match b with + | Z0 -> (abs a),((sgn a),Z0) + | Zpos b0 -> + let g,p = Coq_Pos.ggcd a0 b0 in + let aa,bb = p in (Zpos g),((Zpos aa),(Zpos bb)) + | Zneg b0 -> + let g,p = Coq_Pos.ggcd a0 b0 in + let aa,bb = p in (Zpos g),((Zpos aa),(Zneg bb))) + | Zneg a0 -> + (match b with + | Z0 -> (abs a),((sgn a),Z0) + | Zpos b0 -> + let g,p = Coq_Pos.ggcd a0 b0 in + let aa,bb = p in (Zpos g),((Zneg aa),(Zpos bb)) + | Zneg b0 -> + let g,p = Coq_Pos.ggcd a0 b0 in + let aa,bb = p in (Zpos g),((Zneg aa),(Zneg bb))) + + (** val testbit : z -> z -> bool **) + + let testbit a = function + | Z0 -> odd a + | Zpos p -> + (match a with + | Z0 -> false + | Zpos a0 -> Coq_Pos.testbit a0 (Npos p) + | Zneg a0 -> negb (N.testbit (Coq_Pos.pred_N a0) (Npos p))) + | Zneg p -> false + + (** val shiftl : z -> z -> z **) + + let shiftl a = function + | Z0 -> a + | Zpos p -> Coq_Pos.iter p (mul (Zpos (XO XH))) a + | Zneg p -> Coq_Pos.iter p div2 a + + (** val shiftr : z -> z -> z **) + + let shiftr a n0 = + shiftl a (opp n0) + + (** val coq_lor : z -> z -> z **) + + let coq_lor a b = + match a with + | Z0 -> b + | Zpos a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> Zpos (Coq_Pos.coq_lor a0 b0) + | Zneg b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N b0) (Npos a0)))) + | Zneg a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> Zneg (N.succ_pos (N.ldiff (Coq_Pos.pred_N a0) (Npos b0))) + | Zneg b0 -> + Zneg + (N.succ_pos (N.coq_land (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0)))) + + (** val coq_land : z -> z -> z **) + + let coq_land a b = + match a with + | Z0 -> Z0 + | Zpos a0 -> + (match b with + | Z0 -> Z0 + | Zpos b0 -> of_N (Coq_Pos.coq_land a0 b0) + | Zneg b0 -> of_N (N.ldiff (Npos a0) (Coq_Pos.pred_N b0))) + | Zneg a0 -> + (match b with + | Z0 -> Z0 + | Zpos b0 -> of_N (N.ldiff (Npos b0) (Coq_Pos.pred_N a0)) + | Zneg b0 -> + Zneg + (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0)))) + + (** val ldiff : z -> z -> z **) + + let ldiff a b = + match a with + | Z0 -> Z0 + | Zpos a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> of_N (Coq_Pos.ldiff a0 b0) + | Zneg b0 -> of_N (N.coq_land (Npos a0) (Coq_Pos.pred_N b0))) + | Zneg a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> + Zneg (N.succ_pos (N.coq_lor (Coq_Pos.pred_N a0) (Npos b0))) + | Zneg b0 -> of_N (N.ldiff (Coq_Pos.pred_N b0) (Coq_Pos.pred_N a0))) + + (** val coq_lxor : z -> z -> z **) + + let coq_lxor a b = + match a with + | Z0 -> b + | Zpos a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> of_N (Coq_Pos.coq_lxor a0 b0) + | Zneg b0 -> + Zneg (N.succ_pos (N.coq_lxor (Npos a0) (Coq_Pos.pred_N b0)))) + | Zneg a0 -> + (match b with + | Z0 -> a + | Zpos b0 -> + Zneg (N.succ_pos (N.coq_lxor (Coq_Pos.pred_N a0) (Npos b0))) + | Zneg b0 -> of_N (N.coq_lxor (Coq_Pos.pred_N a0) (Coq_Pos.pred_N b0))) + + (** val eq_dec : z -> z -> bool **) + + let eq_dec x y = + match x with + | Z0 -> + (match y with + | Z0 -> true + | _ -> false) + | Zpos x0 -> + (match y with + | Zpos p2 -> Coq_Pos.eq_dec x0 p2 + | _ -> false) + | Zneg x0 -> + (match y with + | Zneg p2 -> Coq_Pos.eq_dec x0 p2 + | _ -> false) + + module BootStrap = + struct + + end + + module OrderElts = + struct + type t = z + end + + module OrderTac = MakeOrderTac(OrderElts) + + (** val sqrt_up : z -> z **) + + let sqrt_up a = + match compare Z0 a with + | Lt -> succ (sqrt (pred a)) + | _ -> Z0 + + (** val log2_up : z -> z **) + + let log2_up a = + match compare (Zpos XH) a with + | Lt -> succ (log2 (pred a)) + | _ -> Z0 + + module NZDivP = + struct + + end + + module Quot2Div = + struct + (** val div : z -> z -> z **) + + let div = + quot + + (** val modulo : z -> z -> z **) + + let modulo = + rem + end + + module NZQuot = + struct + + end + + (** val lcm : z -> z -> z **) + + let lcm a b = + abs (mul a (div b (gcd a b))) + + (** val b2z : bool -> z **) + + let b2z = function + | true -> Zpos XH + | false -> Z0 + + (** val setbit : z -> z -> z **) + + let setbit a n0 = + coq_lor a (shiftl (Zpos XH) n0) + + (** val clearbit : z -> z -> z **) + + let clearbit a n0 = + ldiff a (shiftl (Zpos XH) n0) + + (** val lnot : z -> z **) + + let lnot a = + pred (opp a) + + (** val ones : z -> z **) + + let ones n0 = + pred (shiftl (Zpos XH) n0) + + module T = + struct + + end + + module ORev = + struct + type t = z + end + + module MRev = + struct + (** val max : z -> z -> z **) + + let max x y = + min y x + end + + module MPRev = MaxLogicalProperties(ORev)(MRev) + + module P = + struct + (** val max_case_strong : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let max_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat n0 (max n0 m) __ (hl __) + | _ -> compat m (max n0 m) __ (hr __)) + + (** val max_case : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 x1 = + max_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val max_dec : z -> z -> bool **) + + let max_dec n0 m = + max_case n0 m (fun x y _ h0 -> h0) true false + + (** val min_case_strong : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) + -> 'a1 **) + + let min_case_strong n0 m compat hl hr = + let c = compSpec2Type n0 m (compare n0 m) in + (match c with + | CompGtT -> compat m (min n0 m) __ (hr __) + | _ -> compat n0 (min n0 m) __ (hl __)) + + (** val min_case : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 x1 = + min_case_strong n0 m x (fun _ -> x0) (fun _ -> x1) + + (** val min_dec : z -> z -> bool **) + + let min_dec n0 m = + min_case n0 m (fun x y _ h0 -> h0) true false + end + + (** val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let max_case_strong n0 m x x0 = + P.max_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val max_case : z -> z -> 'a1 -> 'a1 -> 'a1 **) + + let max_case n0 m x x0 = + max_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val max_dec : z -> z -> bool **) + + let max_dec = + P.max_dec + + (** val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) + + let min_case_strong n0 m x x0 = + P.min_case_strong n0 m (fun x1 y _ x2 -> x2) x x0 + + (** val min_case : z -> z -> 'a1 -> 'a1 -> 'a1 **) + + let min_case n0 m x x0 = + min_case_strong n0 m (fun _ -> x) (fun _ -> x0) + + (** val min_dec : z -> z -> bool **) + + let min_dec = + P.min_dec + end (** val zeq_bool : z -> z -> bool **) let zeq_bool x y = - match zcompare x y with + match Z.compare x y with | Eq -> true | _ -> false -(** val pgcdn : nat -> positive -> positive -> positive **) - -let rec pgcdn n0 a b = - match n0 with - | O -> XH - | S n1 -> - (match a with - | XI a' -> - (match b with - | XI b' -> - (match pcompare a' b' Eq with - | Eq -> a - | Lt -> pgcdn n1 (pminus b' a') a - | Gt -> pgcdn n1 (pminus a' b') b) - | XO b0 -> pgcdn n1 a b0 - | XH -> XH) - | XO a0 -> - (match b with - | XI p -> pgcdn n1 a0 b - | XO b0 -> XO (pgcdn n1 a0 b0) - | XH -> XH) - | XH -> XH) - -(** val pgcd : positive -> positive -> positive **) - -let pgcd a b = - pgcdn (plus (psize a) (psize b)) a b - -(** val zgcd : z -> z -> z **) - -let zgcd a b = - match a with - | Z0 -> zabs b - | Zpos a0 -> - (match b with - | Z0 -> zabs a - | Zpos b0 -> Zpos (pgcd a0 b0) - | Zneg b0 -> Zpos (pgcd a0 b0)) - | Zneg a0 -> - (match b with - | Z0 -> zabs a - | Zpos b0 -> Zpos (pgcd a0 b0) - | Zneg b0 -> Zpos (pgcd a0 b0)) - -(** val zdiv_eucl_POS : positive -> z -> z * z **) - -let rec zdiv_eucl_POS a b = - match a with - | XI a' -> - let q0,r = zdiv_eucl_POS a' b in - let r' = zplus (zmult (Zpos (XO XH)) r) (Zpos XH) in - if zgt_bool b r' - then (zmult (Zpos (XO XH)) q0),r' - else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),(zminus r' b) - | XO a' -> - let q0,r = zdiv_eucl_POS a' b in - let r' = zmult (Zpos (XO XH)) r in - if zgt_bool b r' - then (zmult (Zpos (XO XH)) q0),r' - else (zplus (zmult (Zpos (XO XH)) q0) (Zpos XH)),(zminus r' b) - | XH -> if zge_bool b (Zpos (XO XH)) then Z0,(Zpos XH) else (Zpos XH),Z0 - -(** val zdiv_eucl : z -> z -> z * z **) - -let zdiv_eucl a b = - match a with - | Z0 -> Z0,Z0 - | Zpos a' -> - (match b with - | Z0 -> Z0,Z0 - | Zpos p -> zdiv_eucl_POS a' b - | Zneg b' -> - let q0,r = zdiv_eucl_POS a' (Zpos b') in - (match r with - | Z0 -> (zopp q0),Z0 - | _ -> (zopp (zplus q0 (Zpos XH))),(zplus b r))) - | Zneg a' -> - (match b with - | Z0 -> Z0,Z0 - | Zpos p -> - let q0,r = zdiv_eucl_POS a' b in - (match r with - | Z0 -> (zopp q0),Z0 - | _ -> (zopp (zplus q0 (Zpos XH))),(zminus b r)) - | Zneg b' -> let q0,r = zdiv_eucl_POS a' (Zpos b') in q0,(zopp r)) - -(** val zdiv : z -> z -> z **) - -let zdiv a b = - let q0,x = zdiv_eucl a b in q0 - type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -516,14 +2803,14 @@ let rec peq ceqb p p' = | Pinj (j, q0) -> (match p' with | Pinj (j', q') -> - (match pcompare j j' Eq with + (match Coq_Pos.compare j j' with | Eq -> peq ceqb q0 q' | _ -> false) | _ -> false) | PX (p2, i, q0) -> (match p' with | PX (p'0, i', q') -> - (match pcompare i i' Eq with + (match Coq_Pos.compare i i' with | Eq -> if peq ceqb p2 p'0 then peq ceqb q0 q' else false | _ -> false) | _ -> false) @@ -532,7 +2819,7 @@ let rec peq ceqb p p' = let mkPinj j p = match p with | Pc c -> p -| Pinj (j', q0) -> Pinj ((pplus j j'), q0) +| Pinj (j', q0) -> Pinj ((Coq_Pos.add j j'), q0) | PX (p2, p3, p4) -> Pinj (j, p) (** val mkPinj_pred : positive -> 'a1 pol -> 'a1 pol **) @@ -540,7 +2827,7 @@ let mkPinj j p = match p with let mkPinj_pred j p = match j with | XI j0 -> Pinj ((XO j0), p) - | XO j0 -> Pinj ((pdouble_minus_one j0), p) + | XO j0 -> Pinj ((Coq_Pos.pred_double j0), p) | XH -> p (** val mkPX : @@ -551,7 +2838,9 @@ let mkPX cO ceqb p i q0 = | Pc c -> if ceqb c cO then mkPinj XH q0 else PX (p, i, q0) | Pinj (p2, p3) -> PX (p, i, q0) | PX (p', i', q') -> - if peq ceqb q' (p0 cO) then PX (p', (pplus i' i), q0) else PX (p, i, q0) + if peq ceqb q' (p0 cO) + then PX (p', (Coq_Pos.add i' i), q0) + else PX (p, i, q0) (** val mkXi : 'a1 -> 'a1 -> positive -> 'a1 pol **) @@ -593,14 +2882,14 @@ let rec psubC csub p c = let rec paddI cadd pop q0 j = function | Pc c -> mkPinj j (paddC cadd q0 c) | Pinj (j', q') -> - (match zPminus j' j with + (match Z.pos_sub j' j with | Z0 -> mkPinj j (pop q' q0) | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) | Zneg k -> mkPinj j' (paddI cadd pop q0 k q')) | PX (p2, i, q') -> (match j with | XI j0 -> PX (p2, i, (paddI cadd pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (paddI cadd pop q0 (pdouble_minus_one j0) q')) + | XO j0 -> PX (p2, i, (paddI cadd pop q0 (Coq_Pos.pred_double j0) q')) | XH -> PX (p2, i, (pop q' q0))) (** val psubI : @@ -610,14 +2899,15 @@ let rec paddI cadd pop q0 j = function let rec psubI cadd copp pop q0 j = function | Pc c -> mkPinj j (paddC cadd (popp copp q0) c) | Pinj (j', q') -> - (match zPminus j' j with + (match Z.pos_sub j' j with | Z0 -> mkPinj j (pop q' q0) | Zpos k -> mkPinj j (pop (Pinj (k, q')) q0) | Zneg k -> mkPinj j' (psubI cadd copp pop q0 k q')) | PX (p2, i, q') -> (match j with | XI j0 -> PX (p2, i, (psubI cadd copp pop q0 (XO j0) q')) - | XO j0 -> PX (p2, i, (psubI cadd copp pop q0 (pdouble_minus_one j0) q')) + | XO j0 -> + PX (p2, i, (psubI cadd copp pop q0 (Coq_Pos.pred_double j0) q')) | XH -> PX (p2, i, (pop q' q0))) (** val paddX : @@ -629,10 +2919,10 @@ let rec paddX cO ceqb pop p' i' p = match p with | Pinj (j, q') -> (match j with | XI j0 -> PX (p', i', (Pinj ((XO j0), q'))) - | XO j0 -> PX (p', i', (Pinj ((pdouble_minus_one j0), q'))) + | XO j0 -> PX (p', i', (Pinj ((Coq_Pos.pred_double j0), q'))) | XH -> PX (p', i', q')) | PX (p2, i, q') -> - (match zPminus i i' with + (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (pop p2 p') i q' | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' | Zneg k -> mkPX cO ceqb (paddX cO ceqb pop p' k p2) i q') @@ -646,10 +2936,10 @@ let rec psubX cO copp ceqb pop p' i' p = match p with | Pinj (j, q') -> (match j with | XI j0 -> PX ((popp copp p'), i', (Pinj ((XO j0), q'))) - | XO j0 -> PX ((popp copp p'), i', (Pinj ((pdouble_minus_one j0), q'))) + | XO j0 -> PX ((popp copp p'), i', (Pinj ((Coq_Pos.pred_double j0), q'))) | XH -> PX ((popp copp p'), i', q')) | PX (p2, i, q') -> - (match zPminus i i' with + (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (pop p2 p') i q' | Zpos k -> mkPX cO ceqb (pop (PX (p2, k, (p0 cO))) p') i' q' | Zneg k -> mkPX cO ceqb (psubX cO copp ceqb pop p' k p2) i q') @@ -669,10 +2959,10 @@ let rec padd cO cadd ceqb p = function | XI j0 -> PX (p'0, i', (padd cO cadd ceqb (Pinj ((XO j0), q0)) q')) | XO j0 -> PX (p'0, i', - (padd cO cadd ceqb (Pinj ((pdouble_minus_one j0), q0)) q')) + (padd cO cadd ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q')) | XH -> PX (p'0, i', (padd cO cadd ceqb q0 q'))) | PX (p2, i, q0) -> - (match zPminus i i' with + (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (padd cO cadd ceqb p2 p'0) i (padd cO cadd ceqb q0 q') | Zpos k -> @@ -699,11 +2989,11 @@ let rec psub cO cadd csub copp ceqb p = function (psub cO cadd csub copp ceqb (Pinj ((XO j0), q0)) q')) | XO j0 -> PX ((popp copp p'0), i', - (psub cO cadd csub copp ceqb (Pinj ((pdouble_minus_one j0), q0)) + (psub cO cadd csub copp ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q')) | XH -> PX ((popp copp p'0), i', (psub cO cadd csub copp ceqb q0 q'))) | PX (p2, i, q0) -> - (match zPminus i i' with + (match Z.pos_sub i i' with | Z0 -> mkPX cO ceqb (psub cO cadd csub copp ceqb p2 p'0) i (psub cO cadd csub copp ceqb q0 q') @@ -743,7 +3033,7 @@ let pmulC cO cI cmul ceqb p c = let rec pmulI cO cI cmul ceqb pmul0 q0 j = function | Pc c -> mkPinj j (pmulC cO cI cmul ceqb q0 c) | Pinj (j', q') -> - (match zPminus j' j with + (match Z.pos_sub j' j with | Z0 -> mkPinj j (pmul0 q' q0) | Zpos k -> mkPinj j (pmul0 (Pinj (k, q')) q0) | Zneg k -> mkPinj j' (pmulI cO cI cmul ceqb pmul0 q0 k q')) @@ -754,7 +3044,7 @@ let rec pmulI cO cI cmul ceqb pmul0 q0 j = function (pmulI cO cI cmul ceqb pmul0 q0 (XO j') q') | XO j' -> mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 j p') i' - (pmulI cO cI cmul ceqb pmul0 q0 (pdouble_minus_one j') q') + (pmulI cO cI cmul ceqb pmul0 q0 (Coq_Pos.pred_double j') q') | XH -> mkPX cO ceqb (pmulI cO cI cmul ceqb pmul0 q0 XH p') i' (pmul0 q' q0)) @@ -773,7 +3063,7 @@ let rec pmul cO cI cadd cmul ceqb p p'' = match p'' with match j with | XI j0 -> pmul cO cI cadd cmul ceqb (Pinj ((XO j0), q0)) q' | XO j0 -> - pmul cO cI cadd cmul ceqb (Pinj ((pdouble_minus_one j0), q0)) q' + pmul cO cI cadd cmul ceqb (Pinj ((Coq_Pos.pred_double j0), q0)) q' | XH -> pmul cO cI cadd cmul ceqb q0 q' in mkPX cO ceqb (pmul cO cI cadd cmul ceqb p p') i' qQ' @@ -883,6 +3173,18 @@ type 'a bFormula = | N of 'a bFormula | I of 'a bFormula * 'a bFormula +(** val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula **) + +let rec map_bformula fct = function +| TT -> TT +| FF -> FF +| X -> X +| A a -> A (fct a) +| Cj (f1, f2) -> Cj ((map_bformula fct f1), (map_bformula fct f2)) +| D (f1, f2) -> D ((map_bformula fct f1), (map_bformula fct f2)) +| N f0 -> N (map_bformula fct f0) +| I (f1, f2) -> I ((map_bformula fct f1), (map_bformula fct f2)) + type 'term' clause = 'term' list type 'term' cnf = 'term' clause list @@ -901,21 +3203,21 @@ let ff = ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 -> 'a1 clause -> 'a1 clause option **) -let rec add_term unsat deduce t0 = function +let rec add_term unsat deduce t1 = function | [] -> - (match deduce t0 t0 with - | Some u -> if unsat u then None else Some (t0::[]) - | None -> Some (t0::[])) + (match deduce t1 t1 with + | Some u -> if unsat u then None else Some (t1::[]) + | None -> Some (t1::[])) | t'::cl0 -> - (match deduce t0 t' with + (match deduce t1 t' with | Some u -> if unsat u then None - else (match add_term unsat deduce t0 cl0 with + else (match add_term unsat deduce t1 cl0 with | Some cl' -> Some (t'::cl') | None -> None) | None -> - (match add_term unsat deduce t0 cl0 with + (match add_term unsat deduce t1 cl0 with | Some cl' -> Some (t'::cl') | None -> None)) @@ -926,8 +3228,8 @@ let rec add_term unsat deduce t0 = function let rec or_clause unsat deduce cl1 cl2 = match cl1 with | [] -> Some cl2 - | t0::cl -> - (match add_term unsat deduce t0 cl2 with + | t1::cl -> + (match add_term unsat deduce t1 cl2 with | Some cl' -> or_clause unsat deduce cl cl' | None -> None) @@ -935,9 +3237,9 @@ let rec or_clause unsat deduce cl1 cl2 = ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> 'a1 clause -> 'a1 cnf -> 'a1 cnf **) -let or_clause_cnf unsat deduce t0 f = +let or_clause_cnf unsat deduce t1 f = fold_right (fun e acc -> - match or_clause unsat deduce t0 e with + match or_clause unsat deduce t1 e with | Some cl -> cl::acc | None -> acc) [] f @@ -1175,7 +3477,7 @@ type op2 = | OpLt | OpGt -type 'c formula = { flhs : 'c pExpr; fop : op2; frhs : 'c pExpr } +type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr } (** val flhs : 'a1 formula -> 'a1 pExpr **) @@ -1215,8 +3517,8 @@ let padd0 cO cplus ceqb = -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list **) -let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in +let xnormalise cO cI cplus ctimes cminus copp ceqb t1 = + let { flhs = lhs; fop = o; frhs = rhs } = t1 in let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in (match o with @@ -1236,16 +3538,16 @@ let xnormalise cO cI cplus ctimes cminus copp ceqb t0 = -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula cnf **) -let cnf_normalise cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t0) +let cnf_normalise cO cI cplus ctimes cminus copp ceqb t1 = + map (fun x -> x::[]) (xnormalise cO cI cplus ctimes cminus copp ceqb t1) (** val xnegate : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula list **) -let xnegate cO cI cplus ctimes cminus copp ceqb t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in +let xnegate cO cI cplus ctimes cminus copp ceqb t1 = + let { flhs = lhs; fop = o; frhs = rhs } = t1 in let lhs0 = norm cO cI cplus ctimes cminus copp ceqb lhs in let rhs0 = norm cO cI cplus ctimes cminus copp ceqb rhs in (match o with @@ -1265,32 +3567,49 @@ let xnegate cO cI cplus ctimes cminus copp ceqb t0 = -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula cnf **) -let cnf_negate cO cI cplus ctimes cminus copp ceqb t0 = - map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t0) +let cnf_negate cO cI cplus ctimes cminus copp ceqb t1 = + map (fun x -> x::[]) (xnegate cO cI cplus ctimes cminus copp ceqb t1) (** val xdenorm : positive -> 'a1 pol -> 'a1 pExpr **) let rec xdenorm jmp = function | Pc c -> PEc c -| Pinj (j, p2) -> xdenorm (pplus j jmp) p2 +| Pinj (j, p2) -> xdenorm (Coq_Pos.add j jmp) p2 | PX (p2, j, q0) -> PEadd ((PEmul ((xdenorm jmp p2), (PEpow ((PEX jmp), (Npos j))))), - (xdenorm (psucc jmp) q0)) + (xdenorm (Coq_Pos.succ jmp) q0)) (** val denorm : 'a1 pol -> 'a1 pExpr **) let denorm p = xdenorm XH p +(** val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr **) + +let rec map_PExpr c_of_S = function +| PEc c -> PEc (c_of_S c) +| PEX p -> PEX p +| PEadd (e1, e2) -> PEadd ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) +| PEsub (e1, e2) -> PEsub ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) +| PEmul (e1, e2) -> PEmul ((map_PExpr c_of_S e1), (map_PExpr c_of_S e2)) +| PEopp e0 -> PEopp (map_PExpr c_of_S e0) +| PEpow (e0, n0) -> PEpow ((map_PExpr c_of_S e0), n0) + +(** val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula **) + +let map_Formula c_of_S f = + let { flhs = l; fop = o; frhs = r } = f in + { flhs = (map_PExpr c_of_S l); fop = o; frhs = (map_PExpr c_of_S r) } + (** val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz **) let simpl_cone cO cI ctimes ceqb e = match e with -| PsatzSquare t0 -> - (match t0 with +| PsatzSquare t1 -> + (match t1 with | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c) - | _ -> PsatzSquare t0) + | _ -> PsatzSquare t1) | PsatzMulE (t1, t2) -> (match t1 with | PsatzMulE (x, x0) -> @@ -1354,28 +3673,28 @@ let qden x = x.qden (** val qeq_bool : q -> q -> bool **) let qeq_bool x y = - zeq_bool (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden)) + zeq_bool (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) (** val qle_bool : q -> q -> bool **) let qle_bool x y = - zle_bool (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden)) + Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)) (** val qplus : q -> q -> q **) let qplus x y = - { qnum = (zplus (zmult x.qnum (Zpos y.qden)) (zmult y.qnum (Zpos x.qden))); - qden = (pmult x.qden y.qden) } + { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))); + qden = (Coq_Pos.mul x.qden y.qden) } (** val qmult : q -> q -> q **) let qmult x y = - { qnum = (zmult x.qnum y.qnum); qden = (pmult x.qden y.qden) } + { qnum = (Z.mul x.qnum y.qnum); qden = (Coq_Pos.mul x.qden y.qden) } (** val qopp : q -> q **) let qopp x = - { qnum = (zopp x.qnum); qden = x.qden } + { qnum = (Z.opp x.qnum); qden = x.qden } (** val qminus : q -> q -> q **) @@ -1402,12 +3721,12 @@ let qpower q0 = function | Zpos p -> qpower_positive q0 p | Zneg p -> qinv (qpower_positive q0 p) -type 'a t = +type 'a t0 = | Empty | Leaf of 'a -| Node of 'a t * 'a * 'a t +| Node of 'a t0 * 'a * 'a t0 -(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **) +(** val find : 'a1 -> 'a1 t0 -> positive -> 'a1 **) let rec find default vm p = match vm with @@ -1424,27 +3743,27 @@ type zWitness = z psatz (** val zWeakChecker : z nFormula list -> z psatz -> bool **) let zWeakChecker = - check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool + check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb (** val psub1 : z pol -> z pol -> z pol **) let psub1 = - psub0 Z0 zplus zminus zopp zeq_bool + psub0 Z0 Z.add Z.sub Z.opp zeq_bool (** val padd1 : z pol -> z pol -> z pol **) let padd1 = - padd0 Z0 zplus zeq_bool + padd0 Z0 Z.add zeq_bool (** val norm0 : z pExpr -> z pol **) let norm0 = - norm Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool + norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp zeq_bool (** val xnormalise0 : z formula -> z nFormula list **) -let xnormalise0 t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in +let xnormalise0 t1 = + let { flhs = lhs; fop = o; frhs = rhs } = t1 in let lhs0 = norm0 lhs in let rhs0 = norm0 rhs in (match o with @@ -1461,13 +3780,13 @@ let xnormalise0 t0 = (** val normalise : z formula -> z nFormula cnf **) -let normalise t0 = - map (fun x -> x::[]) (xnormalise0 t0) +let normalise t1 = + map (fun x -> x::[]) (xnormalise0 t1) (** val xnegate0 : z formula -> z nFormula list **) -let xnegate0 t0 = - let { flhs = lhs; fop = o; frhs = rhs } = t0 in +let xnegate0 t1 = + let { flhs = lhs; fop = o; frhs = rhs } = t1 in let lhs0 = norm0 lhs in let rhs0 = norm0 rhs in (match o with @@ -1484,26 +3803,26 @@ let xnegate0 t0 = (** val negate : z formula -> z nFormula cnf **) -let negate t0 = - map (fun x -> x::[]) (xnegate0 t0) +let negate t1 = + map (fun x -> x::[]) (xnegate0 t1) (** val zunsat : z nFormula -> bool **) let zunsat = - check_inconsistent Z0 zeq_bool zle_bool + check_inconsistent Z0 zeq_bool Z.leb (** val zdeduce : z nFormula -> z nFormula -> z nFormula option **) let zdeduce = - nformula_plus_nformula Z0 zplus zeq_bool + nformula_plus_nformula Z0 Z.add zeq_bool (** val ceiling : z -> z -> z **) let ceiling a b = - let q0,r = zdiv_eucl a b in + let q0,r = Z.div_eucl a b in (match r with | Z0 -> q0 - | _ -> zplus q0 (Zpos XH)) + | _ -> Z.add q0 (Zpos XH)) type zArithProof = | DoneProof @@ -1514,7 +3833,7 @@ type zArithProof = (** val zgcdM : z -> z -> z **) let zgcdM x y = - zmax (zgcd x y) (Zpos XH) + Z.max (Z.gcd x y) (Zpos XH) (** val zgcd_pol : z polC -> z * z **) @@ -1529,7 +3848,7 @@ let rec zgcd_pol = function let rec zdiv_pol p x = match p with - | Pc c -> Pc (zdiv c x) + | Pc c -> Pc (Z.div c x) | Pinj (j, p2) -> Pinj (j, (zdiv_pol p2 x)) | PX (p2, j, q0) -> PX ((zdiv_pol p2 x), j, (zdiv_pol q0 x)) @@ -1537,8 +3856,8 @@ let rec zdiv_pol p x = let makeCuttingPlane p = let g,c = zgcd_pol p in - if zgt_bool g Z0 - then (zdiv_pol (psubC zminus p c) g),(zopp (ceiling (zopp c) g)) + if Z.gtb g Z0 + then (zdiv_pol (psubC Z.sub p c) g),(Z.opp (ceiling (Z.opp c) g)) else p,Z0 (** val genCuttingPlane : z nFormula -> ((z polC * z) * op1) option **) @@ -1548,12 +3867,12 @@ let genCuttingPlane = function (match op with | Equal -> let g,c = zgcd_pol e in - if (&&) (zgt_bool g Z0) - ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (zgcd g c) g))) + if (&&) (Z.gtb g Z0) + ((&&) (negb (zeq_bool c Z0)) (negb (zeq_bool (Z.gcd g c) g))) then None else Some ((makeCuttingPlane e),Equal) | NonEqual -> Some ((e,Z0),op) - | Strict -> Some ((makeCuttingPlane (psubC zminus e (Zpos XH))),NonStrict) + | Strict -> Some ((makeCuttingPlane (psubC Z.sub e (Zpos XH))),NonStrict) | NonStrict -> Some ((makeCuttingPlane e),NonStrict)) (** val nformula_of_cutting_plane : ((z polC * z) * op1) -> z nFormula **) @@ -1573,7 +3892,7 @@ let is_pol_Z0 = function (** val eval_Psatz0 : z nFormula list -> zWitness -> z nFormula option **) let eval_Psatz0 = - eval_Psatz Z0 (Zpos XH) zplus zmult zeq_bool zle_bool + eval_Psatz Z0 (Zpos XH) Z.add Z.mul zeq_bool Z.leb (** val valid_cut_sign : op1 -> bool **) @@ -1614,11 +3933,11 @@ let rec zChecker l = function (is_pol_Z0 (padd1 e1 e2)) then let rec label pfs lb ub = match pfs with - | [] -> zgt_bool lb ub + | [] -> Z.gtb lb ub | pf1::rsr -> (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1) - (label rsr (zplus lb (Zpos XH)) ub) - in label pf0 (zopp z1) z2 + (label rsr (Z.add lb (Zpos XH)) ub) + in label pf0 (Z.opp z1) z2 else false | None -> true) | None -> true) @@ -1630,12 +3949,6 @@ let rec zChecker l = function let zTautoChecker f w = tauto_checker zunsat zdeduce normalise negate zChecker f w -(** val n_of_Z : z -> n **) - -let n_of_Z = function -| Zpos p -> Npos p -| _ -> N0 - type qWitness = q psatz (** val qWeakChecker : q nFormula list -> q psatz -> bool **) @@ -1671,35 +3984,63 @@ let qdeduce = let qTautoChecker f w = tauto_checker qunsat qdeduce qnormalise qnegate qWeakChecker f w -type rWitness = z psatz - -(** val rWeakChecker : z nFormula list -> z psatz -> bool **) +type rcst = +| C0 +| C1 +| CQ of q +| CZ of z +| CPlus of rcst * rcst +| CMinus of rcst * rcst +| CMult of rcst * rcst +| CInv of rcst +| COpp of rcst + +(** val q_of_Rcst : rcst -> q **) + +let rec q_of_Rcst = function +| C0 -> { qnum = Z0; qden = XH } +| C1 -> { qnum = (Zpos XH); qden = XH } +| CQ q0 -> q0 +| CZ z0 -> { qnum = z0; qden = XH } +| CPlus (r1, r2) -> qplus (q_of_Rcst r1) (q_of_Rcst r2) +| CMinus (r1, r2) -> qminus (q_of_Rcst r1) (q_of_Rcst r2) +| CMult (r1, r2) -> qmult (q_of_Rcst r1) (q_of_Rcst r2) +| CInv r0 -> qinv (q_of_Rcst r0) +| COpp r0 -> qopp (q_of_Rcst r0) + +type rWitness = q psatz + +(** val rWeakChecker : q nFormula list -> q psatz -> bool **) let rWeakChecker = - check_normalised_formulas Z0 (Zpos XH) zplus zmult zeq_bool zle_bool + check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH); + qden = XH } qplus qmult qeq_bool qle_bool -(** val rnormalise : z formula -> z nFormula cnf **) +(** val rnormalise : q formula -> q nFormula cnf **) let rnormalise = - cnf_normalise Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool + cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } + qplus qmult qminus qopp qeq_bool -(** val rnegate : z formula -> z nFormula cnf **) +(** val rnegate : q formula -> q nFormula cnf **) let rnegate = - cnf_negate Z0 (Zpos XH) zplus zmult zminus zopp zeq_bool + cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus + qmult qminus qopp qeq_bool -(** val runsat : z nFormula -> bool **) +(** val runsat : q nFormula -> bool **) let runsat = - check_inconsistent Z0 zeq_bool zle_bool + check_inconsistent { qnum = Z0; qden = XH } qeq_bool qle_bool -(** val rdeduce : z nFormula -> z nFormula -> z nFormula option **) +(** val rdeduce : q nFormula -> q nFormula -> q nFormula option **) let rdeduce = - nformula_plus_nformula Z0 zplus zeq_bool + nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool -(** val rTautoChecker : z formula bFormula -> rWitness list -> bool **) +(** val rTautoChecker : rcst formula bFormula -> rWitness list -> bool **) let rTautoChecker f w = - tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker f w + tauto_checker runsat rdeduce rnormalise rnegate rWeakChecker + (map_bformula (map_Formula q_of_Rcst) f) w -- cgit v1.2.3