Improvements / Bug fixes for ROmega

-----------------------------------

All romega tests in the test-suite are now bug-free. The only known
remaining limitation of romega with respect to omega is that it cannot
handle stuff on nat.

* Equivalences A<->B are now understood by romega (as well as omega), 
  and seen as (A->B)/\(B->A). There might be a smarter way to procede, 
  for instance having a primitive Iff construct and trying to break 
  equivalences as late as possible. 

* Conclusion-as-Pprop issue: 
  After the resolution by the abstract omega machinery, useless parts
  are discarded from the reification process by replacing them with
  Pprop construct (see really_useful_prop). This allow to decrease 
  the size of the proof terms and speed up their normalisation, I guess.   
  But when such Pprop are created in the conclusion, this leads to 
  failure, since concl is negated, and this is donc only if it is 
  decidable. And introducing some Pprop might change the decidability 
  status of the concl: for instance, Pfalse is decidable, whereas 
  Pprop False is considered as _not_ decidable. Quick fix: no more 
  really_useful_prop applied on concl (needs careful computation of 
  useful_var). 

* NEGATE_CONTRADICT(_INV): 
  This trace instrution comes in fact in two flavors, according to a
  boolean flag. We now translate to O_NEGATE_CONTRADICT_INV if this 
  flag is false. (fix Besson's bug #1298)

* EXACT_DIVIDE: 
  could be used on NeqTerm and not only on EqTerm. 

* h_step indexes: 
  The abstract omega machinery can introduce new hyps. In the list of hyps, 
  they appears _before_ the regular one (but after the goal seen as an hyp 
  by negating it). But the normalization steps were applied to regular hyps
  thanks to their indexes counted _before_ the addition extra hyps. 

* extra hyps (a)normal forms: 
  extra hyps and variables are initially of the shape 
     poly(v1,...,v(n-1)) = vn
  but O_STATE was expecting them in form 0 = poly(...) + -vn
  (by the way, SPLIT_INEQ should be checked someday). 

Since the above is one weekend's worth of debugging, there might well
remain some more bugs :-(. 

For the record, here's the less painful way to debug a failed romega run: 
 - activate debug flag in omega.ml and refl_omega.ml 
 - at the bottom of refl_omega, replace normalise_vm_in_concl with 
   convert_no_check (see comment there): this allow to skip the usually 
   _huge_ error message about "Impossible to unify True with ..."
 - run the romega
 - try to run Qed, and enjoy the nice errror message about a 
   (omega_tactic ? ? ? ?) that should be reducible to True. 
   Here starts the real debug work...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9962 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 46 insertions, 30 deletions

diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v
index 4614c90db0..accaec41ed 100644
--- a/test-suite/success/Omega0.v
+++ b/test-suite/success/Omega0.v
@@ -8,16 +8,16 @@ Lemma test_romega_0 :
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros.
-(*omega.*)
-Admitted.
+omega.
+Qed.
 
 Lemma test_romega_0b : 
  forall m m', 
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros m m'.
-(*omega.*)
-Admitted.
+omega.
+Qed.
 
 Lemma test_romega_1 : 
  forall (z z1 z2 : Z), 
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index 04b666edd3..ff1f57df32 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -7,8 +7,8 @@ Lemma lem1 :
  forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z.
 Proof.
 intros x y.
- (*romega.*)
-Admitted.
+romega.
+Qed.
 
 (* Proposed by Pierre Crégut *)
 
@@ -22,8 +22,8 @@ Qed.
 Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z.
 Proof.
 intros.
- (*romega.*)
-Admitted.
+romega. 
+Qed.
 
 (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *)
 (* internal variable and a section variable (June 2001) *)
@@ -68,7 +68,7 @@ Variable n : nat.
 Variable ap_n : n <> 0.
 Let delta := f n ap_n.
 Lemma lem7 : n = n.
- (*romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+ (*romega. ---> ROMEGA CANT DEAL WITH NAT*)
 Admitted.
 End C.
 
@@ -76,7 +76,7 @@ End C.
 Require Import Omega.
 Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
 intros.
-(* romega.*) (*ROMEGA CANT DEAL WITH NAT*)
+(* romega. ---> ROMEGA CANT DEAL WITH NAT*)
 Admitted.
 
 (* Bug that what caused by the use of intro_using in Omega *)
@@ -84,7 +84,7 @@ Require Import Omega.
 Lemma lem9 :
  forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p.
 intros.
-(* romega.*)(*ROMEGA CANT DEAL WITH NAT*) 
+(* romega. ---> ROMEGA CANT DEAL WITH NAT*) 
 Admitted.
 
 (* Check that the interpretation of mult on nat enforces its positivity *)
diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v
index 0efca1e13f..86cf49cb5e 100644
--- a/test-suite/success/ROmega0.v
+++ b/test-suite/success/ROmega0.v
@@ -8,16 +8,16 @@ Lemma test_romega_0 :
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_0b : 
  forall m m', 
   0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'.
 Proof.
 intros m m'.
-(*romega.*)
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_1 : 
  forall (z z1 z2 : Z), 
@@ -42,8 +42,8 @@ Lemma test_romega_1b :
     z >= 0.
 Proof.
 intros z z1 z2.
-(* romega. *) 
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_2 : forall a b c:Z, 
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
@@ -56,8 +56,8 @@ Lemma test_romega_2b : forall a b c:Z,
  0<=a-b<=1 -> b-c<=2 -> a-c<=3.
 Proof.
 intros a b c.
-(*romega.*)
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_3 : forall a b h hl hr ha hb, 
  0 <= ha - hl <= 1 -> 
@@ -115,22 +115,22 @@ Qed.
 Lemma test_romega_6b : forall z, z>=0 -> 0>z+2 -> False.
 Proof.
 intros z.
-(*romega. *)
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_7 : forall z, 
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
 
 Lemma test_romega_7b : forall z, 
   0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1.
 Proof.
 intros.
-(*romega.*)
-Admitted.
+romega.
+Qed.
 
 (* Magaud #240 *)
 
@@ -144,6 +144,9 @@ intros x y.
 romega.
 Qed.
 
+(* Besson #1298 *)
 
-
-
+Lemma test_romega9 : forall z z':Z, z<>z' -> z'=z -> False.
+intros.
+romega.
+Qed.
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v
index 9d47c9f654..a3be2898c1 100644
--- a/test-suite/success/ROmega2.v
+++ b/test-suite/success/ROmega2.v
@@ -4,6 +4,20 @@ Require Import ZArith ROmega.
 
 Open Scope Z_scope.
 
+
+(* First a simplified version used during debug of romega on Test46 *)
+Lemma Test46_simplified : 
+forall v1 v2 v5 : Z,
+0 = v2 + v5 ->
+0 < v5 ->
+0 < v2 ->
+4*v2 <> 5*v1.
+intros.
+romega.
+Qed.
+
+
+(* The complete problem *)
 Lemma Test46 : 
 forall v1 v2 v3 v4 v5 : Z,
 ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) ->
@@ -23,6 +37,5 @@ forall v1 v2 v3 v4 v5 : Z,
 ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9))
 -> False.
 intros.
-(*romega.*)
-Admitted.
-
+romega.
+Qed.