use Psatz without using axioms about real numbers

_CoqProject

@@ -21,6 +21,7 @@ prelude/listset.v
 prelude/streams.v
 prelude/gmap.v
 prelude/base.v
+prelude/psatz_axiomfree.v
 prelude/tactics.v
 prelude/prelude.v
 prelude/listset_nodup.v

prelude/psatz_axiomfree.v

+(** 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)).

prelude/tactics.v

@@ -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 Psatz.
+From iris.prelude Require Export psatz_axiomfree.
 From iris.prelude Require Export decidable.
 
 Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.

[Robbert Krebbers]

When compiling I get:

*** Warning: in file prelude/psatz_axiomfree.v, declared ML module micromega_plugin has not been found!
*** Warning: in file prelude/psatz_axiomfree.v, declared ML module micromega_plugin has not been found!

Anything we can do about that?

[Ralf Jung]

Add a "grep" to the Makefile to filter it? ;)

I have no idea what this warning is trying to tell me -- after all, it is loading the module. If I use a bogus name, I get that error and also, later, a failure to find the plugin in the load path. On the plus side, the warning only appears when compiling psatz_axiomfree, which will not usually be recompiled. ;)

[Robbert Krebbers]

I also wonder about the intended behavior of adding a Declare ML Module that refers to an ML module in another Coq project. In this case it seems to work, but is that something we can rely on? Maybe we should create a Coq bug report about this error message and see what they have to say.

[Ralf Jung]

shrug I don't care strongly, this is a hack anyway, and if it stops working, then whatever. But I won't stop you. ;)