diff options
Diffstat (limited to 'contrib7/ring/Setoid_ring_theory.v')
| -rw-r--r-- | contrib7/ring/Setoid_ring_theory.v | 429 |
1 files changed, 0 insertions, 429 deletions
diff --git a/contrib7/ring/Setoid_ring_theory.v b/contrib7/ring/Setoid_ring_theory.v deleted file mode 100644 index 13afc5ee..00000000 --- a/contrib7/ring/Setoid_ring_theory.v +++ /dev/null @@ -1,429 +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: Setoid_ring_theory.v,v 1.1.2.1 2004/07/16 19:30:19 herbelin Exp $ *) - -Require Export Bool. -Require Export Setoid. - -Set Implicit Arguments. - -Section Setoid_rings. - -Variable A : Type. -Variable Aequiv : A -> A -> Prop. - -Infix Local "==" Aequiv (at level 5, no associativity). - -Variable S : (Setoid_Theory A Aequiv). - -Add Setoid A Aequiv S. - -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. - -Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2. -Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2. -Variable opp_morph : (a,a0:A) a == a0 -> -a == -a0. - -Add Morphism Aplus : Aplus_ext. -Exact plus_morph. -Save. - -Add Morphism Amult : Amult_ext. -Exact mult_morph. -Save. - -Add Morphism Aopp : Aopp_ext. -Exact opp_morph. -Save. - -Section Theory_of_semi_setoid_rings. - -Record Semi_Setoid_Ring_Theory : Prop := -{ SSR_plus_sym : (n,m:A) n + m == m + n; - SSR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; - SSR_mult_sym : (n,m:A) n*m == m*n; - SSR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; - SSR_plus_zero_left :(n:A) 0 + n == n; - SSR_mult_one_left : (n:A) 1*n == n; - SSR_mult_zero_left : (n:A) 0*n == 0; - SSR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; - SSR_plus_reg_left : (n,m,p:A)n + m == n + p -> m == p; - SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y -}. - -Variable T : Semi_Setoid_Ring_Theory. - -Local plus_sym := (SSR_plus_sym T). -Local plus_assoc := (SSR_plus_assoc T). -Local mult_sym := ( SSR_mult_sym T). -Local mult_assoc := (SSR_mult_assoc T). -Local plus_zero_left := (SSR_plus_zero_left T). -Local mult_one_left := (SSR_mult_one_left T). -Local mult_zero_left := (SSR_mult_zero_left T). -Local distr_left := (SSR_distr_left T). -Local plus_reg_left := (SSR_plus_reg_left T). -Local equiv_refl := (Seq_refl A Aequiv S). -Local equiv_sym := (Seq_sym A Aequiv S). -Local equiv_trans := (Seq_trans A Aequiv S). - -Hints Resolve plus_sym plus_assoc mult_sym mult_assoc - plus_zero_left mult_one_left mult_zero_left distr_left - plus_reg_left equiv_refl (*equiv_sym*). -Hints Immediate equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because - Auto does not symmetry *) -Lemma SSR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). -Auto. Save. - -Lemma SSR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Auto. Save. - -Lemma SSR_plus_zero_left2 : (n:A) n == 0 + n. -Auto. Save. - -Lemma SSR_mult_one_left2 : (n:A) n == 1*n. -Auto. Save. - -Lemma SSR_mult_zero_left2 : (n:A) 0 == 0*n. -Auto. Save. - -Lemma SSR_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Auto. Save. - -Lemma SSR_plus_permute : (n,m,p:A) n+(m+p) == m+(n+p). -Intros. -Rewrite (plus_assoc n m p). -Rewrite (plus_sym n m). -Rewrite <- (plus_assoc m n p). -Trivial. -Save. - -Lemma SSR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). -Intros. -Rewrite (mult_assoc n m p). -Rewrite (mult_sym n m). -Rewrite <- (mult_assoc m n p). -Trivial. -Save. - -Hints Resolve SSR_plus_permute SSR_mult_permute. - -Lemma SSR_distr_right : (n,m,p:A) n*(m+p) == (n*m) + (n*p). -Intros. -Rewrite (mult_sym n (Aplus m p)). -Rewrite (mult_sym n m). -Rewrite (mult_sym n p). -Auto. -Save. - -Lemma SSR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p). -Intros. -Apply equiv_sym. -Apply SSR_distr_right. -Save. - -Lemma SSR_mult_zero_right : (n:A) n*0 == 0. -Intro; Rewrite (mult_sym n Azero); Auto. -Save. - -Lemma SSR_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Rewrite (mult_sym n Azero); Auto. -Save. - -Lemma SSR_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite (plus_sym n Azero); Auto. -Save. - -Lemma SSR_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite (plus_sym n Azero); Auto. -Save. - -Lemma SSR_mult_one_right : (n:A) n*1 == n. -Intro; Rewrite (mult_sym n Aone); Auto. -Save. - -Lemma SSR_mult_one_right2 : (n:A) n == n*1. -Intro; Rewrite (mult_sym n Aone); Auto. -Save. - -Lemma SSR_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). -Intro; Apply plus_reg_left with n; Trivial. -Save. - -End Theory_of_semi_setoid_rings. - -Section Theory_of_setoid_rings. - -Record Setoid_Ring_Theory : Prop := -{ STh_plus_sym : (n,m:A) n + m == m + n; - STh_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p; - STh_mult_sym : (n,m:A) n*m == m*n; - STh_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p; - STh_plus_zero_left :(n:A) 0 + n == n; - STh_mult_one_left : (n:A) 1*n == n; - STh_opp_def : (n:A) n + (-n) == 0; - STh_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p; - STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y -}. - -Variable T : Setoid_Ring_Theory. - -Local plus_sym := (STh_plus_sym T). -Local plus_assoc := (STh_plus_assoc T). -Local mult_sym := (STh_mult_sym T). -Local mult_assoc := (STh_mult_assoc T). -Local plus_zero_left := (STh_plus_zero_left T). -Local mult_one_left := (STh_mult_one_left T). -Local opp_def := (STh_opp_def T). -Local distr_left := (STh_distr_left T). -Local equiv_refl := (Seq_refl A Aequiv S). -Local equiv_sym := (Seq_sym A Aequiv S). -Local equiv_trans := (Seq_trans A Aequiv S). - -Hints Resolve plus_sym plus_assoc mult_sym mult_assoc - plus_zero_left mult_one_left opp_def distr_left - equiv_refl equiv_sym. - -(* Lemmas whose form is x=y are also provided in form y=x because Auto does - not symmetry *) - -Lemma STh_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p). -Auto. Save. - -Lemma STh_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p). -Auto. Save. - -Lemma STh_plus_zero_left2 : (n:A) n == 0 + n. -Auto. Save. - -Lemma STh_mult_one_left2 : (n:A) n == 1*n. -Auto. Save. - -Lemma STh_distr_left2 : (n,m,p:A) n*p + m*p == (n + m)*p. -Auto. Save. - -Lemma STh_opp_def2 : (n:A) 0 == n + (-n). -Auto. Save. - -Lemma STh_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p). -Intros. -Rewrite (plus_assoc n m p). -Rewrite (plus_sym n m). -Rewrite <- (plus_assoc m n p). -Trivial. -Save. - -Lemma STh_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p). -Intros. -Rewrite (mult_assoc n m p). -Rewrite (mult_sym n m). -Rewrite <- (mult_assoc m n p). -Trivial. -Save. - -Hints Resolve STh_plus_permute STh_mult_permute. - -Lemma Saux1 : (a:A) a + a == a -> a == 0. -Intros. -Rewrite <- (plus_zero_left a). -Rewrite (plus_sym Azero a). -Setoid_replace (Aplus a Azero) with (Aplus a (Aplus a (Aopp a))); Auto. -Rewrite (plus_assoc a a (Aopp a)). -Rewrite H. -Apply opp_def. -Save. - -Lemma STh_mult_zero_left :(n:A) 0*n == 0. -Intros. -Apply Saux1. -Rewrite <- (distr_left Azero Azero n). -Rewrite (plus_zero_left Azero). -Trivial. -Save. -Hints Resolve STh_mult_zero_left. - -Lemma STh_mult_zero_left2 : (n:A) 0 == 0*n. -Auto. -Save. - -Lemma Saux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y == z. -Intros. -Rewrite <- (plus_zero_left y). -Rewrite <- H0. -Rewrite <- (plus_assoc x z y). -Rewrite (plus_sym z y). -Rewrite (plus_assoc x y z). -Rewrite H. -Auto. -Save. - -Lemma STh_opp_mult_left : (x,y:A) -(x*y) == (-x)*y. -Intros. -Apply Saux2 with (Amult x y); Auto. -Rewrite <- (distr_left x (Aopp x) y). -Rewrite (opp_def x). -Auto. -Save. -Hints Resolve STh_opp_mult_left. - -Lemma STh_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y) . -Auto. -Save. - -Lemma STh_mult_zero_right : (n:A) n*0 == 0. -Intro; Rewrite (mult_sym n Azero); Auto. -Save. - -Lemma STh_mult_zero_right2 : (n:A) 0 == n*0. -Intro; Rewrite (mult_sym n Azero); Auto. -Save. - -Lemma STh_plus_zero_right :(n:A) n + 0 == n. -Intro; Rewrite (plus_sym n Azero); Auto. -Save. - -Lemma STh_plus_zero_right2 :(n:A) n == n + 0. -Intro; Rewrite (plus_sym n Azero); Auto. -Save. - -Lemma STh_mult_one_right : (n:A) n*1 == n. -Intro; Rewrite (mult_sym n Aone); Auto. -Save. - -Lemma STh_mult_one_right2 : (n:A) n == n*1. -Intro; Rewrite (mult_sym n Aone); Auto. -Save. - -Lemma STh_opp_mult_right : (x,y:A) -(x*y) == x*(-y). -Intros. -Rewrite (mult_sym x y). -Rewrite (mult_sym x (Aopp y)). -Auto. -Save. - -Lemma STh_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y). -Intros. -Rewrite (mult_sym x y). -Rewrite (mult_sym x (Aopp y)). -Auto. -Save. - -Lemma STh_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y). -Intros. -Apply Saux2 with (Aplus x y); Auto. -Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)). -Rewrite <- (plus_assoc x y (Aopp y)). -Rewrite (opp_def y); Rewrite (STh_plus_zero_right x). -Rewrite (STh_opp_def2 x); Trivial. -Save. - -Lemma STh_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p). -Auto. -Save. - -Lemma STh_opp_opp : (n:A) -(-n) == n. -Intro. -Apply Saux2 with (Aopp n); Auto. -Rewrite (plus_sym (Aopp n) n); Auto. -Save. -Hints Resolve STh_opp_opp. - -Lemma STh_opp_opp2 : (n:A) n == -(-n). -Auto. -Save. - -Lemma STh_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y. -Intros. -Rewrite (STh_opp_mult_left2 x (Aopp y)). -Rewrite (STh_opp_mult_right2 x y). -Trivial. -Save. - -Lemma STh_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y). -Intros. -Apply equiv_sym. -Apply STh_mult_opp_opp. -Save. - -Lemma STh_opp_zero : -0 == 0. -Rewrite <- (plus_zero_left (Aopp Azero)). -Trivial. -Save. - -Lemma STh_plus_reg_left : (n,m,p:A) n+m == n+p -> m==p. -Intros. -Rewrite <- (plus_zero_left m). -Rewrite <- (plus_zero_left p). -Rewrite <- (opp_def n). -Rewrite (plus_sym n (Aopp n)). -Rewrite <- (plus_assoc (Aopp n) n m). -Rewrite <- (plus_assoc (Aopp n) n p). -Auto. -Save. - -Lemma STh_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p. -Intros. -Apply STh_plus_reg_left with n. -Rewrite (plus_sym n m); Rewrite (plus_sym n p); -Assumption. -Save. - -Lemma STh_distr_right : (n,m,p:A) n*(m+p) == (n*m)+(n*p). -Intros. -Rewrite (mult_sym n (Aplus m p)). -Rewrite (mult_sym n m). -Rewrite (mult_sym n p). -Trivial. -Save. - -Lemma STh_distr_right2 : (n,m,p:A) (n*m)+(n*p) == n*(m+p). -Intros. -Apply equiv_sym. -Apply STh_distr_right. -Save. - -End Theory_of_setoid_rings. - -Hints Resolve STh_mult_zero_left STh_plus_reg_left : core. - -Unset Implicit Arguments. - -Definition Semi_Setoid_Ring_Theory_of : - Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory. -Intros until 1; Case H. -Split; Intros; Simpl; EAuto. -Defined. - -Coercion Semi_Setoid_Ring_Theory_of : - Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory. - - - -Section product_ring. - -End product_ring. - -Section power_ring. - -End power_ring. - -End Setoid_rings. |