diff options
Diffstat (limited to 'contrib7/ring/Ring_theory.v')
-rw-r--r-- | contrib7/ring/Ring_theory.v | 384 |
1 files changed, 0 insertions, 384 deletions
diff --git a/contrib7/ring/Ring_theory.v b/contrib7/ring/Ring_theory.v deleted file mode 100644 index 85fb7f6c..00000000 --- a/contrib7/ring/Ring_theory.v +++ /dev/null @@ -1,384 +0,0 @@ -(************************************************************************) -(* 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 *) -(************************************************************************) - -(* $Id: Ring_theory.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) - -Require Export Bool. - -Set Implicit Arguments. - -Section Theory_of_semi_rings. - -Variable A : Type. -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -(* There is also a "weakly decidable" equality on A. That means - that if (A_eq x y)=true then x=y but x=y can arise when - (A_eq x y)=false. On an abstract ring the function [x,y:A]false - is a good choice. The proof of A_eq_prop is in this case easy. *) -Variable Aeq : A -> A -> bool. - -Infix 4 "+" Aplus V8only 50 (left associativity). -Infix 4 "*" Amult V8only 40 (left associativity). -Notation "0" := Azero. -Notation "1" := Aone. - -Record Semi_Ring_Theory : Prop := -{ SR_plus_sym : (n,m:A) n + m == m + n; - SR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; - SR_mult_sym : (n,m:A) n*m == m*n; - SR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; - SR_plus_zero_left :(n:A) 0 + n == n; - SR_mult_one_left : (n:A) 1*n == n; - SR_mult_zero_left : (n:A) 0*n == 0; - SR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; - SR_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p; - SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y -}. - -Variable T : Semi_Ring_Theory. - -Local plus_sym := (SR_plus_sym T). -Local plus_assoc := (SR_plus_assoc T). -Local mult_sym := ( SR_mult_sym T). -Local mult_assoc := (SR_mult_assoc T). -Local plus_zero_left := (SR_plus_zero_left T). -Local mult_one_left := (SR_mult_one_left T). -Local mult_zero_left := (SR_mult_zero_left T). -Local distr_left := (SR_distr_left T). -Local plus_reg_left := (SR_plus_reg_left T). - -Hints Resolve plus_sym plus_assoc mult_sym mult_assoc - plus_zero_left mult_one_left mult_zero_left distr_left - plus_reg_left. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) -Lemma SR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). -Symmetry; EAuto. Qed. - -Lemma SR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Symmetry; EAuto. Qed. - -Lemma SR_plus_zero_left2 : (n:A) n == 0 + n. -Symmetry; EAuto. Qed. - -Lemma SR_mult_one_left2 : (n:A) n == 1*n. -Symmetry; EAuto. Qed. - -Lemma SR_mult_zero_left2 : (n:A) 0 == 0*n. -Symmetry; EAuto. Qed. - -Lemma SR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Symmetry; EAuto. Qed. - -Lemma SR_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). -Intros. -Rewrite -> plus_assoc. -Elim (plus_sym m n). -Rewrite <- plus_assoc. -Reflexivity. -Qed. - -Lemma SR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). -Intros. -Rewrite -> mult_assoc. -Elim (mult_sym m n). -Rewrite <- mult_assoc. -Reflexivity. -Qed. - -Hints Resolve SR_plus_permute SR_mult_permute. - -Lemma SR_distr_right : (n,m,p:A) n*(m + p) == (n*m) + (n*p). -Intros. -Repeat Rewrite -> (mult_sym n). -EAuto. -Qed. - -Lemma SR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). -Symmetry; Apply SR_distr_right. Qed. - -Lemma SR_mult_zero_right : (n:A) n*0 == 0. -Intro; Rewrite mult_sym; EAuto. -Qed. - -Lemma SR_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Rewrite mult_sym; EAuto. -Qed. - -Lemma SR_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite plus_sym; EAuto. -Qed. -Lemma SR_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite plus_sym; EAuto. -Qed. - -Lemma SR_mult_one_right : (n:A) n*1 == n. -Intro; Elim mult_sym; Auto. -Qed. - -Lemma SR_mult_one_right2 : (n:A) n == n*1. -Intro; Elim mult_sym; Auto. -Qed. - -Lemma SR_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p. -Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n); EAuto. -Qed. - -End Theory_of_semi_rings. - -Section Theory_of_rings. - -Variable A : Type. - -Variable Aplus : A -> A -> A. -Variable Amult : A -> A -> A. -Variable Aone : A. -Variable Azero : A. -Variable Aopp : A -> A. -Variable Aeq : A -> A -> bool. - -Infix 4 "+" Aplus V8only 50 (left associativity). -Infix 4 "*" Amult V8only 40 (left associativity). -Notation "0" := Azero. -Notation "1" := Aone. -Notation "- x" := (Aopp x) (at level 0) V8only. - -Record Ring_Theory : Prop := -{ Th_plus_sym : (n,m:A) n + m == m + n; - Th_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; - Th_mult_sym : (n,m:A) n*m == m*n; - Th_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; - Th_plus_zero_left :(n:A) 0 + n == n; - Th_mult_one_left : (n:A) 1*n == n; - Th_opp_def : (n:A) n + (-n) == 0; - Th_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; - Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y -}. - -Variable T : Ring_Theory. - -Local plus_sym := (Th_plus_sym T). -Local plus_assoc := (Th_plus_assoc T). -Local mult_sym := ( Th_mult_sym T). -Local mult_assoc := (Th_mult_assoc T). -Local plus_zero_left := (Th_plus_zero_left T). -Local mult_one_left := (Th_mult_one_left T). -Local opp_def := (Th_opp_def T). -Local distr_left := (Th_distr_left T). - -Hints Resolve plus_sym plus_assoc mult_sym mult_assoc - plus_zero_left mult_one_left opp_def distr_left. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) -Lemma Th_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). -Symmetry; EAuto. Qed. - -Lemma Th_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Symmetry; EAuto. Qed. - -Lemma Th_plus_zero_left2 : (n:A) n == 0 + n. -Symmetry; EAuto. Qed. - -Lemma Th_mult_one_left2 : (n:A) n == 1*n. -Symmetry; EAuto. Qed. - -Lemma Th_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Symmetry; EAuto. Qed. - -Lemma Th_opp_def2 : (n:A) 0 == n + (-n). -Symmetry; EAuto. Qed. - -Lemma Th_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). -Intros. -Rewrite -> plus_assoc. -Elim (plus_sym m n). -Rewrite <- plus_assoc. -Reflexivity. -Qed. - -Lemma Th_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). -Intros. -Rewrite -> mult_assoc. -Elim (mult_sym m n). -Rewrite <- mult_assoc. -Reflexivity. -Qed. - -Hints Resolve Th_plus_permute Th_mult_permute. - -Lemma aux1 : (a:A) a + a == a -> a == 0. -Intros. -Generalize (opp_def a). -Pattern 1 a. -Rewrite <- H. -Rewrite <- plus_assoc. -Rewrite -> opp_def. -Elim plus_sym. -Rewrite plus_zero_left. -Trivial. -Qed. - -Lemma Th_mult_zero_left :(n:A) 0*n == 0. -Intros. -Apply aux1. -Rewrite <- distr_left. -Rewrite plus_zero_left. -Reflexivity. -Qed. -Hints Resolve Th_mult_zero_left. - -Lemma Th_mult_zero_left2 : (n:A) 0 == 0*n. -Symmetry; EAuto. Qed. - -Lemma aux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y==z. -Intros. -Rewrite <- (plus_zero_left y). -Elim H0. -Elim plus_assoc. -Elim (plus_sym y z). -Rewrite -> plus_assoc. -Rewrite -> H. -Rewrite plus_zero_left. -Reflexivity. -Qed. - -Lemma Th_opp_mult_left : (x,y:A) -(x*y) == (-x)*y. -Intros. -Apply (aux2 1!x*y); -[ Apply opp_def -| Rewrite <- distr_left; - Rewrite -> opp_def; - Auto]. -Qed. -Hints Resolve Th_opp_mult_left. - -Lemma Th_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y). -Symmetry; EAuto. Qed. - -Lemma Th_mult_zero_right : (n:A) n*0 == 0. -Intro; Elim mult_sym; EAuto. -Qed. - -Lemma Th_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Elim mult_sym; EAuto. -Qed. - -Lemma Th_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite plus_sym; EAuto. -Qed. - -Lemma Th_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite plus_sym; EAuto. -Qed. - -Lemma Th_mult_one_right : (n:A) n*1 == n. -Intro;Elim mult_sym; EAuto. -Qed. - -Lemma Th_mult_one_right2 : (n:A) n == n*1. -Intro;Elim mult_sym; EAuto. -Qed. - -Lemma Th_opp_mult_right : (x,y:A) -(x*y) == x*(-y). -Intros; Do 2 Rewrite -> (mult_sym x); Auto. -Qed. - -Lemma Th_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). -Intros; Do 2 Rewrite -> (mult_sym x); Auto. -Qed. - -Lemma Th_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). -Intros. -Apply (aux2 1! x + y); -[ Elim plus_assoc; - Rewrite -> (Th_plus_permute y (-x)); Rewrite -> plus_assoc; - Rewrite -> opp_def; Rewrite plus_zero_left; Auto -| Auto ]. -Qed. - -Lemma Th_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p). -EAuto. Qed. - -Lemma Th_opp_opp : (n:A) -(-n) == n. -Intro; Apply (aux2 1! -n); - [ Auto | Elim plus_sym; Auto ]. -Qed. -Hints Resolve Th_opp_opp. - -Lemma Th_opp_opp2 : (n:A) n == -(-n). -Symmetry; EAuto. Qed. - -Lemma Th_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y. -Intros; Rewrite <- Th_opp_mult_left; Rewrite <- Th_opp_mult_right; Auto. -Qed. - -Lemma Th_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). -Symmetry; Apply Th_mult_opp_opp. Qed. - -Lemma Th_opp_zero : -0 == 0. -Rewrite <- (plus_zero_left (-0)). -Auto. Qed. - -Lemma Th_plus_reg_left : (n,m,p:A) n + m == n + p -> m==p. -Intros; Generalize (congr_eqT ? ? [z] (-n)+z ? ? H). -Repeat Rewrite plus_assoc. -Rewrite (plus_sym (-n) n). -Rewrite opp_def. -Repeat Rewrite Th_plus_zero_left; EAuto. -Qed. - -Lemma Th_plus_reg_right : (n,m,p:A) m + n == p + n -> m==p. -Intros. -EApply Th_plus_reg_left with n. -Rewrite (plus_sym n m). -Rewrite (plus_sym n p). -Auto. -Qed. - -Lemma Th_distr_right : (n,m,p:A) n*(m + p) == (n*m) + (n*p). -Intros. -Repeat Rewrite -> (mult_sym n). -EAuto. -Qed. - -Lemma Th_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). -Symmetry; Apply Th_distr_right. -Qed. - -End Theory_of_rings. - -Hints Resolve Th_mult_zero_left Th_plus_reg_left : core. - -Unset Implicit Arguments. - -Definition Semi_Ring_Theory_of : - (A:Type)(Aplus : A -> A -> A)(Amult : A -> A -> A)(Aone : A) - (Azero : A)(Aopp : A -> A)(Aeq : A -> A -> bool) - (Ring_Theory Aplus Amult Aone Azero Aopp Aeq) - ->(Semi_Ring_Theory Aplus Amult Aone Azero Aeq). -Intros until 1; Case H. -Split; Intros; Simpl; EAuto. -Defined. - -(* Every ring can be viewed as a semi-ring : this property will be used - in Abstract_polynom. *) -Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory. - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. |