1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* Micromega: A reflexive tactic using the Positivstellensatz *)
11
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
13
(************************************************************************)
15
Require Import ZMicromega.
16
Require Import QMicromega.
17
Require Import RMicromega.
18
Require Import QArith.
19
Require Export Ring_normalize.
20
Require Import ZArith.
21
Require Import Raxioms.
22
Require Export RingMicromega.
23
Require Import VarMap.
27
let tac := lazymatch dom with
29
(sos_Z || psatz_Z d) ;
30
intros __wit __varmap __ff ;
31
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
32
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
34
(sos_R || psatz_R d) ;
35
intros __wit __varmap __ff ;
36
change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
37
apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
39
(sos_Q || psatz_Q d) ;
40
intros __wit __varmap __ff ;
41
change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
42
apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
43
| _ => fail "Unsupported domain"
46
Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
47
Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
50
let tac := lazymatch dom with
53
intros __wit __varmap __ff ;
54
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
55
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
58
intros __wit __varmap __ff ;
59
change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
60
apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
63
intros __wit __varmap __ff ;
64
change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
65
apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
66
| _ => fail "Unsupported domain"
73
intros __wit __varmap __ff ;
74
change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
75
apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.