diff options
Diffstat (limited to 'plugins/setoid_ring/Integral_domain.v')
-rw-r--r-- | plugins/setoid_ring/Integral_domain.v | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Integral_domain.v b/plugins/setoid_ring/Integral_domain.v new file mode 100644 index 00000000..5a224e38 --- /dev/null +++ b/plugins/setoid_ring/Integral_domain.v @@ -0,0 +1,44 @@ +Require Export Cring. + + +(* Definition of integral domains: commutative ring without zero divisor *) + +Class Integral_domain {R : Type}`{Rcr:Cring R} := { + integral_domain_product: + forall x y, x * y == 0 -> x == 0 \/ y == 0; + integral_domain_one_zero: not (1 == 0)}. + +Section integral_domain. + +Context {R:Type}`{Rid:Integral_domain R}. + +Lemma integral_domain_minus_one_zero: ~ - (1:R) == 0. +red;intro. apply integral_domain_one_zero. +assert (0 == - (0:R)). cring. +rewrite H0. rewrite <- H. cring. +Qed. + + +Definition pow (r : R) (n : nat) := Ring_theory.pow_N 1 mul r (N_of_nat n). + +Lemma pow_not_zero: forall p n, pow p n == 0 -> p == 0. +induction n. unfold pow; simpl. intros. absurd (1 == 0). +simpl. apply integral_domain_one_zero. + trivial. setoid_replace (pow p (S n)) with (p * (pow p n)). +intros. +case (integral_domain_product p (pow p n) H). trivial. trivial. +unfold pow; simpl. +clear IHn. induction n; simpl; try cring. + rewrite Ring_theory.pow_pos_Psucc. cring. apply ring_setoid. +apply ring_mult_comp. +apply cring_mul_comm. +apply ring_mul_assoc. +Qed. + +Lemma Rintegral_domain_pow: + forall c p r, ~c == 0 -> c * (pow p r) == ring0 -> p == ring0. +intros. case (integral_domain_product c (pow p r) H0). intros; absurd (c == ring0); auto. +intros. apply pow_not_zero with r. trivial. Qed. + +End integral_domain. + |