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

7 files changed, 112 insertions, 52 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 497fcdb6cb..aa59daf5fa 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -300,6 +300,7 @@ let coq_eq_ind_r = lazy (constant "eq_ind_r")
 let coq_dec_or = lazy (constant "dec_or")
 let coq_dec_and = lazy (constant "dec_and")
 let coq_dec_imp = lazy (constant "dec_imp")
+let coq_dec_iff = lazy (constant "dec_iff")
 let coq_dec_not = lazy (constant "dec_not")
 let coq_dec_False = lazy (constant "dec_False")
 let coq_dec_not_not = lazy (constant "dec_not_not")
@@ -310,6 +311,7 @@ let coq_not_and = lazy (constant "not_and")
 let coq_not_imp = lazy (constant "not_imp")
 let coq_not_not = lazy (constant "not_not")
 let coq_imp_simp = lazy (constant "imp_simp")
+let coq_iff = lazy (constant "iff")
 
 (* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
 
@@ -386,6 +388,8 @@ let destructurate_prop t =
     | _, [_;_] when c = Lazy.force coq_Zgt -> Kapp (Zgt,args)
     | _, [_;_] when c = build_coq_and () -> Kapp (And,args)
     | _, [_;_] when c = build_coq_or () -> Kapp (Or,args)
+    | _, [t1;t2] when c = Lazy.force coq_iff -> 
+	Kapp (And,[mkArrow t1 t2;mkArrow t2 t1])
     | _, [_] when c = build_coq_not () -> Kapp (Not,args)
     | _, [] when c = build_coq_False () -> Kapp (False,args)
     | _, [] when c = build_coq_True () -> Kapp (True,args)
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 5583ce4c90..fda18c6cef 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -1848,6 +1848,15 @@ Definition exact_divide (k : Z) (body : term) (t : nat)
           end
       | false => TrueTerm
       end
+  | NeqTerm (Tint Z0) b =>
+      match eq_term (scalar_norm t (body * Tint k)%term) b with
+      | true =>
+          match eq_Z k 0 with
+          | true => FalseTerm
+          | false => NeqTerm (Tint 0) body
+          end
+      | false => TrueTerm
+      end
   | _ => TrueTerm
   end.
 
@@ -1858,18 +1867,24 @@ Theorem exact_divide_valid :
 unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify;
  simpl in |- *; auto; elim_eq_term (scalar_norm t (k2 * Tint k1)%term) t1;
  simpl in |- *; auto; elim_eq_Z k1 0; simpl in |- *; 
- auto; intros H1 H2; elim H2; elim scalar_norm_stable; 
- simpl in |- *; generalize H1; case (interp_term e k2); 
+ auto; intros H1 H2; elim H2; elim scalar_norm_stable;
+ simpl in |- *; 
+ [
+ generalize H1; case (interp_term e k2); 
  try trivial;
  (case k1; simpl in |- *;
    [ intros; absurd (0 = 0); assumption
    | intros p2 p3 H3 H4; discriminate H4
-   | intros p2 p3 H3 H4; discriminate H4 ]).
-
+   | intros p2 p3 H3 H4; discriminate H4 ])
+ |
+ subst k1; rewrite Zmult_comm; simpl in *; intros; absurd (0=0); trivial
+ |
+ generalize H1; case (interp_term e k2); 
+ try trivial; intros p2 p3 H3 H4; discriminate H4
+ ].
 Qed.
 
 
-
 (* \paragraph{[O_DIV_APPROX]}
   La preuve reprend le schéma de la précédente mais on
   est sur une opération de type valid1 et non sur une opération terminale. *)
@@ -1954,7 +1969,7 @@ Definition state (m : Z) (s : step) (prop1 prop2 : proposition) :=
   match prop1 with
   | EqTerm (Tint Z0) b1 =>
       match prop2 with
-      | EqTerm (Tint Z0) (b2 + - b3)%term =>
+      | EqTerm b2 b3 =>
           EqTerm (Tint 0) (rewrite s (b1 + (- b3 + b2) * Tint m)%term)
       | _ => TrueTerm
       end
@@ -1965,10 +1980,8 @@ Theorem state_valid : forall (m : Z) (s : step), valid2 (state m s).
 
 unfold valid2 in |- *; intros m s ep e p1 p2; unfold state in |- *; Simplify;
  simpl in |- *; auto; elim (rewrite_stable s e); simpl in |- *; 
- intros H1 H2; elim H1;
- rewrite (Zplus_comm (- interp_term e t5) (interp_term e t3)); 
- elim H2; simpl in |- *; reflexivity.
-
+ intros H1 H2; elim H1.
+ rewrite H2; rewrite Zplus_opp_l; simpl; reflexivity.
 Qed.
 
 (* \subsubsection{Tactiques générant plusieurs but}
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml
index 285fc0ca8c..e7e7b3c590 100644
--- a/contrib/romega/refl_omega.ml
+++ b/contrib/romega/refl_omega.ml
@@ -6,6 +6,10 @@
 
  *************************************************************************)
 
+(* The addition on int, since it while be hidden soon by the one on BigInt *)
+
+let (+.) = (+)
+
 open Const_omega
 module OmegaSolver = Omega.MakeOmegaSolver (Bigint)
 open OmegaSolver
