aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Arith/Arith.v12
-rw-r--r--theories/Arith/Arith_base.v20
-rw-r--r--theories/Arith/Compare.v2
-rw-r--r--theories/Reals/LegacyRfield.v35
-rw-r--r--theories/Reals/RIneq.v30
-rw-r--r--theories/Reals/Rfunctions.v7
-rw-r--r--theories/ZArith/Zabs.v4
-rw-r--r--theories/ZArith/Zmax.v2
-rw-r--r--theories/ZArith/Zmin.v2
-rw-r--r--theories/ZArith/Znat.v2
-rw-r--r--theories/ZArith/Zorder.v2
-rw-r--r--theories/ZArith/auxiliary.v2
12 files changed, 67 insertions, 53 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index c522e01b3e..18dbd27f96 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -8,15 +8,5 @@
(*i $Id$ i*)
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-Require Export Between.
-Require Export Peano_dec.
-Require Export Compare_dec.
-Require Export Factorial.
-
+Require Export Arith_base.
Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
new file mode 100644
index 0000000000..b076de2aff
--- /dev/null
+++ b/theories/Arith/Arith_base.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Peano_dec.
+Require Export Compare_dec.
+Require Export Factorial.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 77fa805390..6f8a5f127a 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -16,7 +16,7 @@ Notation not_eq_sym := sym_not_eq.
Implicit Types m n p q : nat.
-Require Import Arith.
+Require Import Arith_base.
Require Import Peano_dec.
Require Import Compare_dec.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
new file mode 100644
index 0000000000..d285fef30e
--- /dev/null
+++ b/theories/Reals/LegacyRfield.v
@@ -0,0 +1,35 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Raxioms.
+Require Export LegacyField.
+Import LegacyRing_theory.
+Open Scope R_scope.
+
+Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
+ split.
+ exact Rplus_comm.
+ symmetry in |- *; apply Rplus_assoc.
+ exact Rmult_comm.
+ symmetry in |- *; apply Rmult_assoc.
+ intro; apply Rplus_0_l.
+ intro; apply Rmult_1_l.
+ exact Rplus_opp_r.
+ intros.
+ rewrite Rmult_comm.
+ rewrite (Rmult_comm n p).
+ rewrite (Rmult_comm m p).
+ apply Rmult_plus_distr_l.
+ intros; contradiction.
+Defined.
+
+Add Legacy Field
+R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
+ with minus := Rminus div := Rdiv.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 1996eaa97d..daebd91789 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -16,42 +16,12 @@ Require Export Raxioms.
Require Export ZArithRing.
Require Import Omega.
Require Export RealField.
-Require Export LegacyField.
Open Local Scope Z_scope.
Open Local Scope R_scope.
Implicit Type r : R.
-(***************************************************************************)
-(** * Instantiating Field tactic on reals *)
-(***************************************************************************)
-
-(* Legacy Field *)
-Require Export LegacyField.
-Import LegacyRing_theory.
-
-Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
- split.
- exact Rplus_comm.
- symmetry in |- *; apply Rplus_assoc.
- exact Rmult_comm.
- symmetry in |- *; apply Rmult_assoc.
- intro; apply Rplus_0_l.
- intro; apply Rmult_1_l.
- exact Rplus_opp_r.
- intros.
- rewrite Rmult_comm.
- rewrite (Rmult_comm n p).
- rewrite (Rmult_comm m p).
- apply Rmult_plus_distr_l.
- intros; contradiction.
-Defined.
-
-Add Legacy Field
-R Rplus Rmult 1 0 Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
- with minus := Rminus div := Rdiv.
-
(**************************************************************************)
(** * Relation between orders and equality *)
(**************************************************************************)
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index db995f3b0c..f048faf53a 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -397,15 +397,14 @@ Lemma pow_1_even : forall n:nat, (-1) ^ (2 * n) = 1.
Proof.
intro; induction n as [| n Hrecn].
reflexivity.
- replace (2 * S n)%nat with (2 + 2 * n)%nat.
+ replace (2 * S n)%nat with (2 + 2 * n)%nat by ring.
rewrite pow_add; rewrite Hrecn; simpl in |- *; ring.
- replace (S n) with (n + 1)%nat; [ ring | ring ].
Qed.
(**********)
Lemma pow_1_odd : forall n:nat, (-1) ^ S (2 * n) = -1.
Proof.
- intro; replace (S (2 * n)) with (2 * n + 1)%nat; [ idtac | ring ].
+ intro; replace (S (2 * n)) with (2 * n + 1)%nat by ring.
rewrite pow_add; rewrite pow_1_even; simpl in |- *; ring.
Qed.
@@ -425,7 +424,7 @@ Proof.
intros; induction n2 as [| n2 Hrecn2].
simpl in |- *; replace (n1 * 0)%nat with 0%nat; [ reflexivity | ring ].
replace (n1 * S n2)%nat with (n1 * n2 + n1)%nat.
- replace (S n2) with (n2 + 1)%nat; [ idtac | ring ].
+ replace (S n2) with (n2 + 1)%nat by ring.
do 2 rewrite pow_add.
rewrite Hrecn2.
simpl in |- *.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index f648867aad..c7f0bb7232 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -9,7 +9,7 @@
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
-Require Import Arith.
+Require Import Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zorder.
@@ -127,4 +127,4 @@ Proof.
compute in |- *. intro H0. discriminate H0. intuition.
intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index ca647ff3cc..b2c0685640 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -7,7 +7,7 @@
(************************************************************************)
(*i $Id$ i*)
-Require Import Arith.
+Require Import Arith_base.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index a1e46fa5ff..0e0caa1bd6 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -12,7 +12,7 @@
from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
*)
-Require Import Arith.
+Require Import Arith_base.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 8a18798c24..27f31bf83b 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -10,7 +10,7 @@
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
-Require Export Arith.
+Require Export Arith_base.
Require Import BinPos.
Require Import BinInt.
Require Import Zcompare.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index e267545052..4b0d2562e7 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -11,7 +11,7 @@
Require Import BinPos.
Require Import BinInt.
-Require Import Arith.
+Require Import Arith_base.
Require Import Decidable.
Require Import Zcompare.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index c6b3981105..18b49f4bbd 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -10,7 +10,7 @@
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
-Require Export Arith.
+Require Export Arith_base.
Require Import BinInt.
Require Import Zorder.
Require Import Decidable.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-17 05:17:22 +0000