blob: f9aa3e50ec19b285e7c4788d82264dedb997f31c (
plain)
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
|
(************************************************************************)
(* 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: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Export Ring.
Require Export QArith_base.
(** * A ring tactic 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.
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.
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.
Add Ring Qring : Qsrt (decidable Qeq_bool_correct, constants [Qcst]).
(** 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#1.
intro.
ring.
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.
|