@@ -792,6 +796,9 @@ and oproposition_of_constr env ((negated,depends,origin,path) as ctxt) gl c =
     | Kimp(t1,t2) ->
 	binprop env ctxt (not negated) (not negated) gl 
 	  (fun i x y -> Pimp(i,x,y)) t1 t2
+    | Kapp("iff",[t1;t2]) ->
+	binprop env ctxt negated negated gl 
+	  (fun i x y -> Pand(i,x,y)) (Term.mkArrow t1 t2) (Term.mkArrow t2 t1)
     | _ -> Pprop c
   with e when Logic.catchable_exception e -> Pprop c
 
@@ -995,10 +1002,10 @@ let rec equas_of_solution_tree = function
       list_union (equas_of_solution_tree t1) (equas_of_solution_tree t2)
   | Leaf s -> s.s_equa_deps
 
-
-(* Because of really_useful_prop, decidable formulas such as Pfalse
-   and Ptrue are moved to Pprop, thus breaking the decidability check
-   in ReflOmegaCore.concl_to_hyp... *)
+(* [really_useful_prop] pushes useless props in a new Pprop variable *)
+(* Things get shorter, but may also get wrong, since a Prop is considered 
+   to be undecidable in ReflOmegaCore.concl_to_hyp, whereas for instance 
+   Pfalse is decidable. So should not be used on conclusion (??) *)
 
 let really_useful_prop l_equa c =
   let rec real_of = function
@@ -1034,6 +1041,14 @@ let really_useful_prop l_equa c =
     None -> Pprop (real_of c)
   | Some t -> t
 
+let rec vars_of_prop = function 
+  | Pequa(_,e) -> vars_of_equations [e]
+  | Pnot p -> vars_of_prop p
+  | Por(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | Pand(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | Pimp(_,p1,p2) -> list_union (vars_of_prop p1) (vars_of_prop p2)
+  | _ -> []
+
 let rec display_solution_tree ch = function
     Leaf t -> 
       output_string ch 
@@ -1160,10 +1175,15 @@ let replay_history env env_hyp =
       |	CONSTANT_NUL e :: l ->
 	  mkApp (Lazy.force coq_s_constant_nul, 
 		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	NEGATE_CONTRADICT(e1,e2,b) :: l ->
+      |	NEGATE_CONTRADICT(e1,e2,true) :: l ->
 	  mkApp (Lazy.force coq_s_negate_contradict, 
 		 [|  mk_nat (get_hyp env_hyp e1.id);
 		     mk_nat (get_hyp env_hyp e2.id) |])
+      |	NEGATE_CONTRADICT(e1,e2,false) :: l ->
+	  mkApp (Lazy.force coq_s_negate_contradict_inv, 
+		 [|  mk_nat (List.length e2.body); 
+		     mk_nat (get_hyp env_hyp e1.id);
+		     mk_nat (get_hyp env_hyp e2.id) |])
       | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: l ->
 	  let i =  get_hyp env_hyp e.id in
 	  let r1 = loop (CCEqua e1 :: env_hyp) l1 in
@@ -1254,14 +1274,18 @@ let resolution env full_reified_goal systems_list =
   let l_hyps = id_concl :: list_remove id_concl l_hyps' in
   let useful_hyps =
     List.map (fun id -> List.assoc id full_reified_goal) l_hyps in
-  let useful_vars = vars_of_equations equations in
+  let useful_vars = 
+    let really_useful_vars = vars_of_equations equations in
+    let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in     
+    list_uniq (List.sort compare (really_useful_vars @ concl_vars))
+  in 
   (* variables a introduire *)
   let to_introduce = add_stated_equations env solution_tree in
   let stated_vars =  List.map (fun (v,_,_,_) -> v) to_introduce in
   let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
   let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
   (* L'environnement de base se construit en deux morceaux :
-     - les variables des équations utiles
+     - les variables des équations utiles (et de la conclusion)
      - les nouvelles variables declarées durant les preuves *)
   let all_vars_env = useful_vars @ stated_vars in
   let basic_env =
@@ -1280,8 +1304,7 @@ let resolution env full_reified_goal systems_list =
               to_introduce in
   let reified_concl = 
     match useful_hyps with
-      (Pnot p) :: _ ->
-	reified_of_proposition env (really_useful_prop useful_equa_id p)
+      (Pnot p) :: _ -> reified_of_proposition env p
     | _ ->  reified_of_proposition env Pfalse in
   let l_reified_terms =
     (List.map
@@ -1301,9 +1324,13 @@ let resolution env full_reified_goal systems_list =
 	          [| e.e_trace |]
       |	((O_left | O_mono) :: l) -> app coq_p_left [| loop l |]
       |	(O_right :: l) -> app coq_p_right [| loop l |] in
-    app coq_pair_step 
-        [| mk_nat (list_index e.e_origin.o_hyp l_hyps) ;
-	   loop e.e_origin.o_path |] in
+    let correct_index = 
+      let i = list_index e.e_origin.o_hyp l_hyps in 
+      (* PL: it seems that additionnally introduced hyps are in the way during 
+             normalization, hence this index shifting... *) 
+      if i=0 then 0 else i +. List.length to_introduce
+    in 	
+    app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =
     mk_list (Lazy.force coq_h_step) (List.map normalize_equation equations) in
 
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.