aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Lists/ListTactics.v8
-rw-r--r--theories/QArith/Qring.v20
-rw-r--r--theories/Reals/Cos_rel.v21
-rw-r--r--theories/Reals/Rdefinitions.v2
-rw-r--r--theories/Reals/Rfunctions.v6
-rw-r--r--theories/Reals/Rpow_def.v7
-rw-r--r--theories/Reals/Rtrigo.v10
-rw-r--r--theories/ZArith/Zpow_def.v27
-rw-r--r--theories/ZArith/Zpower.v15
-rw-r--r--theories/ZArith/Zsqrt.v2
10 files changed, 75 insertions, 43 deletions
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 961101d65..233b40b88 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l :=
| nil => fnil
end.
+Ltac lazy_list_fold_right fcons fnil l :=
+ match l with
+ | (cons ?x ?tl) =>
+ let cont := lazy_list_fold_right fcons fnil in
+ fcons x cont tl
+ | nil => fnil
+ end.
+
Ltac list_fold_left fcons fnil l :=
match l with
| (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 265851ec7..609e82b07 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -37,15 +37,15 @@ Proof.
Qed.
Ltac isQcst t :=
- let t := eval hnf in t in
- match t with
- Qmake ?n ?d =>
- match isZcst n with
- true => isZcst d
- | _ => false
- end
- | _ => false
- end.
+ match t with
+ | inject_Z ?z => isZcst z
+ | Qmake ?n ?d =>
+ match isZcst n with
+ true => isPcst d
+ | _ => false
+ end
+ | _ => false
+ end.
Ltac Qcst t :=
match isQcst t with
@@ -74,7 +74,7 @@ Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
Qed.
Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
- ring.
+ ring.
Qed.
Let ex5 : 1+1 == 2#1.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index a3dbca23d..eff4a6c3d 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -109,9 +109,10 @@ pose
C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
end).
ring_simplify.
+unfold Rminus.
replace
(* (- old ring compat *)
- (-1 *
+ (-
sum_f_R0
(fun k:nat =>
sum_f_R0
@@ -140,7 +141,6 @@ replace
(fun l:nat =>
C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
(sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
-(*rewrite Rplus_comm.*) (* compatibility old ring... *)
apply sum_decomposition.
apply sum_eq; intros.
unfold Wn in |- *.
@@ -154,8 +154,7 @@ apply Rmult_eq_compat_l.
replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
reflexivity.
omega.
-replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
-(*replace (* compatibility old ring... *)
+replace
(-
sum_f_R0
(fun k:nat =>
@@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
(fun p:nat =>
(-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
- y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*)
-apply Rmult_eq_compat_l.
+ y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
rewrite scal_sum.
rewrite decomp_sum.
replace (sin_nnn 0%nat) with 0.
-rewrite Rmult_0_l; rewrite Rplus_0_l.
-replace (pred (S n)) with n; [ idtac | reflexivity ].
+rewrite Rplus_0_l.
+change (pred (S n)) with n.
+ (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
apply sum_eq; intros.
rewrite Rmult_comm.
unfold sin_nnn in |- *.
@@ -185,8 +184,8 @@ rewrite scal_sum.
rewrite scal_sum.
apply sum_eq; intros.
unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+(*repeat rewrite Rmult_assoc.*)
+(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
repeat rewrite <- Rmult_assoc.
rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
repeat rewrite <- Rmult_assoc.
@@ -216,7 +215,7 @@ apply INR_fact_neq_0.
apply INR_fact_neq_0.
reflexivity.
apply lt_O_Sn.
-ring.
+(* ring. *)
apply sum_eq; intros.
rewrite scal_sum.
apply sum_eq; intros.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index 7077d1015..3447aa0e4 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -55,6 +55,8 @@ Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
(**********)
Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
+(**********)
+
Infix "-" := Rminus : R_scope.
Infix "/" := Rdiv : R_scope.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index f048faf53..ba7396ed6 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -19,6 +19,7 @@ Require Export LegacyArithRing. (* for ring_nat... *)
Require Export ArithRing.
Require Import Rbase.
+Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
Require Export R_sqr.
@@ -65,11 +66,6 @@ Qed.
(** * Power *)
(*******************************)
(*********)
-Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
- match n with
- | O => 1
- | S n => r * pow r n
- end.
Infix "^" := pow : R_scope.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 000000000..5bdbb76b9
--- /dev/null
+++ b/theories/Reals/Rpow_def.v
@@ -0,0 +1,7 @@
+Require Import Rdefinitions.
+
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+ match n with
+ | O => R1
+ | S n => Rmult r (pow r n)
+ end.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index d05fd99cb..2adac468b 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 :
Proof.
intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
- rewrite <- Z_R_minus; simpl; ring_simplify;
-(* rewrite (Rmult_comm PI);*) (* old ring compat *)
+ rewrite <- Z_R_minus; simpl.
+unfold INR in H3. field_simplify [(sym_eq H3)]. field.
+(**
+ ring_simplify.
+ (* rewrite (Rmult_comm PI);*) (* old ring compat *)
rewrite <- H3; simpl;
- field; repeat split; discrR.
+ field;repeat split; discrR.
+*)
Qed.
Lemma cos_eq_0_1 :
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
new file mode 100644
index 000000000..dabd6ace1
--- /dev/null
+++ b/theories/ZArith/Zpow_def.v
@@ -0,0 +1,27 @@
+Require Import ZArith_base.
+Require Import Ring_theory.
+
+Open Scope Z_scope.
+
+(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
+ integer (type [positive]) and [z] a signed integer (type [Z]) *)
+Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
+
+Definition Zpower (x y:Z) :=
+ match y with
+ | Zpos p => Zpower_pos x p
+ | Z0 => 1
+ | Zneg p => 0
+ end.
+
+Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Proof.
+ constructor. intros.
+ destruct n;simpl;trivial.
+ unfold Zpower_pos.
+ assert (forall k, iter_pos p Z (fun x : Z => r * x) k = pow_pos Zmult r p*k).
+ induction p;simpl;intros;repeat rewrite IHp;trivial;
+ repeat rewrite Zmult_assoc;trivial.
+ rewrite H;rewrite Zmult_1_r;trivial.
+Qed.
+
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 248af0102..4e08c726e 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -9,6 +9,7 @@
(*i $Id$ i*)
Require Import ZArith_base.
+Require Export Zpow_def.
Require Import Omega.
Require Import Zcomplements.
Open Local Scope Z_scope.
@@ -35,11 +36,6 @@ Section section1.
apply Zmult_assoc ].
Qed.
- (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
- integer (type [positive]) and [z] a signed integer (type [Z]) *)
-
- Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
-
(** This theorem shows that powers of unary and binary integers
are the same thing, modulo the function convert : [positive -> nat] *)
@@ -66,13 +62,6 @@ Section section1.
apply Zpower_nat_is_exp.
Qed.
- Definition Zpower (x y:Z) :=
- match y with
- | Zpos p => Zpower_pos x p
- | Z0 => 1
- | Zneg p => 0
- end.
-
Infix "^" := Zpower : Z_scope.
Hint Immediate Zpower_nat_is_exp: zarith.
@@ -382,4 +371,4 @@ Section power_div_with_rest.
apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
Qed.
-End power_div_with_rest. \ No newline at end of file
+End power_div_with_rest.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 79fce8964..4a395e6f8 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -132,7 +132,7 @@ Definition Zsqrt :
(fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
_)
end); try omega.
-split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
+ split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ].
Defined.
(** Define a function of type Z->Z that computes the integer square root,
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 03:20:30 +0000