1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
|
(************************************************************************)
(* 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$ i*)
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.
Proof.
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.
Qed.
Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
Proof.
constructor.
exact Qsrt.
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_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).
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.
|
