diff options
Diffstat (limited to 'plugins/ring/Setoid_ring_theory.v')
| -rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 425 |
1 files changed, 0 insertions, 425 deletions
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v deleted file mode 100644 index bb88f646..00000000 --- a/plugins/ring/Setoid_ring_theory.v +++ /dev/null @@ -1,425 +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. -Require Export Setoid. - -Set Implicit Arguments. - -Section Setoid_rings. - -Variable A : Type. -Variable Aequiv : A -> A -> Prop. - -Infix Local "==" := Aequiv (at level 70, no associativity). - -Variable S : Setoid_Theory A Aequiv. - -Add Setoid A Aequiv S as Asetoid. - -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). - -Variable plus_morph : - forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2. -Variable mult_morph : - forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2. -Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0. - -Add Morphism Aplus : Aplus_ext. -intros; apply plus_morph; assumption. -Qed. - -Add Morphism Amult : Amult_ext. -intros; apply mult_morph; assumption. -Qed. - -Add Morphism Aopp : Aopp_ext. -exact opp_morph. -Qed. - -Section Theory_of_semi_setoid_rings. - -Record Semi_Setoid_Ring_Theory : Prop := - {SSR_plus_comm : forall n m:A, n + m == m + n; - SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; - SSR_mult_comm : forall n m:A, n * m == m * n; - SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - SSR_plus_zero_left : forall n:A, 0 + n == n; - SSR_mult_one_left : forall n:A, 1 * n == n; - SSR_mult_zero_left : forall n:A, 0 * n == 0; - SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p; - SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Semi_Setoid_Ring_Theory. - -Let plus_comm := SSR_plus_comm T. -Let plus_assoc := SSR_plus_assoc T. -Let mult_comm := SSR_mult_comm T. -Let mult_assoc := SSR_mult_assoc T. -Let plus_zero_left := SSR_plus_zero_left T. -Let mult_one_left := SSR_mult_one_left T. -Let mult_zero_left := SSR_mult_zero_left T. -Let distr_left := SSR_distr_left T. -Let plus_reg_left := SSR_plus_reg_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left - mult_one_left mult_zero_left distr_left plus_reg_left - equiv_refl (*equiv_sym*). -Hint 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 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. Qed. - -Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve SSR_plus_permute SSR_mult_permute. - -Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -auto. -Qed. - -Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply SSR_distr_right. -Qed. - -Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma SSR_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma SSR_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). -intro; apply plus_reg_left with n; trivial. -Qed. - -End Theory_of_semi_setoid_rings. - -Section Theory_of_setoid_rings. - -Record Setoid_Ring_Theory : Prop := - {STh_plus_comm : forall n m:A, n + m == m + n; - STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p; - STh_mult_comm : forall n m:A, n * m == m * n; - STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p; - STh_plus_zero_left : forall n:A, 0 + n == n; - STh_mult_one_left : forall n:A, 1 * n == n; - STh_opp_def : forall n:A, n + - n == 0; - STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p; - STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}. - -Variable T : Setoid_Ring_Theory. - -Let plus_comm := STh_plus_comm T. -Let plus_assoc := STh_plus_assoc T. -Let mult_comm := STh_mult_comm T. -Let mult_assoc := STh_mult_assoc T. -Let plus_zero_left := STh_plus_zero_left T. -Let mult_one_left := STh_mult_one_left T. -Let opp_def := STh_opp_def T. -Let distr_left := STh_distr_left T. -Let equiv_refl := Seq_refl A Aequiv S. -Let equiv_sym := Seq_sym A Aequiv S. -Let equiv_trans := Seq_trans A Aequiv S. - -Hint Resolve plus_comm plus_assoc mult_comm 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 : forall n m p:A, n * m * p == n * (m * p). -auto. Qed. - -Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p). -auto. Qed. - -Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n. -auto. Qed. - -Lemma STh_mult_one_left2 : forall n:A, n == 1 * n. -auto. Qed. - -Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p. -auto. Qed. - -Lemma STh_opp_def2 : forall n:A, 0 == n + - n. -auto. Qed. - -Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p). -intros. -rewrite (plus_assoc n m p). -rewrite (plus_comm n m). -rewrite <- (plus_assoc m n p). -trivial. -Qed. - -Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p). -intros. -rewrite (mult_assoc n m p). -rewrite (mult_comm n m). -rewrite <- (mult_assoc m n p). -trivial. -Qed. - -Hint Resolve STh_plus_permute STh_mult_permute. - -Lemma Saux1 : forall a:A, a + a == a -> a == 0. -intros. -rewrite <- (plus_zero_left a). -rewrite (plus_comm 0 a). -setoid_replace (a + 0) with (a + (a + - a)) by auto. -rewrite (plus_assoc a a (- a)). -rewrite H. -apply opp_def. -Qed. - -Lemma STh_mult_zero_left : forall n:A, 0 * n == 0. -intros. -apply Saux1. -rewrite <- (distr_left 0 0 n). -rewrite (plus_zero_left 0). -trivial. -Qed. -Hint Resolve STh_mult_zero_left. - -Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n. -auto. -Qed. - -Lemma Saux2 : forall 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_comm z y). -rewrite (plus_assoc x y z). -rewrite H. -auto. -Qed. - -Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y. -intros. -apply Saux2 with (x * y); auto. -rewrite <- (distr_left x (- x) y). -rewrite (opp_def x). -auto. -Qed. -Hint Resolve STh_opp_mult_left. - -Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y). -auto. -Qed. - -Lemma STh_mult_zero_right : forall n:A, n * 0 == 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0. -intro; rewrite (mult_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right : forall n:A, n + 0 == n. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_plus_zero_right2 : forall n:A, n == n + 0. -intro; rewrite (plus_comm n 0); auto. -Qed. - -Lemma STh_mult_one_right : forall n:A, n * 1 == n. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_mult_one_right2 : forall n:A, n == n * 1. -intro; rewrite (mult_comm n 1); auto. -Qed. - -Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y. -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y). -intros. -rewrite (mult_comm x y). -rewrite (mult_comm x (- y)). -auto. -Qed. - -Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y). -intros. -apply Saux2 with (x + y); auto. -rewrite (STh_plus_permute (x + y) (- x) (- y)). -rewrite <- (plus_assoc x y (- y)). -rewrite (opp_def y); rewrite (STh_plus_zero_right x). -rewrite (STh_opp_def2 x); trivial. -Qed. - -Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p). -auto. -Qed. - -Lemma STh_opp_opp : forall n:A, - - n == n. -intro. -apply Saux2 with (- n); auto. -rewrite (plus_comm (- n) n); auto. -Qed. -Hint Resolve STh_opp_opp. - -Lemma STh_opp_opp2 : forall n:A, n == - - n. -auto. -Qed. - -Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y. -intros. -rewrite (STh_opp_mult_left2 x (- y)). -rewrite (STh_opp_mult_right2 x y). -trivial. -Qed. - -Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y. -intros. -apply equiv_sym. -apply STh_mult_opp_opp. -Qed. - -Lemma STh_opp_zero : - 0 == 0. -rewrite <- (plus_zero_left (- 0)). -trivial. -Qed. - -Lemma STh_plus_reg_left : forall 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_comm n (- n)). -rewrite <- (plus_assoc (- n) n m). -rewrite <- (plus_assoc (- n) n p). -auto. -Qed. - -Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p. -intros. -apply STh_plus_reg_left with n. -rewrite (plus_comm n m); rewrite (plus_comm n p); assumption. -Qed. - -Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p. -intros. -rewrite (mult_comm n (m + p)). -rewrite (mult_comm n m). -rewrite (mult_comm n p). -trivial. -Qed. - -Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p). -intros. -apply equiv_sym. -apply STh_distr_right. -Qed. - -End Theory_of_setoid_rings. - -Hint 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. |