From fc2613e871dffffa788d90044a81598f671d0a3b Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 Jul 2012 16:56:16 +0000 Subject: ZArith + other : favor the use of modern names instead of compat notations - For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/omega/coq_omega.ml | 57 ++++++++++++++++++++++++---------------------- 1 file changed, 30 insertions(+), 27 deletions(-) (limited to 'plugins/omega/coq_omega.ml') diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 2a98cae53..9fa18e7dc 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -173,6 +173,9 @@ let init_constant = gen_constant_in_modules "Omega" init_modules let constant = gen_constant_in_modules "Omega" coq_modules let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]] +let zbase_constant = + gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]] + (* Zarith *) let coq_xH = lazy (constant "xH") @@ -184,20 +187,20 @@ let coq_Zneg = lazy (constant "Zneg") let coq_Z = lazy (constant "Z") let coq_comparison = lazy (constant "comparison") let coq_Gt = lazy (constant "Gt") -let coq_Zplus = lazy (constant "Zplus") -let coq_Zmult = lazy (constant "Zmult") -let coq_Zopp = lazy (constant "Zopp") -let coq_Zminus = lazy (constant "Zminus") -let coq_Zsucc = lazy (constant "Zsucc") -let coq_Zpred = lazy (constant "Zpred") -let coq_Zgt = lazy (constant "Zgt") -let coq_Zle = lazy (constant "Zle") -let coq_Z_of_nat = lazy (constant "Z_of_nat") -let coq_inj_plus = lazy (constant "inj_plus") -let coq_inj_mult = lazy (constant "inj_mult") -let coq_inj_minus1 = lazy (constant "inj_minus1") +let coq_Zplus = lazy (zbase_constant "Z.add") +let coq_Zmult = lazy (zbase_constant "Z.mul") +let coq_Zopp = lazy (zbase_constant "Z.opp") +let coq_Zminus = lazy (zbase_constant "Z.sub") +let coq_Zsucc = lazy (zbase_constant "Z.succ") +let coq_Zpred = lazy (zbase_constant "Z.pred") +let coq_Zgt = lazy (zbase_constant "Z.gt") +let coq_Zle = lazy (zbase_constant "Z.le") +let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat") +let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add") +let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul") +let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub") let coq_inj_minus2 = lazy (constant "inj_minus2") -let coq_inj_S = lazy (z_constant "inj_S") +let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ") let coq_inj_le = lazy (z_constant "Znat.inj_le") let coq_inj_lt = lazy (z_constant "Znat.inj_lt") let coq_inj_ge = lazy (z_constant "Znat.inj_ge") @@ -253,10 +256,10 @@ let coq_Zle_left = lazy (constant "Zle_left") let coq_new_var = lazy (constant "new_var") let coq_intro_Z = lazy (constant "intro_Z") -let coq_dec_eq = lazy (constant "dec_eq") +let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable") let coq_dec_Zne = lazy (constant "dec_Zne") -let coq_dec_Zle = lazy (constant "dec_Zle") -let coq_dec_Zlt = lazy (constant "dec_Zlt") +let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable") +let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable") let coq_dec_Zgt = lazy (constant "dec_Zgt") let coq_dec_Zge = lazy (constant "dec_Zge") @@ -268,10 +271,10 @@ let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt") let coq_Znot_gt_le = lazy (constant "Znot_gt_le") let coq_neq = lazy (constant "neq") let coq_Zne = lazy (constant "Zne") -let coq_Zle = lazy (constant "Zle") -let coq_Zgt = lazy (constant "Zgt") -let coq_Zge = lazy (constant "Zge") -let coq_Zlt = lazy (constant "Zlt") +let coq_Zle = lazy (zbase_constant "Z.le") +let coq_Zgt = lazy (zbase_constant "Z.gt") +let coq_Zge = lazy (zbase_constant "Z.ge") +let coq_Zlt = lazy (zbase_constant "Z.lt") (* Peano/Datatypes *) let coq_le = lazy (init_constant "le") @@ -329,13 +332,13 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with EvalConstRef kn | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant") -let sp_Zsucc = lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc) -let sp_Zpred = lazy (evaluable_ref_of_constr "Zpred" coq_Zpred) -let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus) -let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle) -let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt) -let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge) -let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt) +let sp_Zsucc = lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc) +let sp_Zpred = lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred) +let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus) +let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle) +let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt) +let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge) +let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt) let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ()))) let mk_var v = mkVar (id_of_string v) -- cgit v1.2.3