# Library Coq.QArith.Qfield

Require Export Field.
Require Export QArith_base.
Require Import NArithRing.

# field and ring tactics for rational numbers

Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
Lemma Qpower_theory : power_theory 1 Qmult Qeq Z_of_N Qpower.
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_eq,
completeness Qeq_eq_bool,
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 ).
Qed.
Let ex2 : forall x y : Q, x + y == y + x.
Qed.
Let ex3 : forall x y z : Q, ( x + y )+ z == x +( y + z ).
Qed.
Let ex4 : ( inject_Z 1)+( inject_Z 1) ==( inject_Z 2).
Qed.
Let ex5 : 1+1 == 2#1.
Qed.
Let ex6 : (1#1)+(1#1) == 2#1.
Qed.
Let ex7 : forall x : Q, x - x == 0.
Qed.
Let ex8 : forall x : Q, x ^1 == x.
Qed.
Let ex9 : forall x : Q, x ^0 == 1.
Qed.
Let ex10 : forall x y : Q, ~( y ==0) -> ( x / y )* y == x.
Qed.
End Examples.
Lemma Qopp_plus : forall a b, -( a + b ) == - a + - b.
Lemma Qopp_opp : forall q, - - q == q.