From ca6b6bfde9a0c5b91a53e9c139140403369ff658 Mon Sep 17 00:00:00 2001 From: pottier Date: Thu, 4 Aug 2011 15:22:08 +0000 Subject: moins de reification inutile, noatations standards git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14385 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/setoid_ring/Rings_Q.v | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 plugins/setoid_ring/Rings_Q.v (limited to 'plugins/setoid_ring/Rings_Q.v') diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v new file mode 100644 index 000000000..fd7654713 --- /dev/null +++ b/plugins/setoid_ring/Rings_Q.v @@ -0,0 +1,30 @@ +Require Export Cring. +Require Export Integral_domain. + +(* Rational numbers *) +Require Import QArith. + +Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). + +Instance Qri : (Ring (Ro:=Qops)). +constructor. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. +apply Qopp_comp. + exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. + exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. +reflexivity. exact Qplus_opp_r. +Defined. + +Instance Qcri: (Cring (Rr:=Qri)). +red. exact Qmult_comm. Defined. + +Lemma Q_one_zero: not (Qeq 1%Q 0%Q). +unfold Qeq. simpl. auto with *. Qed. + +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. +exact Qmult_integral. exact Q_one_zero. Defined. -- cgit v1.2.3