diff options
Diffstat (limited to 'plugins/ring/LegacyRing_theory.v')
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 376 |
1 files changed, 376 insertions, 0 deletions
diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v new file mode 100644 index 00000000..30d29515 --- /dev/null +++ b/plugins/ring/LegacyRing_theory.v @@ -0,0 +1,376 @@ +(************************************************************************) +(* 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$ *) + +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 "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 40, left associativity). +Notation "0" := Azero. +Notation "1" := Aone. + +Record Semi_Ring_Theory : Prop := + {SR_plus_comm : forall n m:A, n + m = m + n; + SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + SR_mult_comm : forall n m:A, n * m = m * n; + SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + SR_plus_zero_left : forall n:A, 0 + n = n; + SR_mult_one_left : forall n:A, 1 * n = n; + SR_mult_zero_left : forall n:A, 0 * n = 0; + SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; +(* SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*) + SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. + +Variable T : Semi_Ring_Theory. + +Let plus_comm := SR_plus_comm T. +Let plus_assoc := SR_plus_assoc T. +Let mult_comm := SR_mult_comm T. +Let mult_assoc := SR_mult_assoc T. +Let plus_zero_left := SR_plus_zero_left T. +Let mult_one_left := SR_mult_one_left T. +Let mult_zero_left := SR_mult_zero_left T. +Let distr_left := SR_distr_left T. +(*Let plus_reg_left := SR_plus_reg_left T.*) + +Hint Resolve plus_comm plus_assoc mult_comm 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 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. + +Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm m n). +rewrite <- plus_assoc. +reflexivity. +Qed. + +Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm m n). +rewrite <- mult_assoc. +reflexivity. +Qed. + +Hint Resolve SR_plus_permute SR_mult_permute. + +Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. +intros. +repeat rewrite (mult_comm n). +eauto. +Qed. + +Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply SR_distr_right. Qed. + +Lemma SR_mult_zero_right : forall n:A, n * 0 = 0. +intro; rewrite mult_comm; eauto. +Qed. + +Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; rewrite mult_comm; eauto. +Qed. + +Lemma SR_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. +Qed. +Lemma SR_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma SR_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; auto. +Qed. + +Lemma SR_mult_one_right2 : forall n:A, n = n * 1. +intro; elim mult_comm; auto. +Qed. +(* +Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. +intros n m p; rewrite (plus_comm m n); rewrite (plus_comm 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 "+" := Aplus (at level 50, left associativity). +Infix "*" := Amult (at level 40, left associativity). +Notation "0" := Azero. +Notation "1" := Aone. +Notation "- x" := (Aopp x). + +Record Ring_Theory : Prop := + {Th_plus_comm : forall n m:A, n + m = m + n; + Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p; + Th_mult_comm : forall n m:A, n * m = m * n; + Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p; + Th_plus_zero_left : forall n:A, 0 + n = n; + Th_mult_one_left : forall n:A, 1 * n = n; + Th_opp_def : forall n:A, n + - n = 0; + Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p; + Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}. + +Variable T : Ring_Theory. + +Let plus_comm := Th_plus_comm T. +Let plus_assoc := Th_plus_assoc T. +Let mult_comm := Th_mult_comm T. +Let mult_assoc := Th_mult_assoc T. +Let plus_zero_left := Th_plus_zero_left T. +Let mult_one_left := Th_mult_one_left T. +Let opp_def := Th_opp_def T. +Let distr_left := Th_distr_left T. + +Hint Resolve plus_comm plus_assoc mult_comm 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 : forall n m p:A, n * m * p = n * (m * p). +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. +symmetry in |- *; eauto. Qed. + +Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. +symmetry in |- *; eauto. Qed. + +Lemma Th_opp_def2 : forall n:A, 0 = n + - n. +symmetry in |- *; eauto. Qed. + +Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p). +intros. +rewrite plus_assoc. +elim (plus_comm m n). +rewrite <- plus_assoc. +reflexivity. +Qed. + +Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p). +intros. +rewrite mult_assoc. +elim (mult_comm m n). +rewrite <- mult_assoc. +reflexivity. +Qed. + +Hint Resolve Th_plus_permute Th_mult_permute. + +Lemma aux1 : forall a:A, a + a = a -> a = 0. +intros. +generalize (opp_def a). +pattern a at 1 in |- *. +rewrite <- H. +rewrite <- plus_assoc. +rewrite opp_def. +elim plus_comm. +rewrite plus_zero_left. +trivial. +Qed. + +Lemma Th_mult_zero_left : forall n:A, 0 * n = 0. +intros. +apply aux1. +rewrite <- distr_left. +rewrite plus_zero_left. +reflexivity. +Qed. +Hint Resolve Th_mult_zero_left. + +Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n. +symmetry in |- *; eauto. Qed. + +Lemma aux2 : forall 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_comm y z). +rewrite plus_assoc. +rewrite H. +rewrite plus_zero_left. +reflexivity. +Qed. + +Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y. +intros. +apply (aux2 (x:=(x * y))); + [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ]. +Qed. +Hint Resolve Th_opp_mult_left. + +Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y). +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_zero_right : forall n:A, n * 0 = 0. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_plus_zero_right : forall n:A, n + 0 = n. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma Th_plus_zero_right2 : forall n:A, n = n + 0. +intro; rewrite plus_comm; eauto. +Qed. + +Lemma Th_mult_one_right : forall n:A, n * 1 = n. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_mult_one_right2 : forall n:A, n = n * 1. +intro; elim mult_comm; eauto. +Qed. + +Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y. +intros; do 2 rewrite (mult_comm x); auto. +Qed. + +Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y). +intros; do 2 rewrite (mult_comm x); auto. +Qed. + +Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y). +intros. +apply (aux2 (x:=(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 : forall n m p:A, - m + (n + p) = n + (- m + p). +eauto. Qed. + +Lemma Th_opp_opp : forall n:A, - - n = n. +intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ]. +Qed. +Hint Resolve Th_opp_opp. + +Lemma Th_opp_opp2 : forall n:A, n = - - n. +symmetry in |- *; eauto. Qed. + +Lemma Th_mult_opp_opp : forall 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 : forall x y:A, x * y = - x * - y. +symmetry in |- *; apply Th_mult_opp_opp. Qed. + +Lemma Th_opp_zero : - 0 = 0. +rewrite <- (plus_zero_left (- 0)). +auto. Qed. +(* +Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p. +intros; generalize (f_equal (fun z => - n + z) H). +repeat rewrite plus_assoc. +rewrite (plus_comm (- n) n). +rewrite opp_def. +repeat rewrite Th_plus_zero_left; eauto. +Qed. + +Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p. +intros. +eapply Th_plus_reg_left with n. +rewrite (plus_comm n m). +rewrite (plus_comm n p). +auto. +Qed. +*) +Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p. +intros. +repeat rewrite (mult_comm n). +eauto. +Qed. + +Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p). +symmetry in |- *; apply Th_distr_right. +Qed. + +End Theory_of_rings. + +Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core. + +Unset Implicit Arguments. + +Definition Semi_Ring_Theory_of : + forall (A:Type) (Aplus Amult:A -> A -> A) (Aone 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 in |- *; 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. |