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
0af80759
Commit
0af80759
authored
Aug 29, 2016
by
Ralf Jung
Browse files
Turn out Coq 8.5 already comes with a module to get lia without axioms: Lia
parent
a7c55441
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/psatz_axiomfree.v
deleted
100644 → 0
View file @
a7c55441
(** 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 @
0af80759
...
...
@@ -3,7 +3,7 @@
(** This file collects general purpose tactics that are used throughout
the development. *)
From
Coq
Require
Import
Omega
.
From
stdpp
Require
Export
psatz_axiomfree
.
From
Coq
Require
Export
Lia
.
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