diff options
Diffstat (limited to 'contrib/setoid_ring/ZArithRing.v')
-rw-r--r-- | contrib/setoid_ring/ZArithRing.v | 47 |
1 files changed, 35 insertions, 12 deletions
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v index 4f47fff0..8de7021e 100644 --- a/contrib/setoid_ring/ZArithRing.v +++ b/contrib/setoid_ring/ZArithRing.v @@ -8,26 +8,49 @@ Require Export Ring. Require Import ZArith_base. +Require Import Zpow_def. + Import InitialRing. Set Implicit Arguments. -Ltac isZcst t := - let t := eval hnf in t in - match t with - Z0 => constr:true - | Zpos ?p => isZcst p - | Zneg ?p => isZcst p - | xI ?p => isZcst p - | xO ?p => isZcst p - | xH => constr:true - | _ => constr:false - end. Ltac Zcst t := match isZcst t with true => t | _ => NotConstant end. +Ltac isZpow_coef t := + match t with + | Zpos ?p => isPcst p + | Z0 => true + | _ => false + end. + +Definition N_of_Z x := + match x with + | Zpos p => Npos p + | _ => N0 + end. + +Ltac Zpow_tac t := + match isZpow_coef t with + | true => constr:(N_of_Z t) + | _ => constr:(NotConstant) + end. + +Ltac Zpower_neg := + repeat match goal with + | [|- ?G] => + match G with + | context c [Zpower _ (Zneg _)] => + let t := context c [Z0] in + change t + end + end. + + Add Ring Zr : Zth - (decidable Zeqb_ok, constants [Zcst], preprocess [unfold Zsucc]). + (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc], + power_tac Zpower_theory [Zpow_tac]). + |