diff options
Diffstat (limited to 'contrib7/ring/Setoid_ring_theory.v')
| -rw-r--r-- | contrib7/ring/Setoid_ring_theory.v | 429 |
1 files changed, 429 insertions, 0 deletions
diff --git a/contrib7/ring/Setoid_ring_theory.v b/contrib7/ring/Setoid_ring_theory.v new file mode 100644 index 00000000..13afc5ee --- /dev/null +++ b/contrib7/ring/Setoid_ring_theory.v @@ -0,0 +1,429 @@ +(************************************************************************) +(* 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. |