diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-20 17:01:54 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-05-20 17:01:54 +0000 |
| commit | 7da3e3d85c88eb42e932230048cb0db255474b5d (patch) | |
| tree | 0cd987e72b528d88c5a2a6bbcfa1d0718a74efa6 /plugins/micromega | |
| parent | 4c6c284ddc6db47f070026ad68b5c29f6737c4a0 (diff) | |
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
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 13 | ||||
| -rw-r--r-- | plugins/micromega/Psatz.v | 1 | ||||
| -rw-r--r-- | plugins/micromega/RMicromega.v | 481 | ||||
| -rw-r--r-- | plugins/micromega/RingMicromega.v | 81 | ||||
| -rw-r--r-- | plugins/micromega/Tauto.v | 33 | ||||
| -rw-r--r-- | plugins/micromega/ZMicromega.v | 2 | ||||
| -rw-r--r-- | plugins/micromega/certificate.ml | 4 | ||||
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 370 | ||||
| -rw-r--r-- | plugins/micromega/micromega.ml | 3371 | ||||
| -rw-r--r-- | plugins/micromega/micromega.mli | 924 |
10 files changed, 4530 insertions, 750 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 9b55eea45..19a98f876 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -38,11 +38,24 @@ Extract Inductive sumor => option [ Some None ]. Let's rather use the ocaml && *) Extract Inlined Constant andb => "(&&)". +Require Import Reals. + +Extract Constant R => "int". +Extract Constant R0 => "0". +Extract Constant R1 => "1". +Extract Constant Rplus => "( + )". +Extract Constant Rmult => "( * )". +Extract Constant Ropp => "fun x -> - x". +Extract Constant Rinv => "fun x -> 1 / x". + Extraction "micromega.ml" List.map simpl_cone (*map_cone indexes*) denorm Qpower n_of_Z N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. + + + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 84ce85f29..325cc31bb 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -66,6 +66,7 @@ Ltac psatzl dom := change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) | R => + unfold Rdiv in * ; psatzl_R ; (* If csdp is not installed, the previous step might not produce any progress: the rest of the tactical will then fail. Hence the 'try'. *) diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 406b4ba25..eb4847486 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -16,6 +16,9 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. Require Import Raxioms RIneq Rpow_def DiscrR. +Require Import QArith. +Require Import Qfield. + Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -60,32 +63,405 @@ Proof. apply (Rmult_lt_compat_r) ; auto. Qed. -Require ZMicromega. -(* R with coeffs in Z *) +Definition Q2R := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R. + + +Lemma Rinv_elim : forall x y z, + y <> 0 -> (z * y = x <-> x * / y = z). +Proof. + intros. + split ; intros. + subst. + rewrite Rmult_assoc. + rewrite Rinv_r; auto. + ring. + subst. + rewrite Rmult_assoc. + rewrite (Rmult_comm (/ y)). + rewrite Rinv_r ; auto. + ring. +Qed. + +Ltac INR_nat_of_P := + match goal with + | H : context[INR (nat_of_P ?X)] |- _ => + revert H ; + let HH := fresh in + assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X)) + | |- context[INR (nat_of_P ?X)] => + let HH := fresh in + assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (nat_of_P X)) + end. + +Ltac add_eq expr val := set (temp := expr) ; + generalize (refl_equal temp) ; + unfold temp at 1 ; generalize temp ; intro val ; clear temp. + +Ltac Rinv_elim := + match goal with + | |- context[?x * / ?y] => + let z := fresh "v" in + add_eq (x * / y) z ; + let H := fresh in intro H ; rewrite <- Rinv_elim in H + end. + +Lemma Rlt_neq : forall r , 0 < r -> r <> 0. +Proof. + red. intros. + subst. + apply (Rlt_irrefl 0 H). +Qed. + + +Lemma Rinv_1 : forall x, x * / 1 = x. +Proof. + intro. + Rinv_elim. + subst ; ring. + apply R1_neq_R0. +Qed. + +Lemma Qeq_true : forall x y, + Qeq_bool x y = true -> + Q2R x = Q2R y. +Proof. + unfold Q2R. + simpl. + intros. + apply Qeq_bool_eq in H. + unfold Qeq in H. + assert (IZR (Qnum x * ' Qden y) = IZR (Qnum y * ' Qden x))%Z. + rewrite H. reflexivity. + repeat rewrite mult_IZR in H0. + simpl in H0. + revert H0. + repeat INR_nat_of_P. + intros. + apply Rinv_elim in H2 ; [| apply Rlt_neq ; auto]. + rewrite <- H2. + field. + split ; apply Rlt_neq ; auto. +Qed. + +Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y. +Proof. + intros. + apply Qeq_bool_neq in H. + intro. apply H. clear H. + unfold Qeq,Q2R in *. + simpl in *. + revert H0. + repeat Rinv_elim. + intros. + subst. + assert (IZR (Qnum x * ' Qden y)%Z = IZR (Qnum y * ' Qden x)%Z). + repeat rewrite mult_IZR. + simpl. + rewrite <- H0. rewrite <- H. + ring. + apply eq_IZR ; auto. + INR_nat_of_P; intros; apply Rlt_neq ; auto. + INR_nat_of_P; intros ; apply Rlt_neq ; auto. +Qed. + + + +Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y. +Proof. + intros. + apply Qle_bool_imp_le in H. + unfold Qle in H. + unfold Q2R. + simpl in *. + apply IZR_le in H. + repeat rewrite mult_IZR in H. + simpl in H. + repeat INR_nat_of_P; intros. + assert (Hr := Rlt_neq r H). + assert (Hr0 := Rlt_neq r0 H0). + replace (IZR (Qnum x) * / r) with ((IZR (Qnum x) * r0) * (/r * /r0)). + replace (IZR (Qnum y) * / r0) with ((IZR (Qnum y) * r) * (/r * /r0)). + apply Rmult_le_compat_r ; auto. + apply Rmult_le_pos. + unfold Rle. left. apply Rinv_0_lt_compat ; auto. + unfold Rle. left. apply Rinv_0_lt_compat ; auto. + field ; intuition. + field ; intuition. +Qed. + + + +Lemma Q2R_0 : Q2R 0 = 0. +Proof. + compute. apply Rinv_1. +Qed. + +Lemma Q2R_1 : Q2R 1 = 1. +Proof. + compute. apply Rinv_1. +Qed. + +Lemma Q2R_plus : forall x y, Q2R (x + y) = Q2R x + Q2R y. +Proof. + intros. + unfold Q2R. + simpl in *. + rewrite plus_IZR in *. + rewrite mult_IZR in *. + simpl. + rewrite nat_of_P_mult_morphism. + rewrite mult_INR. + rewrite mult_IZR. + simpl. + repeat INR_nat_of_P. + intros. field. + split ; apply Rlt_neq ; auto. +Qed. + +Lemma Q2R_opp : forall x, Q2R (- x) = - Q2R x. +Proof. + intros. + unfold Q2R. + simpl. + rewrite opp_IZR. + ring. +Qed. + +Lemma Q2R_minus : forall x y, Q2R (x - y) = Q2R x - Q2R y. +Proof. + intros. + unfold Qminus. + rewrite Q2R_plus. + rewrite Q2R_opp. + ring. +Qed. + + +Lemma Q2R_mult : forall x y, Q2R (x * y) = Q2R x * Q2R y. +Proof. + unfold Q2R ; intros. + simpl. + repeat rewrite mult_IZR. + simpl. + rewrite nat_of_P_mult_morphism. + rewrite mult_INR. + repeat INR_nat_of_P. + intros. field ; split ; apply Rlt_neq ; auto. +Qed. + +Lemma Q2R_inv_lt : forall x, (0 < x)%Q -> + Q2R (/ x) = / Q2R x. +Proof. + unfold Q2R ; simpl. + intros. + unfold Qlt in H. + revert H. + simpl. + intros. + unfold Qinv. + destruct x ; simpl in *. + destruct Qnum ; simpl. + exfalso. auto with zarith. + clear H. + repeat INR_nat_of_P. + intros. + assert (HH := Rlt_neq _ H). + assert (HH0 := Rlt_neq _ H0). + rewrite Rinv_mult_distr ; auto. + rewrite Rinv_involutive ; auto. + ring. + apply Rinv_0_lt_compat in H0. + apply Rlt_neq ; auto. + simpl in H. + exfalso. + rewrite Pmult_comm in H. + compute in H. + discriminate. +Qed. + +Lemma Qinv_opp : forall x, (- (/ x) = / ( -x))%Q. +Proof. + destruct x ; destruct Qnum ; reflexivity. +Qed. + +Lemma Qopp_involutive_strong : forall x, (- - x = x)%Q. +Proof. + intros. + destruct x. + unfold Qopp. + simpl. + rewrite Zopp_involutive. + reflexivity. +Qed. + +Lemma Ropp_0 : forall r , - r = 0 -> r = 0. +Proof. + intros. + rewrite <- (Ropp_involutive r). + apply Ropp_eq_0_compat ; auto. +Qed. + +Lemma Q2R_x_0 : forall x, Q2R x = 0 -> x == 0%Q. +Proof. + destruct x ; simpl. + unfold Q2R. + simpl. + INR_nat_of_P. + intros. + apply Rmult_integral in H0. + destruct H0. + apply eq_IZR_R0 in H0. + subst. + reflexivity. + exfalso. + apply Rinv_0_lt_compat in H. + rewrite <- H0 in H. + apply Rlt_irrefl in H. auto. +Qed. + + +Lemma Q2R_inv_gt : forall x, (0 > x)%Q -> + Q2R (/ x) = / Q2R x. +Proof. + intros. + rewrite <- (Qopp_involutive_strong x). + rewrite <- Qinv_opp. + rewrite Q2R_opp. + rewrite Q2R_inv_lt. + repeat rewrite Q2R_opp. + rewrite Ropp_inv_permute. + auto. + intro. + apply Ropp_0 in H0. + apply Q2R_x_0 in H0. + rewrite H0 in H. + compute in H. discriminate. + unfold Qlt in *. + destruct x ; simpl in *. + auto with zarith. +Qed. + +Lemma Q2R_inv : forall x, ~ x == 0 -> + Q2R (/ x) = / Q2R x. +Proof. + intros. + assert ( 0 > x \/ 0 < x)%Q. + destruct x ; unfold Qlt, Qeq in * ; simpl in *. + rewrite Zmult_1_r in *. + destruct Qnum ; simpl in * ; intuition auto. + right. reflexivity. + left ; reflexivity. + destruct H0. + apply Q2R_inv_gt ; auto. + apply Q2R_inv_lt ; auto. +Qed. + +Lemma Q2R_inv_ext : forall x, + Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x). +Proof. + intros. + case_eq (Qeq_bool x 0). + intros. + apply Qeq_bool_eq in H. + destruct x ; simpl. + unfold Qeq in H. + simpl in H. + replace Qnum with 0%Z. + compute. rewrite Rinv_1. + reflexivity. + rewrite <- H. ring. + intros. + apply Q2R_inv. + intro. + rewrite <- Qeq_bool_iff in H0. + congruence. +Qed. + + +Notation to_nat := N.to_nat. (*Nnat.nat_of_N*) -Lemma RZSORaddon : - SORaddon R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) - 0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *) - Zeq_bool Zle_bool - IZR nat_of_N pow. +Lemma QSORaddon : + @SORaddon R + R0 R1 Rplus Rmult Rminus Ropp (@eq R) Rle (* ring elements *) + Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *) + Qeq_bool Qle_bool + Q2R nat to_nat pow. Proof. constructor. constructor ; intros ; try reflexivity. - apply plus_IZR. - symmetry. apply Z_R_minus. - apply mult_IZR. - apply Ropp_Ropp_IZR. - apply IZR_eq. - apply Zeq_bool_eq ; auto. + apply Q2R_0. + apply Q2R_1. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. + apply Q2R_opp. + apply Qeq_true ; auto. apply R_power_theory. - intros x y. - intro. - apply IZR_neq. - apply Zeq_bool_neq ; auto. - intros. apply IZR_le. apply Zle_bool_imp_le. auto. + apply Qeq_false. + apply Qle_true. Qed. +(* Syntactic ring coefficients. + For computing, we use Q. *) +Inductive Rcst := +| C0 +| C1 +| CQ (r : Q) +| CZ (r : Z) +| CPlus (r1 r2 : Rcst) +| CMinus (r1 r2 : Rcst) +| CMult (r1 r2 : Rcst) +| CInv (r : Rcst) +| COpp (r : Rcst). + + +Fixpoint Q_of_Rcst (r : Rcst) : Q := + match r with + | C0 => 0 # 1 + | C1 => 1 # 1 + | CZ z => z # 1 + | CQ q => q + | 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 r => Qinv (Q_of_Rcst r) + | COpp r => Qopp (Q_of_Rcst r) + end. + + +Fixpoint R_of_Rcst (r : Rcst) : R := + match r with + | C0 => R0 + | C1 => R1 + | CZ z => IZR z + | CQ q => Q2R q + | CPlus r1 r2 => (R_of_Rcst r1) + (R_of_Rcst r2) + | CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2) + | CMult r1 r2 => (R_of_Rcst r1) * (R_of_Rcst r2) + | CInv r => + if Qeq_bool (Q_of_Rcst r) (0 # 1) + then R0 + else Rinv (R_of_Rcst r) + | COpp r => - (R_of_Rcst r) + end. + +Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c. +Proof. + induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2). + apply Q2R_0. + apply Q2R_1. + reflexivity. + unfold Q2R. simpl. rewrite Rinv_1. reflexivity. + apply Q2R_plus. + apply Q2R_minus. + apply Q2R_mult. + rewrite <- IHc. + apply Q2R_inv_ext. + rewrite <- IHc. + apply Q2R_opp. + Qed. + Require Import EnvRing. Definition INZ (n:N) : R := @@ -94,7 +470,7 @@ Definition INZ (n:N) : R := | Npos p => IZR (Zpos p) end. -Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp IZR nat_of_N pow. +Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp R_of_Rcst nat_of_N pow. Definition Reval_op2 (o:Op2) : R -> R -> Prop := @@ -108,11 +484,15 @@ Definition Reval_op2 (o:Op2) : R -> R -> Prop := end. -Definition Reval_formula (e: PolEnv R) (ff : Formula Z) := +Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) := let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs). + Definition Reval_formula' := - eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR nat_of_N pow. + eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt nat_of_N pow R_of_Rcst. + +Definition QReval_formula := + eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R nat_of_N pow . Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f. Proof. @@ -126,69 +506,74 @@ Proof. apply Rle_ge. Qed. -Definition Reval_nformula := - eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt IZR. +Definition Qeval_nformula := + eval_nformula 0 Rplus Rmult (@eq R) Rle Rlt Q2R. -Lemma Reval_nformula_dec : forall env d, (Reval_nformula env d) \/ ~ (Reval_nformula env d). +Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d). Proof. - exact (fun env d =>eval_nformula_dec Rsor IZR env d). + exact (fun env d =>eval_nformula_dec Rsor Q2R env d). Qed. -Definition RWitness := Psatz Z. +Definition RWitness := Psatz Q. -Definition RWeakChecker := check_normalised_formulas 0%Z 1%Z Zplus Zmult Zeq_bool Zle_bool. +Definition RWeakChecker := check_normalised_formulas 0%Q 1%Q Qplus Qmult Qeq_bool Qle_bool. Require Import List. -Lemma RWeakChecker_sound : forall (l : list (NFormula Z)) (cm : RWitness), +Lemma RWeakChecker_sound : forall (l : list (NFormula Q)) (cm : RWitness), RWeakChecker l cm = true -> - forall env, make_impl (Reval_nformula env) l False. + forall env, make_impl (Qeval_nformula env) l False. Proof. intros l cm H. intro. - unfold Reval_nformula. - apply (checker_nf_sound Rsor RZSORaddon l cm). + unfold Qeval_nformula. + apply (checker_nf_sound Rsor QSORaddon l cm). unfold RWeakChecker in H. exact H. Qed. Require Import Tauto. -Definition Rnormalise := @cnf_normalise Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. -Definition Rnegate := @cnf_negate Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool. - -Definition runsat := check_inconsistent 0%Z Zeq_bool Zle_bool. +Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. +Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool. -Definition rdeduce := nformula_plus_nformula 0%Z Zplus Zeq_bool. +Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool. +Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool. - -Definition RTautoChecker (f : BFormula (Formula Z)) (w: list RWitness) : bool := - @tauto_checker (Formula Z) (NFormula Z) +Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool := + @tauto_checker (Formula Q) (NFormula Q) runsat rdeduce Rnormalise Rnegate - RWitness RWeakChecker f w. + RWitness RWeakChecker (map_bformula (map_Formula Q_of_Rcst) f) w. Lemma RTautoChecker_sound : forall f w, RTautoChecker f w = true -> forall env, eval_f (Reval_formula env) f. Proof. intros f w. unfold RTautoChecker. - apply (tauto_checker_sound Reval_formula Reval_nformula). + intros TC env. + apply (tauto_checker_sound QReval_formula Qeval_nformula) with (env := env) in TC. + rewrite eval_f_map in TC. + rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto. + intro. + unfold QReval_formula. + rewrite <- eval_formulaSC with (phiS := R_of_Rcst). + rewrite Reval_formula_compat. + tauto. + intro. rewrite Q_of_RcstR. reflexivity. apply Reval_nformula_dec. - intros until env. - unfold eval_nformula. unfold RingMicromega.eval_nformula. destruct t. - apply (check_inconsistent_sound Rsor RZSORaddon) ; auto. - unfold rdeduce. apply (nformula_plus_nformula_correct Rsor RZSORaddon). - intros. rewrite Reval_formula_compat. - unfold Reval_formula'. now apply (cnf_normalise_correct Rsor RZSORaddon). - intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor RZSORaddon). + apply (check_inconsistent_sound Rsor QSORaddon) ; auto. + unfold rdeduce. apply (nformula_plus_nformula_correct Rsor QSORaddon). + now apply (cnf_normalise_correct Rsor QSORaddon). + intros. now apply (cnf_negate_correct Rsor QSORaddon). intros t w0. apply RWeakChecker_sound. Qed. + (* Local Variables: *) (* coding: utf-8 *) (* End: *) diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index e658ad237..7b4fdb089 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -687,13 +687,13 @@ end. Definition eval_pexpr (l : PolEnv) (pe : PExpr C) : R := PEeval rplus rtimes rminus ropp phi pow_phi rpow l pe. -Record Formula : Type := { - Flhs : PExpr C; +Record Formula (T:Type) : Type := { + Flhs : PExpr T; Fop : Op2; - Frhs : PExpr C + Frhs : PExpr T }. -Definition eval_formula (env : PolEnv) (f : Formula) : Prop := +Definition eval_formula (env : PolEnv) (f : Formula C) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs). @@ -706,7 +706,7 @@ Definition psub := Psub cO cplus cminus copp ceqb. Definition padd := Padd cO cplus ceqb. -Definition normalise (f : Formula) : NFormula := +Definition normalise (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in let rhs := norm rhs in @@ -719,7 +719,7 @@ let (lhs, op, rhs) := f in | OpLt => (psub rhs lhs, Strict) end. -Definition negate (f : Formula) : NFormula := +Definition negate (f : Formula C) : NFormula := let (lhs, op, rhs) := f in let lhs := norm lhs in let rhs := norm rhs in @@ -755,7 +755,7 @@ Qed. Theorem normalise_sound : - forall (env : PolEnv) (f : Formula), + forall (env : PolEnv) (f : Formula C), eval_formula env f -> eval_nformula env (normalise f). Proof. intros env f H; destruct f as [lhs op rhs]; simpl in *. @@ -769,7 +769,7 @@ now apply -> (Rlt_lt_minus sor). Qed. Theorem negate_correct : - forall (env : PolEnv) (f : Formula), + forall (env : PolEnv) (f : Formula C), eval_formula env f <-> ~ (eval_nformula env (negate f)). Proof. intros env f; destruct f as [lhs op rhs]; simpl. @@ -785,7 +785,7 @@ Qed. (** Another normalisation - this is used for cnf conversion **) -Definition xnormalise (t:Formula) : list (NFormula) := +Definition xnormalise (t:Formula C) : list (NFormula) := let (lhs,o,rhs) := t in let lhs := norm lhs in let rhs := norm rhs in @@ -801,7 +801,7 @@ Definition xnormalise (t:Formula) : list (NFormula) := Require Import Tauto. -Definition cnf_normalise (t:Formula) : cnf (NFormula) := +Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). @@ -826,7 +826,7 @@ Proof. rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). auto. Qed. -Definition xnegate (t:Formula) : list (NFormula) := +Definition xnegate (t:Formula C) : list (NFormula) := let (lhs,o,rhs) := t in let lhs := norm lhs in let rhs := norm rhs in @@ -839,7 +839,7 @@ Definition xnegate (t:Formula) : list (NFormula) := | OpLe => (psub rhs lhs,NonStrict) :: nil end. -Definition cnf_negate (t:Formula) : cnf (NFormula) := +Definition cnf_negate (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnegate t). Lemma cnf_negate_correct : forall env t, eval_cnf eval_nformula env (cnf_negate t) -> ~ eval_formula env t. @@ -937,6 +937,63 @@ Proof. Qed. +(** Sometimes it is convenient to make a distinction between "syntactic" coefficients and "real" +coefficients that are used to actually compute *) + + + +Variable S : Type. + +Variable C_of_S : S -> C. + +Variable phiS : S -> R. + +Variable phi_C_of_S : forall c, phiS c = phi (C_of_S c). + +Fixpoint map_PExpr (e : PExpr S) : PExpr C := + match e with + | PEc c => PEc (C_of_S c) + | PEX p => PEX _ p + | PEadd e1 e2 => PEadd (map_PExpr e1) (map_PExpr e2) + | PEsub e1 e2 => PEsub (map_PExpr e1) (map_PExpr e2) + | PEmul e1 e2 => PEmul (map_PExpr e1) (map_PExpr e2) + | PEopp e => PEopp (map_PExpr e) + | PEpow e n => PEpow (map_PExpr e) n + end. + +Definition map_Formula (f : Formula S) : Formula C := + let (l,o,r) := f in + Build_Formula (map_PExpr l) o (map_PExpr r). + + +Definition eval_sexpr (env : PolEnv) (e : PExpr S) : R := + PEeval rplus rtimes rminus ropp phiS pow_phi rpow env e. + +Definition eval_sformula (env : PolEnv) (f : Formula S) : Prop := + let (lhs, op, rhs) := f in + (eval_op2 op) (eval_sexpr env lhs) (eval_sexpr env rhs). + +Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s). +Proof. + unfold eval_pexpr, eval_sexpr. + induction s ; simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity. + apply phi_C_of_S. + rewrite IHs. reflexivity. + rewrite IHs. reflexivity. +Qed. + +(** equality migth be (too) strong *) +Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f). +Proof. + destruct f. + simpl. + repeat rewrite eval_pexprSC. + reflexivity. +Qed. + + + + (** Some syntactic simplifications of expressions *) diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v index ed7a104e8..b3ccdfcc4 100644 --- a/plugins/micromega/Tauto.v +++ b/plugins/micromega/Tauto.v @@ -41,6 +41,37 @@ Set Implicit Arguments. | I f1 f2 => (eval_f ev f1) -> (eval_f ev f2) end. + Lemma eval_f_morph : forall A (ev ev' : A -> Prop) (f : BFormula A), + (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f). + Proof. + induction f ; simpl ; try tauto. + intros. + assert (H' := H a). + auto. + Qed. + + + + Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U := + match f with + | TT => TT _ + | FF => FF _ + | X p => X _ p + | 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 f => N (map_bformula fct f) + | I f1 f2 => I (map_bformula fct f1) (map_bformula fct f2) + end. + + Lemma eval_f_map : forall T U (fct: T-> U) env f , + eval_f env (map_bformula fct f) = eval_f (fun x => env (fct x)) f. + Proof. + induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto. + rewrite <- IHf. auto. + Qed. + + Lemma map_simpl : forall A B f l, @map A B f l = match l with | nil => nil @@ -52,6 +83,7 @@ Set Implicit Arguments. + Section S. Variable Env : Type. @@ -480,7 +512,6 @@ Set Implicit Arguments. - End S. (* Local Variables: *) diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index 6dad2ba60..f840e471b 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -8,7 +8,7 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2011 *) (* *) (************************************************************************) diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 6e8018b91..5efe9f426 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -43,7 +43,7 @@ let z_spec = { number_to_num = (fun x -> Big_int (C2Ml.z_big_int x)); zero = Mc.Z0; unit = Mc.Zpos Mc.XH; - mult = Mc.zmult; + mult = Mc.Z.mul; eqb = Mc.zeq_bool } @@ -579,7 +579,7 @@ let q_cert_of_pos pos = | Sub(t1,t2) -> PEsub (term_to_z_expr t1, term_to_z_expr t2) | _ -> failwith "term_to_z_expr: not implemented" - let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.zplus Mc.zmult Mc.zminus Mc.zopp Mc.zeq_bool (term_to_z_expr e) + let term_to_z_pol e = Mc.norm_aux (Ml2C.z 0) (Ml2C.z 1) Mc.Z.add Mc.Z.mul Mc.Z.sub Mc.Z.opp Mc.zeq_bool (term_to_z_expr e) let z_cert_of_pos pos = let s,pos = (scale_certificate pos) in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ebf44e74c..69ec518ee 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -55,7 +55,7 @@ type 'cst atom = 'cst Micromega.formula * Micromega's encoding of formulas. * By order of appearance: boolean constants, variables, atoms, conjunctions, * disjunctions, negation, implication. - *) +*) type 'cst formula = | TT @@ -86,6 +86,18 @@ let rec pp_formula o f = | None -> "") pp_formula f2 | N(f) -> Printf.fprintf o "N(%a)" pp_formula f + +let rec map_atoms fct f = + match f with + | TT -> TT + | FF -> FF + | X x -> X x + | A (at,tg,cstr) -> A(fct at,tg,cstr) + | C (f1,f2) -> C(map_atoms fct f1, map_atoms fct f2) + | D (f1,f2) -> D(map_atoms fct f1, map_atoms fct f2) + | N f -> N(map_atoms fct f) + | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2) + (** * Collect the identifiers of a (string of) implications. Implication labels * are inherited from Coq/CoC's higher order dependent type constructor (Pi). @@ -272,6 +284,7 @@ struct ["RingMicromega"]; ["EnvRing"]; ["Coq"; "micromega"; "ZMicromega"]; + ["Coq"; "micromega"; "RMicromega"]; ["Coq" ; "micromega" ; "Tauto"]; ["Coq" ; "micromega" ; "RingMicromega"]; ["Coq" ; "micromega" ; "EnvRing"]; @@ -284,7 +297,8 @@ struct let r_modules = [["Coq";"Reals" ; "Rdefinitions"]; - ["Coq";"Reals" ; "Rpow_def"]] + ["Coq";"Reals" ; "Rpow_def"] ; +] (** * Initialization : a large amount of Caml symbols are derived from @@ -335,6 +349,19 @@ struct let coq_Build_Witness = lazy (constant "Build_Witness") let coq_Qmake = lazy (constant "Qmake") + + let coq_Rcst = lazy (constant "Rcst") + let coq_C0 = lazy (constant "C0") + let coq_C1 = lazy (constant "C1") + let coq_CQ = lazy (constant "CQ") + let coq_CZ = lazy (constant "CZ") + let coq_CPlus = lazy (constant "CPlus") + let coq_CMinus = lazy (constant "CMinus") + let coq_CMult = lazy (constant "CMult") + let coq_CInv = lazy (constant "CInv") + let coq_COpp = lazy (constant "COpp") + + let coq_R0 = lazy (constant "R0") let coq_R1 = lazy (constant "R1") @@ -377,7 +404,11 @@ struct let coq_Rminus = lazy (r_constant "Rminus") let coq_Ropp = lazy (r_constant "Ropp") let coq_Rmult = lazy (r_constant "Rmult") + let coq_Rdiv = lazy (r_constant "Rdiv") + let coq_Rinv = lazy (r_constant "Rinv") let coq_Rpower = lazy (r_constant "pow") + let coq_Q2R = lazy (constant "Q2R") + let coq_IZR = lazy (constant "IZR") let coq_PEX = lazy (constant "PEX" ) let coq_PEc = lazy (constant"PEc") @@ -589,6 +620,48 @@ struct else raise ParseError | _ -> raise ParseError + + let rec pp_Rcst o cst = + match cst with + | Mc.C0 -> output_string o "C0" + | Mc.C1 -> output_string o "C1" + | Mc.CQ q -> output_string o "CQ _" + | Mc.CZ z -> pp_z o z + | Mc.CPlus(x,y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y + | Mc.CMinus(x,y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y + | Mc.CMult(x,y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y + | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t + | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t + + + let rec dump_Rcst cst = + match cst with + | Mc.C0 -> Lazy.force coq_C0 + | Mc.C1 -> Lazy.force coq_C1 + | Mc.CQ q -> Term.mkApp(Lazy.force coq_CQ, [| dump_q q |]) + | Mc.CZ z -> Term.mkApp(Lazy.force coq_CZ, [| dump_z z |]) + | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CInv t -> Term.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) + | Mc.COpp t -> Term.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) + + let rec parse_Rcst term = + let (i,c) = get_left_construct term in + match i with + | 1 -> Mc.C0 + | 2 -> Mc.C1 + | 3 -> Mc.CQ (parse_q c.(0)) + | 4 -> Mc.CPlus(parse_Rcst c.(0), parse_Rcst c.(1)) + | 5 -> Mc.CMinus(parse_Rcst c.(0), parse_Rcst c.(1)) + | 6 -> Mc.CMult(parse_Rcst c.(0), parse_Rcst c.(1)) + | 7 -> Mc.CInv(parse_Rcst c.(0)) + | 8 -> Mc.COpp(parse_Rcst c.(0)) + | _ -> raise ParseError + + + + let rec parse_list parse_elt term = let (i,c) = get_left_construct term in match i with @@ -824,12 +897,17 @@ struct then (Pp.pp (Pp.str "parse_expr: "); Pp.pp_flush ();Pp.pp (Printer.prterm term); Pp.pp_flush ()); +(* let constant_or_variable env term = try ( Mc.PEc (parse_constant term) , env) with ParseError -> let (env,n) = Env.compute_rank_add env term in (Mc.PEX n , env) in +*) + let parse_variable env term = + let (env,n) = Env.compute_rank_add env term in + (Mc.PEX n , env) in let rec parse_expr env term = let combine env op (t1,t2) = @@ -837,32 +915,34 @@ struct let (expr2,env) = parse_expr env t2 in (op expr1 expr2,env) in - match kind_of_term term with - | App(t,args) -> - ( - match kind_of_term t with - | Const c -> - ( match assoc_ops t ops_spec with - | Binop f -> combine env f (args.(0),args.(1)) - | Opp -> let (expr,env) = parse_expr env args.(0) in - (Mc.PEopp expr, env) - | Power -> - begin - try - let (expr,env) = parse_expr env args.(0) in - let power = (parse_exp expr args.(1)) in - (power , env) - with _ -> (* if the exponent is a variable *) - let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) - end - | Ukn s -> - if debug - then (Printf.printf "unknown op: %s\n" s; flush stdout;); - let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) + try (Mc.PEc (parse_constant term) , env) + with ParseError -> + match kind_of_term term with + | App(t,args) -> + ( + match kind_of_term t with + | Const c -> + ( match assoc_ops t ops_spec with + | Binop f -> combine env f (args.(0),args.(1)) + | Opp -> let (expr,env) = parse_expr env args.(0) in + (Mc.PEopp expr, env) + | Power -> + begin + try + let (expr,env) = parse_expr env args.(0) in + let power = (parse_exp expr args.(1)) in + (power , env) + with _ -> (* if the exponent is a variable *) + let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) + end + | Ukn s -> + if debug + then (Printf.printf "unknown op: %s\n" s; flush stdout;); + let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env) + ) + | _ -> parse_variable env term ) - | _ -> constant_or_variable env term - ) - | _ -> constant_or_variable env term in + | _ -> parse_variable env term in parse_expr env term let zop_spec = @@ -892,27 +972,57 @@ struct let zconstant = parse_z let qconstant = parse_q - let rconstant term = - if debug - then (Pp.pp_flush (); - Pp.pp (Pp.str "rconstant: "); - Pp.pp (Printer.prterm term); Pp.pp_flush ()); + + let rconst_assoc = + [ + coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ; + coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ; + coq_Rmult , (fun x y -> Mc.CMult(x,y)) ; + coq_Rdiv , (fun x y -> Mc.CMult(x,Mc.CInv y)) ; + ] + + let rec rconstant term = match Term.kind_of_term term with | Const x -> if term = Lazy.force coq_R0 - then Mc.Z0 + then Mc.C0 else if term = Lazy.force coq_R1 - then Mc.Zpos Mc.XH + then Mc.C1 else raise ParseError + | App(op,args) -> + begin + try + (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1)) + with + ParseError -> + match op with + | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0)) + | op when op = Lazy.force coq_Q2R -> Mc.CQ (parse_q args.(0)) +(* | op when op = Lazy.force coq_IZR -> Mc.CZ (parse_z args.(0))*) + | _ -> raise ParseError + end + | _ -> raise ParseError + + let rconstant term = + if debug + then (Pp.pp_flush (); + Pp.pp (Pp.str "rconstant: "); + Pp.pp (Printer.prterm term); Pp.pp_flush ()); + let res = rconstant term in + if debug then + (Printf.printf "rconstant -> %a" pp_Rcst res ; flush stdout) ; + res + + let parse_zexpr = parse_expr zconstant (fun expr x -> let exp = (parse_z x) in match exp with | Mc.Zneg _ -> Mc.PEc Mc.Z0 - | _ -> Mc.PEpow(expr, Mc.n_of_Z exp)) + | _ -> Mc.PEpow(expr, Mc.Z.to_N exp)) zop_spec let parse_qexpr = parse_expr @@ -926,14 +1036,14 @@ struct | Mc.PEc q -> Mc.PEc (Mc.qpower q exp) | _ -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError end - | _ -> let exp = Mc.n_of_Z exp in + | _ -> let exp = Mc.Z.to_N exp in Mc.PEpow(expr,exp)) qop_spec let parse_rexpr = parse_expr rconstant (fun expr x -> - let exp = Mc.n_of_nat (parse_nat x) in + let exp = Mc.N.of_nat (parse_nat x) in Mc.PEpow(expr,exp)) rop_spec @@ -1019,7 +1129,7 @@ struct | _ when term = Lazy.force coq_True -> (TT,env,tg) | _ when term = Lazy.force coq_False -> (FF,env,tg) | _ -> X(term),env,tg in - xparse_formula env tg (Reductionops.whd_zeta term) + xparse_formula env tg ((*Reductionops.whd_zeta*) term) let dump_formula typ dump_atom f = let rec xdump f = @@ -1216,13 +1326,12 @@ let parse_goal parse_arith env hyps term = (** * The datastructures that aggregate theory-dependent proof values. *) - -type ('d, 'prf) domain_spec = { - typ : Term.constr; (* Z, Q , R *) - coeff : Term.constr ; (* Z, Q *) - dump_coeff : 'd -> Term.constr ; - proof_typ : Term.constr ; - dump_proof : 'prf -> Term.constr +type ('synt_c, 'prf) domain_spec = { + typ : Term.constr; (* is the type of the interpretation domain - Z, Q, R*) + coeff : Term.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) + dump_coeff : 'synt_c -> Term.constr ; + proof_typ : Term.constr ; + dump_proof : 'prf -> Term.constr } let zz_domain_spec = lazy { @@ -1241,12 +1350,12 @@ let qq_domain_spec = lazy { dump_proof = dump_psatz coq_Q dump_q } -let rz_domain_spec = lazy { +let rcst_domain_spec = lazy { typ = Lazy.force coq_R; - coeff = Lazy.force coq_Z; - dump_coeff = dump_z; - proof_typ = Lazy.force coq_ZWitness ; - dump_proof = dump_psatz coq_Z dump_z + coeff = Lazy.force coq_Rcst; + dump_coeff = dump_Rcst; + proof_typ = Lazy.force coq_QWitness ; + dump_proof = dump_psatz coq_Q dump_q } (** @@ -1404,6 +1513,19 @@ let abstract_formula hyps f = | TT -> TT in xabs f + +(* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2 *) +let rec abstract_wrt_formula f1 f2 = + match f1 , f2 with + | X c , _ -> X c + | A _ , A _ -> f2 + | C(a,b) , C(a',b') -> C(abstract_wrt_formula a a', abstract_wrt_formula b b') + | D(a,b) , D(a',b') -> D(abstract_wrt_formula a a', abstract_wrt_formula b b') + | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b') + | FF , FF -> FF + | TT , TT -> TT + | _ -> failwith "abstract_wrt_formula" + (** * This exception is raised by really_call_csdpcert if Coq's configure didn't * find a CSDP executable. @@ -1416,17 +1538,19 @@ exception CsdpNotFound * prune unused fomulas, and finally modify the proof state. *) -let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = - let spec = Lazy.force spec in - - (* Express the goal as one big implication *) - let (ff,ids) = +let formula_hyps_concl hyps concl = List.fold_right (fun (id,f) (cc,ids) -> match f with X _ -> (cc,ids) | _ -> (I(f,Some id,cc), id::ids)) - polys1 (polys2,[]) in + hyps (concl,[]) + + +let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl = + + (* Express the goal as one big implication *) + let (ff,ids) = formula_hyps_concl polys1 polys2 in (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *) let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in @@ -1442,7 +1566,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 end; match witness_list_tags prover cnf_ff with - | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl + | None -> None | Some res -> (*Printf.printf "\nList %i" (List.length `res); *) let hyps = List.fold_left (fun s (cl,(prf,p)) -> let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in @@ -1477,22 +1601,19 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 end ; *) let res' = compact_proofs cnf_ff res cnf_ff' in - let (ff',res',ids) = (ff',res',List.map Term.mkVar (ids_of_formula ff')) in + let (ff',res',ids) = (ff',res', ids_of_formula ff') in let res' = dump_list (spec.proof_typ) spec.dump_proof res' in - (Tacticals.tclTHENSEQ - [ - Tactics.generalize ids ; - micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' - ]) gl + Some (ids,ff',res') + + (** * Parse the proof environment, and call micromega_tauto *) let micromega_gen - parse_arith + parse_arith (negate:'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf) unsat deduce @@ -1502,7 +1623,88 @@ let micromega_gen try let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in let env = Env.elements env in - micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl + let spec = Lazy.force spec in + + match micromega_tauto negate normalise unsat deduce spec prover env hyps concl gl with + | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl + | Some (ids,ff',res') -> + (Tacticals.tclTHENSEQ + [ + Tactics.generalize (List.map Term.mkVar ids) ; + micromega_order_change spec res' + (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff' + ]) gl + with +(* | Failure x -> flush stdout ; Pp.pp_flush () ; + Tacticals.tclFAIL 0 (Pp.str x) gl *) + | ParseError -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl + | CsdpNotFound -> flush stdout ; Pp.pp_flush () ; + Tacticals.tclFAIL 0 (Pp.str + (" Skipping what remains of this tactic: the complexity of the goal requires " + ^ "the use of a specialized external tool called csdp. \n\n" + ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" + ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl + + + +let micromega_order_changer cert env ff gl = + let coeff = Lazy.force coq_Rcst in + let dump_coeff = dump_Rcst in + let typ = Lazy.force coq_R in + let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in + + let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in + let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in + let vm = dump_varmap (typ) env in + Tactics.change_in_concl None + (set + [ + ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, Term.mkApp + (Coqlib.gen_constant_in_modules "VarMap" + [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); + ("__wit", cert, cert_typ) + ] + (Tacmach.pf_concl gl) + ) + gl + + +let micromega_genr prover gl = + let parse_arith = parse_rarith in + let negate = Mc.rnegate in + let normalise = Mc.rnormalise in + let unsat = Mc.runsat in + let deduce = Mc.rdeduce in + let spec = lazy { + typ = Lazy.force coq_R; + coeff = Lazy.force coq_Rcst; + dump_coeff = dump_q; + proof_typ = Lazy.force coq_QWitness ; + dump_proof = dump_psatz coq_Q dump_q + } in + + let concl = Tacmach.pf_concl gl in + let hyps = Tacmach.pf_hyps_types gl in + try + let (hyps,concl,env) = parse_goal parse_arith Env.empty hyps concl in + let env = Env.elements env in + let spec = Lazy.force spec in + + let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in + let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in + + match micromega_tauto negate normalise unsat deduce spec prover env hyps' concl' gl with + | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl + | Some (ids,ff',res') -> + let (ff,ids') = formula_hyps_concl + (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in + + (Tacticals.tclTHENSEQ + [ + Tactics.generalize (List.map Term.mkVar ids) ; + micromega_order_changer res' env (abstract_wrt_formula ff' ff) + ]) gl with (* | Failure x -> flush stdout ; Pp.pp_flush () ; Tacticals.tclFAIL 0 (Pp.str x) gl *) @@ -1514,6 +1716,10 @@ let micromega_gen ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n" ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl + + + + let lift_ratproof prover l = match prover l with | None -> None @@ -1685,15 +1891,17 @@ let linear_prover_Q = { pp_f = fun o x -> pp_pol pp_q o (fst x) } + let linear_prover_R = { name = "linear prover"; - prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec) ; + prover = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ; hyps = hyps_of_cone ; compact = compact_cone ; - pp_prf = pp_psatz pp_z ; - pp_f = fun o x -> pp_pol pp_z o (fst x) + pp_prf = pp_psatz pp_q ; + pp_f = fun o x -> pp_pol pp_q o (fst x) } + let non_linear_prover_Q str o = { name = "real nonlinear prover"; prover = call_csdpcert_q (str, o); @@ -1705,11 +1913,11 @@ let non_linear_prover_Q str o = { let non_linear_prover_R str o = { name = "real nonlinear prover"; - prover = call_csdpcert_z (str, o); + prover = call_csdpcert_q (str, o); hyps = hyps_of_cone; compact = compact_cone; - pp_prf = pp_psatz pp_z; - pp_f = fun o x -> pp_pol pp_z o (fst x) + pp_prf = pp_psatz pp_q; + pp_f = fun o x -> pp_pol pp_q o (fst x) } let non_linear_prover_Z str o = { @@ -1780,13 +1988,14 @@ let psatz_Q i gl = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl + let psatzl_R gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec - [ linear_prover_R ] gl + micromega_genr [ linear_prover_R ] gl + let psatz_R i gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec - [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl + micromega_genr [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl + let psatz_Z i gl = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec @@ -1800,19 +2009,20 @@ let sos_Q gl = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "pure_sos" None ] gl + let sos_R gl = - micromega_gen parse_rarith Mc.rnegate Mc.rnormalise Mc.runsat Mc.rdeduce rz_domain_spec - [ non_linear_prover_R "pure_sos" None ] gl + micromega_genr [ non_linear_prover_R "pure_sos" None ] gl + let xlia gl = try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] gl with z -> (*Printexc.print_backtrace stdout ;*) raise z let xnlia gl = try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec + micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] gl with z -> (*Printexc.print_backtrace stdout ;*) raise z 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 diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli index 675a5a0cc..bcd61f39b 100644 --- a/plugins/micromega/micromega.mli +++ b/plugins/micromega/micromega.mli @@ -1,9 +1,17 @@ +type __ = Obj.t + val negb : bool -> bool type nat = | O | S of nat +val fst : ('a1 * 'a2) -> 'a1 + +val snd : ('a1 * 'a2) -> 'a2 + +val app : 'a1 list -> 'a1 list -> 'a1 list + type comparison = | Eq | Lt @@ -11,109 +19,826 @@ type comparison = val compOpp : comparison -> comparison -val app : 'a1 list -> 'a1 list -> 'a1 list - -val plus : nat -> nat -> nat - -type positive = -| XI of positive -| XO of positive -| XH - -val psucc : positive -> positive - -val pplus : positive -> positive -> positive +type compareSpecT = +| CompEqT +| CompLtT +| CompGtT -val pplus_carry : positive -> positive -> positive +val compareSpec2Type : comparison -> compareSpecT -val p_of_succ_nat : nat -> positive +type 'a compSpecT = compareSpecT -val pdouble_minus_one : positive -> positive +val compSpec2Type : 'a1 -> 'a1 -> comparison -> 'a1 compSpecT -type positive_mask = -| IsNul -| IsPos of positive -| IsNeg +type 'a sig0 = + 'a + (* singleton inductive, whose constructor was exist *) -val pdouble_plus_one_mask : positive_mask -> positive_mask - -val pdouble_mask : positive_mask -> positive_mask - -val pdouble_minus_two : positive -> positive_mask - -val pminus_mask : positive -> positive -> positive_mask - -val pminus_mask_carry : positive -> positive -> positive_mask - -val pminus : positive -> positive -> positive - -val pmult : positive -> positive -> positive +val plus : nat -> nat -> nat -val psize : positive -> nat +val nat_iter : nat -> ('a1 -> 'a1) -> 'a1 -> 'a1 -val pcompare : positive -> positive -> comparison -> comparison +type positive = +| XI of positive +| XO of positive +| XH type n = | N0 | Npos of positive -val n_of_nat : nat -> n - -val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 - -val nth : nat -> 'a1 list -> 'a1 -> 'a1 - -val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list - -val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 - type z = | Z0 | Zpos of positive | Zneg of positive -val zdouble_plus_one : z -> z - -val zdouble_minus_one : z -> z - -val zdouble : z -> z - -val zPminus : positive -> positive -> z +module type TotalOrder' = + sig + type t + end + +module MakeOrderTac : + functor (O:TotalOrder') -> + sig + + end + +module MaxLogicalProperties : + functor (O:TotalOrder') -> + functor (M:sig + val max : O.t -> O.t -> O.t + end) -> + sig + module T : + sig + + end + end + +module Pos : + sig + type t = positive + + val succ : positive -> positive + + val add : positive -> positive -> positive + + val add_carry : positive -> positive -> positive + + val pred_double : positive -> positive + + val pred : positive -> positive + + val pred_N : positive -> n + + type mask = + | IsNul + | IsPos of positive + | IsNeg + + val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 + + val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 + + val succ_double_mask : mask -> mask + + val double_mask : mask -> mask + + val double_pred_mask : positive -> mask + + val pred_mask : mask -> mask + + val sub_mask : positive -> positive -> mask + + val sub_mask_carry : positive -> positive -> mask + + val sub : positive -> positive -> positive + + val mul : positive -> positive -> positive + + val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 + + val pow : positive -> positive -> positive + + val div2 : positive -> positive + + val div2_up : positive -> positive + + val size_nat : positive -> nat + + val size : positive -> positive + + val compare_cont : positive -> positive -> comparison -> comparison + + val compare : positive -> positive -> comparison + + val min : positive -> positive -> positive + + val max : positive -> positive -> positive + + val eqb : positive -> positive -> bool + + val leb : positive -> positive -> bool + + val ltb : positive -> positive -> bool + + val sqrtrem_step : + (positive -> positive) -> (positive -> positive) -> (positive * mask) -> + positive * mask + + val sqrtrem : positive -> positive * mask + + val sqrt : positive -> positive + + val gcdn : nat -> positive -> positive -> positive + + val gcd : positive -> positive -> positive + + val ggcdn : nat -> positive -> positive -> positive * (positive * positive) + + val ggcd : positive -> positive -> positive * (positive * positive) + + val coq_Nsucc_double : n -> n + + val coq_Ndouble : n -> n + + val coq_lor : positive -> positive -> positive + + val coq_land : positive -> positive -> n + + val ldiff : positive -> positive -> n + + val coq_lxor : positive -> positive -> n + + val shiftl_nat : positive -> nat -> positive + + val shiftr_nat : positive -> nat -> positive + + val shiftl : positive -> n -> positive + + val shiftr : positive -> n -> positive + + val testbit_nat : positive -> nat -> bool + + val testbit : positive -> n -> bool + + val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 + + val to_nat : positive -> nat + + val of_nat : nat -> positive + + val of_succ_nat : nat -> positive + end + +module Coq_Pos : + sig + module Coq__1 : sig + type t = positive + end + type t = Coq__1.t + + val succ : positive -> positive + + val add : positive -> positive -> positive + + val add_carry : positive -> positive -> positive + + val pred_double : positive -> positive + + val pred : positive -> positive + + val pred_N : positive -> n + + type mask = Pos.mask = + | IsNul + | IsPos of positive + | IsNeg + + val mask_rect : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 + + val mask_rec : 'a1 -> (positive -> 'a1) -> 'a1 -> mask -> 'a1 + + val succ_double_mask : mask -> mask + + val double_mask : mask -> mask + + val double_pred_mask : positive -> mask + + val pred_mask : mask -> mask + + val sub_mask : positive -> positive -> mask + + val sub_mask_carry : positive -> positive -> mask + + val sub : positive -> positive -> positive + + val mul : positive -> positive -> positive + + val iter : positive -> ('a1 -> 'a1) -> 'a1 -> 'a1 + + val pow : positive -> positive -> positive + + val div2 : positive -> positive + + val div2_up : positive -> positive + + val size_nat : positive -> nat + + val size : positive -> positive + + val compare_cont : positive -> positive -> comparison -> comparison + + val compare : positive -> positive -> comparison + + val min : positive -> positive -> positive + + val max : positive -> positive -> positive + + val eqb : positive -> positive -> bool + + val leb : positive -> positive -> bool + + val ltb : positive -> positive -> bool + + val sqrtrem_step : + (positive -> positive) -> (positive -> positive) -> (positive * mask) -> + positive * mask + + val sqrtrem : positive -> positive * mask + + val sqrt : positive -> positive + + val gcdn : nat -> positive -> positive -> positive + + val gcd : positive -> positive -> positive + + val ggcdn : nat -> positive -> positive -> positive * (positive * positive) + + val ggcd : positive -> positive -> positive * (positive * positive) + + val coq_Nsucc_double : n -> n + + val coq_Ndouble : n -> n + + val coq_lor : positive -> positive -> positive + + val coq_land : positive -> positive -> n + + val ldiff : positive -> positive -> n + + val coq_lxor : positive -> positive -> n + + val shiftl_nat : positive -> nat -> positive + + val shiftr_nat : positive -> nat -> positive + + val shiftl : positive -> n -> positive + + val shiftr : positive -> n -> positive + + val testbit_nat : positive -> nat -> bool + + val testbit : positive -> n -> bool + + val iter_op : ('a1 -> 'a1 -> 'a1) -> positive -> 'a1 -> 'a1 + + val to_nat : positive -> nat + + val of_nat : nat -> positive + + val of_succ_nat : nat -> positive + + val eq_dec : positive -> positive -> bool + + val peano_rect : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 + + val peano_rec : 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> 'a1 + + type coq_PeanoView = + | PeanoOne + | PeanoSucc of positive * coq_PeanoView + + val coq_PeanoView_rect : + 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> + coq_PeanoView -> 'a1 + + val coq_PeanoView_rec : + 'a1 -> (positive -> coq_PeanoView -> 'a1 -> 'a1) -> positive -> + coq_PeanoView -> 'a1 + + val peanoView_xO : positive -> coq_PeanoView -> coq_PeanoView + + val peanoView_xI : positive -> coq_PeanoView -> coq_PeanoView + + val peanoView : positive -> coq_PeanoView + + val coq_PeanoView_iter : + 'a1 -> (positive -> 'a1 -> 'a1) -> positive -> coq_PeanoView -> 'a1 + + val switch_Eq : comparison -> comparison -> comparison + + val mask2cmp : mask -> comparison + + module T : + sig + + end + + module ORev : + sig + type t = Coq__1.t + end + + module MRev : + sig + val max : t -> t -> t + end + + module MPRev : + sig + module T : + sig + + end + end + + module P : + sig + val max_case_strong : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val max_case : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val max_dec : t -> t -> bool + + val min_case_strong : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val min_case : + t -> t -> (t -> t -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val min_dec : t -> t -> bool + end + + val max_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val max_case : t -> t -> 'a1 -> 'a1 -> 'a1 + + val max_dec : t -> t -> bool + + val min_case_strong : t -> t -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val min_case : t -> t -> 'a1 -> 'a1 -> 'a1 + + val min_dec : t -> t -> bool + end + +module N : + sig + type t = n + + val zero : n + + val one : n + + val two : n + + val succ_double : n -> n + + val double : n -> n + + val succ : n -> n + + val pred : n -> n + + val succ_pos : n -> positive + + val add : n -> n -> n + + val sub : n -> n -> n + + val mul : n -> n -> n + + val compare : n -> n -> comparison + + val eqb : n -> n -> bool + + val leb : n -> n -> bool + + val ltb : n -> n -> bool + + val min : n -> n -> n + + val max : n -> n -> n + + val div2 : n -> n + + val even : n -> bool + + val odd : n -> bool + + val pow : n -> n -> n + + val log2 : n -> n + + val size : n -> n + + val size_nat : n -> nat + + val pos_div_eucl : positive -> n -> n * n + + val div_eucl : n -> n -> n * n + + val div : n -> n -> n + + val modulo : n -> n -> n + + val gcd : n -> n -> n + + val ggcd : n -> n -> n * (n * n) + + val sqrtrem : n -> n * n + + val sqrt : n -> n + + val coq_lor : n -> n -> n + + val coq_land : n -> n -> n + + val ldiff : n -> n -> n + + val coq_lxor : n -> n -> n + + val shiftl_nat : n -> nat -> n + + val shiftr_nat : n -> nat -> n + + val shiftl : n -> n -> n + + val shiftr : n -> n -> n + + val testbit_nat : n -> nat -> bool + + val testbit : n -> n -> bool + + val to_nat : n -> nat + + val of_nat : nat -> n + + val iter : n -> ('a1 -> 'a1) -> 'a1 -> 'a1 + + val eq_dec : n -> n -> bool + + val discr : n -> positive option + + val binary_rect : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 + + val binary_rec : 'a1 -> (n -> 'a1 -> 'a1) -> (n -> 'a1 -> 'a1) -> n -> 'a1 + + val peano_rect : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 + + val peano_rec : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 + + module BootStrap : + sig + + end + + val recursion : 'a1 -> (n -> 'a1 -> 'a1) -> n -> 'a1 + + module OrderElts : + sig + type t = n + end + + module OrderTac : + sig + + end + + module NZPowP : + sig + + end + + module NZSqrtP : + sig + + end + + val sqrt_up : n -> n + + val log2_up : n -> n + + module NZDivP : + sig + + end + + val lcm : n -> n -> n + + val b2n : bool -> n + + val setbit : n -> n -> n + + val clearbit : n -> n -> n + + val ones : n -> n + + val lnot : n -> n -> n + + module T : + sig + + end + + module ORev : + sig + type t = n + end + + module MRev : + sig + val max : n -> n -> n + end + + module MPRev : + sig + module T : + sig + + end + end + + module P : + sig + val max_case_strong : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val max_case : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val max_dec : n -> n -> bool + + val min_case_strong : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val min_case : + n -> n -> (n -> n -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val min_dec : n -> n -> bool + end + + val max_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val max_case : n -> n -> 'a1 -> 'a1 -> 'a1 + + val max_dec : n -> n -> bool + + val min_case_strong : n -> n -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val min_case : n -> n -> 'a1 -> 'a1 -> 'a1 + + val min_dec : n -> n -> bool + end -val zplus : z -> z -> z - -val zopp : z -> z - -val zminus : z -> z -> z - -val zmult : z -> z -> z - -val zcompare : z -> z -> comparison - -val zmax : z -> z -> z +val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 -val zabs : z -> z +val nth : nat -> 'a1 list -> 'a1 -> 'a1 -val zle_bool : z -> z -> bool +val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list -val zge_bool : z -> z -> bool +val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1 -val zgt_bool : z -> z -> bool +module Z : + sig + type t = z + + val zero : z + + val one : z + + val two : z + + val double : z -> z + + val succ_double : z -> z + + val pred_double : z -> z + + val pos_sub : positive -> positive -> z + + val add : z -> z -> z + + val opp : z -> z + + val succ : z -> z + + val pred : z -> z + + val sub : z -> z -> z + + val mul : z -> z -> z + + val pow_pos : z -> positive -> z + + val pow : z -> z -> z + + val compare : z -> z -> comparison + + val sgn : z -> z + + val leb : z -> z -> bool + + val geb : z -> z -> bool + + val ltb : z -> z -> bool + + val gtb : z -> z -> bool + + val eqb : z -> z -> bool + + val max : z -> z -> z + + val min : z -> z -> z + + val abs : z -> z + + val abs_nat : z -> nat + + val abs_N : z -> n + + val to_nat : z -> nat + + val to_N : z -> n + + val of_nat : nat -> z + + val of_N : n -> z + + val iter : z -> ('a1 -> 'a1) -> 'a1 -> 'a1 + + val pos_div_eucl : positive -> z -> z * z + + val div_eucl : z -> z -> z * z + + val div : z -> z -> z + + val modulo : z -> z -> z + + val quotrem : z -> z -> z * z + + val quot : z -> z -> z + + val rem : z -> z -> z + + val even : z -> bool + + val odd : z -> bool + + val div2 : z -> z + + val quot2 : z -> z + + val log2 : z -> z + + val sqrtrem : z -> z * z + + val sqrt : z -> z + + val gcd : z -> z -> z + + val ggcd : z -> z -> z * (z * z) + + val testbit : z -> z -> bool + + val shiftl : z -> z -> z + + val shiftr : z -> z -> z + + val coq_lor : z -> z -> z + + val coq_land : z -> z -> z + + val ldiff : z -> z -> z + + val coq_lxor : z -> z -> z + + val eq_dec : z -> z -> bool + + module BootStrap : + sig + + end + + module OrderElts : + sig + type t = z + end + + module OrderTac : + sig + + end + + val sqrt_up : z -> z + + val log2_up : z -> z + + module NZDivP : + sig + + end + + module Quot2Div : + sig + val div : z -> z -> z + + val modulo : z -> z -> z + end + + module NZQuot : + sig + + end + + val lcm : z -> z -> z + + val b2z : bool -> z + + val setbit : z -> z -> z + + val clearbit : z -> z -> z + + val lnot : z -> z + + val ones : z -> z + + module T : + sig + + end + + module ORev : + sig + type t = z + end + + module MRev : + sig + val max : z -> z -> z + end + + module MPRev : + sig + module T : + sig + + end + end + + module P : + sig + val max_case_strong : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val max_case : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val max_dec : z -> z -> bool + + val min_case_strong : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> + 'a1 + + val min_case : + z -> z -> (z -> z -> __ -> 'a1 -> 'a1) -> 'a1 -> 'a1 -> 'a1 + + val min_dec : z -> z -> bool + end + + val max_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val max_case : z -> z -> 'a1 -> 'a1 -> 'a1 + + val max_dec : z -> z -> bool + + val min_case_strong : z -> z -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 + + val min_case : z -> z -> 'a1 -> 'a1 -> 'a1 + + val min_dec : z -> z -> bool + end val zeq_bool : z -> z -> bool -val pgcdn : nat -> positive -> positive -> positive - -val pgcd : positive -> positive -> positive - -val zgcd : z -> z -> z - -val zdiv_eucl_POS : positive -> z -> z * z - -val zdiv_eucl : z -> z -> z * z - -val zdiv : z -> z -> z - type 'c pol = | Pc of 'c | Pinj of positive * 'c pol @@ -219,6 +944,8 @@ type 'a bFormula = | N of 'a bFormula | I of 'a bFormula * 'a bFormula +val map_bformula : ('a1 -> 'a2) -> 'a1 bFormula -> 'a2 bFormula + type 'term' clause = 'term' list type 'term' cnf = 'term' clause list @@ -319,7 +1046,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 @@ -363,6 +1090,10 @@ val xdenorm : positive -> 'a1 pol -> 'a1 pExpr val denorm : 'a1 pol -> 'a1 pExpr +val map_PExpr : ('a2 -> 'a1) -> 'a2 pExpr -> 'a1 pExpr + +val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula + val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz @@ -391,12 +1122,12 @@ val qpower_positive : q -> positive -> q val qpower : q -> z -> q -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 type zWitness = z psatz @@ -450,8 +1181,6 @@ val zChecker : z nFormula list -> zArithProof -> bool val zTautoChecker : z formula bFormula -> zArithProof list -> bool -val n_of_Z : z -> n - type qWitness = q psatz val qWeakChecker : q nFormula list -> q psatz -> bool @@ -466,17 +1195,30 @@ val qdeduce : q nFormula -> q nFormula -> q nFormula option val qTautoChecker : q formula bFormula -> qWitness list -> bool -type rWitness = z psatz +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 + +type rWitness = q psatz -val rWeakChecker : z nFormula list -> z psatz -> bool +val rWeakChecker : q nFormula list -> q psatz -> bool -val rnormalise : z formula -> z nFormula cnf +val rnormalise : q formula -> q nFormula cnf -val rnegate : z formula -> z nFormula cnf +val rnegate : q formula -> q nFormula cnf -val runsat : z nFormula -> bool +val runsat : q nFormula -> bool -val rdeduce : z nFormula -> z nFormula -> z nFormula option +val rdeduce : q nFormula -> q nFormula -> q nFormula option -val rTautoChecker : z formula bFormula -> rWitness list -> bool +val rTautoChecker : rcst formula bFormula -> rWitness list -> bool |