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