diff options
Diffstat (limited to 'plugins/ring/LegacyRing_theory.v')
| -rw-r--r-- | plugins/ring/LegacyRing_theory.v | 374 |
1 files changed, 0 insertions, 374 deletions
diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v deleted file mode 100644 index 8f07ad26..00000000 --- a/plugins/ring/LegacyRing_theory.v +++ /dev/null @@ -1,374 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -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 ; eauto. Qed. - -Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma SR_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n. -symmetry ; eauto. Qed. - -Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; 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 ; 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 ; eauto. Qed. - -Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p). -symmetry ; eauto. Qed. - -Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n. -symmetry ; eauto. Qed. - -Lemma Th_mult_one_left2 : forall n:A, n = 1 * n. -symmetry ; eauto. Qed. - -Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p. -symmetry ; eauto. Qed. - -Lemma Th_opp_def2 : forall n:A, 0 = n + - n. -symmetry ; 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. -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 ; 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 ; 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 ; 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 ; 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 ; 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; 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. |