diff options
Diffstat (limited to 'plugins/nsatz/NsatzZ.v')
-rw-r--r-- | plugins/nsatz/NsatzZ.v | 73 |
1 files changed, 73 insertions, 0 deletions
diff --git a/plugins/nsatz/NsatzZ.v b/plugins/nsatz/NsatzZ.v new file mode 100644 index 00000000..a65efac2 --- /dev/null +++ b/plugins/nsatz/NsatzZ.v @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Reals ZArith. +Require Export NsatzR. + +Open Scope Z_scope. + +Lemma nsatzZhypR: forall x y:Z, x=y -> IZR x = IZR y. +Proof IZR_eq. (* or f_equal ... *) + +Lemma nsatzZconclR: forall x y:Z, IZR x = IZR y -> x = y. +Proof eq_IZR. + +Lemma nsatzZhypnotR: forall x y:Z, x<>y -> IZR x <> IZR y. +Proof IZR_neq. + +Lemma nsatzZconclnotR: forall x y:Z, IZR x <> IZR y -> x <> y. +Proof. +intros x y H. contradict H. f_equal. assumption. +Qed. + +Ltac nsatzZtoR1 := + repeat + (match goal with + | H:(@eq Z ?x ?y) |- _ => + generalize (@nsatzZhypR _ _ H); clear H; intro H + | |- (@eq Z ?x ?y) => apply nsatzZconclR + | H:not (@eq Z ?x ?y) |- _ => + generalize (@nsatzZhypnotR _ _ H); clear H; intro H + | |- not (@eq Z ?x ?y) => apply nsatzZconclnotR + end). + +Lemma nsatzZR1: forall x y:Z, IZR(x+y) = (IZR x + IZR y)%R. +Proof plus_IZR. + +Lemma nsatzZR2: forall x y:Z, IZR(x*y) = (IZR x * IZR y)%R. +Proof mult_IZR. + +Lemma nsatzZR3: forall x y:Z, IZR(x-y) = (IZR x - IZR y)%R. +Proof. +intros; symmetry. apply Z_R_minus. +Qed. + +Lemma nsatzZR4: forall (x:Z) p, IZR(x ^ Zpos p) = (IZR x ^ nat_of_P p)%R. +Proof. +intros. rewrite pow_IZR. +do 2 f_equal. +apply Zpos_eq_Z_of_nat_o_nat_of_P. +Qed. + +Ltac nsatzZtoR2:= + repeat + (rewrite nsatzZR1 in * || + rewrite nsatzZR2 in * || + rewrite nsatzZR3 in * || + rewrite nsatzZR4 in *). + +Ltac nsatzZ_begin := + intros; + nsatzZtoR1; + nsatzZtoR2; + simpl in *. + (*cbv beta iota zeta delta [nat_of_P Pmult_nat plus mult] in *.*) + +Ltac nsatzZ := + nsatzZ_begin; (*idtac "nsatzZ_begin;";*) + nsatzR. |