blob: 8acf0ff882ccecfa76e641f31b88f571089ad6a4 (
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* *)
(* Micromega: A reflexive tactic using the Positivstellensatz *)
(* *)
(* Frédéric Besson (Irisa/Inria) 2006-2016 *)
(* *)
(************************************************************************)
Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
Require Import QArith.
Require Import ZArith.
Require Import Rdefinitions.
Require Import RingMicromega.
Require Import VarMap.
Require Coq.micromega.Tauto.
Require Lia.
Require Lra.
Require Lqa.
Declare ML Module "micromega_plugin".
Ltac lia := Lia.lia.
Ltac nia := Lia.nia.
Ltac xpsatz dom d :=
let tac := lazymatch dom with
| Z =>
(sos_Z Lia.zchecker) || (psatz_Z d Lia.zchecker)
| R =>
(sos_R Lra.rchecker) || (psatz_R d Lra.rchecker)
| Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.rchecker)
| _ => fail "Unsupported domain"
end in tac.
Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
Ltac psatzl dom :=
let tac := lazymatch dom with
| Z => Lia.lia
| Q => Lqa.lra
| R => Lra.lra
| _ => fail "Unsupported domain"
end in tac.
Ltac lra :=
first [ psatzl R | psatzl Q ].
Ltac nra :=
first [ Lra.nra | Lqa.nra ].
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
|
