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
145
146
147
148
149
150
151
152
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.
|
