summaryrefslogtreecommitdiff
path: root/theories/QArith/Qfield.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /theories/QArith/Qfield.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'theories/QArith/Qfield.v')
-rw-r--r--theories/QArith/Qfield.v153
1 files changed, 153 insertions, 0 deletions
diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v
new file mode 100644
index 00000000..5d548aea
--- /dev/null
+++ b/theories/QArith/Qfield.v
@@ -0,0 +1,153 @@
+(************************************************************************)
+(* 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 *)
+(************************************************************************)
+
+(*i $Id: Qfield.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
+Require Export Field.
+Require Export QArith_base.
+Require Import NArithRing.
+
+(** * field and ring tactics for rational numbers *)
+
+Definition Qeq_bool (x y : Q) :=
+ if Qeq_dec x y then true else false.
+
+Lemma Qeq_bool_correct : forall x y : Q, Qeq_bool x y = true -> x==y.
+Proof.
+ intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+ intros _ H; inversion H.
+Qed.
+
+Lemma Qeq_bool_complete : forall x y : Q, x==y -> Qeq_bool x y = true.
+Proof.
+ intros x y; unfold Qeq_bool in |- *; case (Qeq_dec x y); simpl in |- *; auto.
+Qed.
+
+Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
+Proof.
+ constructor.
+ constructor.
+ exact Qplus_0_l.
+ exact Qplus_comm.
+ exact Qplus_assoc.
+ exact Qmult_1_l.
+ exact Qmult_comm.
+ exact Qmult_assoc.
+ exact Qmult_plus_distr_l.
+ reflexivity.
+ exact Qplus_opp_r.
+ discriminate.
+ reflexivity.
+ intros p Hp.
+ rewrite Qmult_comm.
+ apply Qmult_inv_r.
+ exact Hp.
+Qed.
+
+Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower.
+Proof.
+constructor.
+intros r [|n];
+reflexivity.
+Qed.
+
+Ltac isQcst t :=
+ match t with
+ | inject_Z ?z => isZcst z
+ | Qmake ?n ?d =>
+ match isZcst n with
+ true => isPcst d
+ | _ => false
+ end
+ | _ => false
+ end.
+
+Ltac Qcst t :=
+ match isQcst t with
+ true => t
+ | _ => NotConstant
+ end.
+
+Ltac Qpow_tac t :=
+ match t with
+ | Z0 => N0
+ | Zpos ?n => Ncst (Npos n)
+ | Z_of_N ?n => Ncst n
+ | NtoZ ?n => Ncst n
+ | _ => NotConstant
+ end.
+
+Add Field Qfield : Qsft
+ (decidable Qeq_bool_correct,
+ completeness Qeq_bool_complete,
+ constants [Qcst],
+ power_tac Qpower_theory [Qpow_tac]).
+
+(** Exemple of use: *)
+
+Section Examples.
+
+Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z).
+ intros.
+ ring.
+Qed.
+
+Let ex2 : forall x y : Q, x+y == y+x.
+ intros.
+ ring.
+Qed.
+
+Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
+ intros.
+ ring.
+Qed.
+
+Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
+ ring.
+Qed.
+
+Let ex5 : 1+1 == 2#1.
+ ring.
+Qed.
+
+Let ex6 : (1#1)+(1#1) == 2#1.
+ ring.
+Qed.
+
+Let ex7 : forall x : Q, x-x== 0.
+ intro.
+ ring.
+Qed.
+
+Let ex8 : forall x : Q, x^1 == x.
+ intro.
+ ring.
+Qed.
+
+Let ex9 : forall x : Q, x^0 == 1.
+ intro.
+ ring.
+Qed.
+
+Let ex10 : forall x y : Q, ~(y==0) -> (x/y)*y == x.
+intros.
+field.
+auto.
+Qed.
+
+End Examples.
+
+Lemma Qopp_plus : forall a b, -(a+b) == -a + -b.
+Proof.
+ intros; ring.
+Qed.
+
+Lemma Qopp_opp : forall q, - -q==q.
+Proof.
+ intros; ring.
+Qed.