Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Tej Chajed
stdpp
Commits
90ce6473
Commit
90ce6473
authored
Aug 22, 2016
by
Ralf Jung
Browse files
use Psatz without using axioms about real numbers
parent
b8b41bc5
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/psatz_axiomfree.v
0 → 100644
View file @
90ce6473
(** This file is a hack that lets us use Psatz without importing all sorts of
axioms about real numbers. It has been created by copying the file
Psatz.v from the Coq distribution, removing everything defined after the lia
tactic, and removing the two lines importing RMicromega and Rdefinitions.
The original license header follows. *)
(************************************************************************)
(* 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-2008 *)
(* *)
(************************************************************************)
From
Coq
Require
Import
ZMicromega
.
From
Coq
Require
Import
QMicromega
.
From
Coq
Require
Import
QArith
.
From
Coq
Require
Import
ZArith
.
From
Coq
Require
Import
RingMicromega
.
From
Coq
Require
Import
VarMap
.
From
Coq
Require
Tauto
.
Declare
ML
Module
"micromega_plugin"
.
Ltac
preprocess
:
=
zify
;
unfold
Z
.
succ
in
*
;
unfold
Z
.
pred
in
*.
Ltac
lia
:
=
preprocess
;
xlia
;
abstract
(
intros
__wit
__varmap
__ff
;
change
(
Tauto
.
eval_f
(
Zeval_formula
(@
find
Z
Z0
__varmap
))
__ff
)
;
apply
(
ZTautoChecker_sound
__ff
__wit
)
;
vm_cast_no_check
(
eq_refl
true
)).
theories/tactics.v
View file @
90ce6473
...
...
@@ -3,7 +3,7 @@
(** This file collects general purpose tactics that are used throughout
the development. *)
From
Coq
Require
Import
Omega
.
From
Coq
Require
Export
P
satz
.
From
stdpp
Require
Export
p
satz
_axiomfree
.
From
stdpp
Require
Export
decidable
.
Lemma
f_equal_dep
{
A
B
}
(
f
g
:
∀
x
:
A
,
B
x
)
x
:
f
=
g
→
f
x
=
g
x
.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment