blob: c81c025a551f7200509ed4347242e2f497354455 (
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
|
(************************************************************************)
(* 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 || psatz_Z d) ; Lia.zchecker
| R =>
(sos_R || psatz_R d) ;
(* If csdp is not installed, the previous step might not produce any
progress: the rest of the tactical will then fail. Hence the 'try'. *)
try Lra.rchecker
| Q => (sos_Q || psatz_Q d) ;
(* If csdp is not installed, the previous step might not produce any
progress: the rest of the tactical will then fail. Hence the 'try'. *)
try 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: *)
|
