From bbf3682aa80bb86502e29018465e3602f0d9bb3e Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 1 Aug 2014 15:23:24 +0200
Subject: micromega : improve efficiency/termination of type-checking

* unused terms are generalised
* proof is abstract
---
 plugins/micromega/Psatz.v | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'plugins/micromega/Psatz.v')

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 69b0046b99..94b1fe9503 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -23,19 +23,24 @@ Require Import VarMap.
 Require Tauto.
 Declare ML Module "micromega_plugin".
 
+Ltac preprocess := 
+    zify ; unfold Z.succ in * ; unfold Z.pred in *.
+
 Ltac lia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
+  abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 Ltac nia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   xnlia ;
+  abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 
 Ltac xpsatz dom d :=
-- 
cgit v1.2.3