blob: ae58bee3164e4c82d6a1eee9cff6fe1a9c986d56 (
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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(*i $Id$ i*)
Require Rbase.
Recursive Tactic Definition Isrealint trm:=
Match trm With
| [``0``] -> Idtac
| [``1``] -> Idtac
| [``?1+?2``] -> (Isrealint ?1);(Isrealint ?2)
| [``?1-?2``] -> (Isrealint ?1);(Isrealint ?2)
| [``?1*?2``] -> (Isrealint ?1);(Isrealint ?2)
| [``-?1``] -> (Isrealint ?1)
| _ -> Fail.
Recursive Tactic Definition Sup0 :=
Match Context With
| [ |- ``1>0`` ] -> Unfold Rgt;Apply Rlt_R0_R1
| [ |- ``1+?1>0`` ] ->
Apply (Rgt_trans ``1+?1`` ?1 ``0``);
[Pattern 1 ``1+?1``;Rewrite Rplus_sym;Unfold Rgt;
Apply Rlt_r_r_plus_R1|Sup0].
Tactic Definition DiscrR :=
Try Match Context With
| [ |- ~(?1==?2) ] ->
Isrealint ?1;Isrealint ?2;
Apply Rminus_not_eq; Ring ``?1-?2``;
(Match Context With
| [ |- [``-1``] ] ->
Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq
| _ -> Idtac);Apply Rgt_not_eq;Sup0.
|
