From 5b8e645b675b6b2efac8e13c29da5e984248e507 Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 27 Oct 2006 21:21:17 +0000 Subject: simplif de la partie ML de ring/field git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9302 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Arith/Arith.v | 12 +----------- theories/Arith/Arith_base.v | 20 ++++++++++++++++++++ theories/Arith/Compare.v | 2 +- theories/Reals/LegacyRfield.v | 35 +++++++++++++++++++++++++++++++++++ theories/Reals/RIneq.v | 30 ------------------------------ theories/Reals/Rfunctions.v | 7 +++---- theories/ZArith/Zabs.v | 4 ++-- theories/ZArith/Zmax.v | 2 +- theories/ZArith/Zmin.v | 2 +- theories/ZArith/Znat.v | 2 +- theories/ZArith/Zorder.v | 2 +- theories/ZArith/auxiliary.v | 2 +- 12 files changed, 67 insertions(+), 53 deletions(-) create mode 100644 theories/Arith/Arith_base.v create mode 100644 theories/Reals/LegacyRfield.v (limited to 'theories') 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 *) +(* 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. -- cgit v1.2.3