ROmega : merge O_CONSTANT* into a single O_BAD_CONSTANT

4 files changed, 77 insertions, 138 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 0476c385c..057752271 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1454,20 +1454,17 @@ Qed.
    [0<>...] or inequations [0<=...].
 
    First, the final steps leading to a contradiction:
-   - [O_CONSTANT_NOT_NUL i] :
-     equation i is [0=k] with a non-nul constant [k].
-   - [O_CONSTANT_NUL i] : disequation i is [0<>0].
-   - [O_CONSTANT_NEG i] :
-     inequation i is [0<=k] with a negative constant [k].
+   - [O_BAD_CONSTANT i] : hypothesis i has a constant body
+     and this constant is not compatible with the kind of i.
    - [O_CONTRADICTION i j] :
      inequations i and j have a sum which is a negative constant.
-     Shortcut for [(O_SUM 1 i 1 j (O_CONSTANT_NEG 0))].
+     Shortcut for [(O_SUM 1 i 1 j (O_BAD_CONSTANT 0))].
    - [O_NEGATE_CONTRADICT i j] :
      equation i and disequation j (or vice-versa) have the same body.
-     Shortcut for [(O_SUM 1 i (-1) j (O_CONSTANT_NUL 0))].
+     Shortcut for [(O_SUM 1 i (-1) j (O_BAD_CONSTANT 0))].
    - [O_NEGATE_CONTRADICT_INV i j] :
      equation i and disequation j (or vice-versa) have opposite bodies.
-     Shortcut for [(O_SUM 1 i 1 j (O_CONSTANT_NUL 0))].
+     Shortcut for [(O_SUM 1 i 1 j (O_BAD_CONSTANT 0))].
    - [O_NOT_EXACT_DIVIDE i k1 k2 t] :
      equation i has a body equivalent to [k1*t+k2] with [0<k2<k1].
 
@@ -1493,9 +1490,7 @@ Qed.
 Definition idx := nat. (** Index of an hypothesis in the list *)
 
 Inductive t_omega : Set :=
-  | O_CONSTANT_NOT_NUL : idx -> t_omega
-  | O_CONSTANT_NUL : idx -> t_omega
-  | O_CONSTANT_NEG : idx -> t_omega
+  | O_BAD_CONSTANT : idx -> t_omega
   | O_CONTRADICTION : idx -> idx -> t_omega
   | O_NEGATE_CONTRADICT : idx -> idx -> t_omega
   | O_NEGATE_CONTRADICT_INV : idx -> idx -> t_omega
@@ -1512,51 +1507,21 @@ Inductive t_omega : Set :=
 
 (** First, the final steps, leading to a contradiction *)
 
-(** [O_CONSTANT_NOT_NUL] *)
+(** [O_BAD_CONSTANT] *)
 
-Definition constant_not_nul (i : nat) (h : hyps) :=
+Definition bad_constant (i : nat) (h : hyps) :=
   match nth_hyps i h with
-  | EqTerm (Tint Nul) (Tint n) =>
-      if beq n Nul then h else absurd
+  | EqTerm (Tint Nul) (Tint n) => if beq n Nul then h else absurd
+  | NeqTerm (Tint Nul) (Tint n) => if beq n Nul then absurd else h
+  | LeqTerm (Tint Nul) (Tint n) => if bgt Nul n then absurd else h
   | _ => h
   end.
 
-Theorem constant_not_nul_valid :
- forall i : nat, valid_hyps (constant_not_nul i).
+Theorem bad_constant_valid i : valid_hyps (bad_constant i).
 Proof.
- unfold valid_hyps, constant_not_nul; intros i ep e lp H.
+ unfold valid_hyps, bad_constant; intros ep e lp H.
  generalize (nth_valid ep e i lp H); Simplify.
-Qed.
-
-(** [O_CONSTANT_NUL] *)
-
-Definition constant_nul (i : nat) (h : hyps) :=
-  match nth_hyps i h with
-  | NeqTerm (Tint Null) (Tint Null') =>
-      if beq Null Null' then absurd else h
-  | _ => h
-  end.
-
-Theorem constant_nul_valid : forall i : nat, valid_hyps (constant_nul i).
-Proof.
- unfold valid_hyps, constant_nul; intros;
- generalize (nth_valid ep e i lp); Simplify; simpl; intuition.
-Qed.
-
-(** [O_CONSTANT_NEG] *)
-
-Definition constant_neg (i : nat) (h : hyps) :=
-  match nth_hyps i h with
-  | LeqTerm (Tint Nul) (Tint Neg) =>
-     if bgt Nul Neg then absurd else h
-  | _ => h
-  end.
-
-Theorem constant_neg_valid : forall i : nat, valid_hyps (constant_neg i).
-Proof.
- unfold valid_hyps, constant_neg. intros.
- generalize (nth_valid ep e i lp). Simplify; simpl.
- rewrite gt_lt_iff in *; rewrite le_lt_iff; intuition.
+ rewrite gt_lt_iff in *. rewrite le_lt_iff. intuition.
 Qed.
 
 (** [O_CONTRADICTION] *)
@@ -1889,9 +1854,7 @@ Qed.
 
 Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
   match t with
-  | O_CONSTANT_NOT_NUL n => singleton (constant_not_nul n l)
-  | O_CONSTANT_NUL i => singleton (constant_nul i l)
-  | O_CONSTANT_NEG n => singleton (constant_neg n l)
+  | O_BAD_CONSTANT i => singleton (bad_constant i l)
   | O_CONTRADICTION i j => singleton (contradiction i j l)
   | O_NEGATE_CONTRADICT i j => singleton (negate_contradict i j l)
   | O_NEGATE_CONTRADICT_INV i j =>
@@ -1915,9 +1878,7 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
 Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
 Proof.
  simple induction tr; unfold valid_list_hyps, valid_hyps; simpl.
- - intros; left; now apply constant_not_nul_valid.
- - intros; left; now apply constant_nul_valid.
- - intros; left; now apply constant_neg_valid.
+ - intros; left; now apply bad_constant_valid.
  - intros; left; now apply contradiction_valid.
  - intros; left; now apply negate_contradict_valid.
  - intros; left; now apply negate_contradict_inv_valid.
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4fd224e2b..fa92903ba 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -101,8 +101,7 @@ let coq_p_and = lazy (constant  "Tand")
 let coq_p_imp = lazy (constant  "Timp")
 let coq_p_prop = lazy (constant  "Tprop")
 
-let coq_s_constant_not_nul = lazy (constant  "O_CONSTANT_NOT_NUL")
-let coq_s_constant_neg = lazy (constant  "O_CONSTANT_NEG")
+let coq_s_bad_constant = lazy (constant  "O_BAD_CONSTANT")
 let coq_s_div_approx = lazy (constant  "O_DIV_APPROX")
 let coq_s_not_exact_divide = lazy (constant  "O_NOT_EXACT_DIVIDE")
 let coq_s_exact_divide = lazy (constant  "O_EXACT_DIVIDE")
@@ -111,7 +110,6 @@ let coq_s_state = lazy (constant  "O_STATE")
 let coq_s_contradiction = lazy (constant  "O_CONTRADICTION")
 let coq_s_merge_eq = lazy (constant  "O_MERGE_EQ")
 let coq_s_split_ineq =lazy (constant  "O_SPLIT_INEQ")
-let coq_s_constant_nul =lazy (constant  "O_CONSTANT_NUL")
 let coq_s_negate_contradict =lazy (constant  "O_NEGATE_CONTRADICT")
 let coq_s_negate_contradict_inv =lazy (constant  "O_NEGATE_CONTRADICT_INV")
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 787ace603..ba8b097fe 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -42,8 +42,7 @@ val coq_p_and : Term.constr lazy_t
 val coq_p_imp : Term.constr lazy_t
 val coq_p_prop : Term.constr lazy_t
 
-val coq_s_constant_not_nul : Term.constr lazy_t
-val coq_s_constant_neg : Term.constr lazy_t
+val coq_s_bad_constant : Term.constr lazy_t
 val coq_s_div_approx : Term.constr lazy_t
 val coq_s_not_exact_divide : Term.constr lazy_t
 val coq_s_exact_divide : Term.constr lazy_t
@@ -52,7 +51,6 @@ val coq_s_state : Term.constr lazy_t
 val coq_s_contradiction : Term.constr lazy_t
 val coq_s_merge_eq : Term.constr lazy_t
 val coq_s_split_ineq : Term.constr lazy_t
-val coq_s_constant_nul : Term.constr lazy_t
 val coq_s_negate_contradict : Term.constr lazy_t
 val coq_s_negate_contradict_inv : Term.constr lazy_t
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 7a48b9788..45b141f92 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -855,87 +855,69 @@ let mk_direction_list l =
 
 (* \section{Rejouer l'historique} *)
 
-let get_hyp env_hyp i =
+let hyp_idx env_hyp i =
   let rec loop count = function
     | [] -> failwith (Printf.sprintf "get_hyp %d" i)
-    | CCEqua i' :: _ when Int.equal i i' -> count
+    | CCEqua i' :: _ when Int.equal i i' -> mk_nat count
     | _ :: l -> loop (succ count) l
   in loop 0 env_hyp
 
-let replay_history env env_hyp =
-  let rec loop env_hyp t =
-    match t with
-      | CONTRADICTION (e1,e2) :: l ->
-         mkApp (Lazy.force coq_s_contradiction,
-                [| mk_nat (get_hyp env_hyp e1.id);
-                   mk_nat (get_hyp env_hyp e2.id) |])
-      | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
-         mkApp (Lazy.force coq_s_div_approx,
-                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d;
-                   reified_of_omega env e2.body e2.constant;
-                   loop env_hyp l |])
-      | NOT_EXACT_DIVIDE (e1,k) :: l ->
-         let e2_constant = floor_div e1.constant k in
-         let d = e1.constant - e2_constant * k in
-         let e2_body = map_eq_linear (fun c -> c / k) e1.body in
-         mkApp (Lazy.force coq_s_not_exact_divide,
-                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k; Z.mk d;
-                   reified_of_omega env e2_body e2_constant |])
-      | EXACT_DIVIDE (e1,k) :: l ->
-         let e2_body = map_eq_linear (fun c -> c / k) e1.body in
-         let e2_constant = floor_div e1.constant k in
-         mkApp (Lazy.force coq_s_exact_divide,
-                [| mk_nat (get_hyp env_hyp e1.id); Z.mk k;
-                   reified_of_omega env e2_body e2_constant;
-                   loop env_hyp l |])
-      | (MERGE_EQ(e3,e1,e2)) :: l ->
-	  let n1 = get_hyp env_hyp e1.id and n2 = get_hyp env_hyp e2 in
-          mkApp (Lazy.force coq_s_merge_eq,
-		 [| mk_nat n1; mk_nat n2;
-		    loop (CCEqua e3:: env_hyp) l |])
-      | SUM(e3,(k1,e1),(k2,e2)) :: l ->
-         let n1 = get_hyp env_hyp e1.id
-         and n2 = get_hyp env_hyp e2.id in
-         mkApp (Lazy.force coq_s_sum,
-                [| Z.mk k1; mk_nat n1; Z.mk k2;
-                   mk_nat n2; (loop (CCEqua e3 :: env_hyp) l) |])
-      | CONSTANT_NOT_NUL(e,k) :: l ->
-          mkApp (Lazy.force coq_s_constant_not_nul,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      | CONSTANT_NEG(e,k) :: l ->
-          mkApp (Lazy.force coq_s_constant_neg,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      | STATE {st_new_eq=new_eq; st_def =def;
-               st_orig=orig; st_coef=m;
-               st_var=sigma } :: l ->
-         let n1 = get_hyp env_hyp orig.id
-         and n2 = get_hyp env_hyp def.id in
-         mkApp (Lazy.force coq_s_state,
-                [| Z.mk m; mk_nat n1; mk_nat n2;
-                   loop (CCEqua new_eq.id :: env_hyp) l |])
-      |	HYP _ :: l -> loop env_hyp l
-      |	CONSTANT_NUL e :: l ->
-	  mkApp (Lazy.force coq_s_constant_nul,
-		 [|  mk_nat (get_hyp env_hyp e) |])
-      |	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 (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
-	  let r2 = loop (CCEqua e2 :: env_hyp) l2 in
-	  mkApp (Lazy.force coq_s_split_ineq,
-                  [| mk_nat i; r1 ; r2 |])
-      |	(FORGET_C _ | FORGET _ | FORGET_I _) :: l ->
-	  loop env_hyp l
-      | (WEAKEN  _ ) :: l -> failwith "not_treated"
-      |	[] -> failwith "no contradiction"
-  in loop env_hyp
+let rec reify_trace env env_hyp = function
+  | CONSTANT_NOT_NUL(e,_) :: []
+  | CONSTANT_NEG(e,_) :: []
+  | CONSTANT_NUL e :: [] ->
+     mkApp (Lazy.force coq_s_bad_constant,[| hyp_idx env_hyp e |])
+  | NEGATE_CONTRADICT(e1,e2,direct) :: [] ->
+     let c = if direct then coq_s_negate_contradict
+             else coq_s_negate_contradict_inv
+     in
+     mkApp (Lazy.force c, [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2.id |])
+  | CONTRADICTION (e1,e2) :: [] ->
+     mkApp (Lazy.force coq_s_contradiction,
+            [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2.id |])
+  | NOT_EXACT_DIVIDE (e1,k) :: [] ->
+     let e2_constant = floor_div e1.constant k in
+     let d = e1.constant - e2_constant * k in
+     let e2_body = map_eq_linear (fun c -> c / k) e1.body in
+     mkApp (Lazy.force coq_s_not_exact_divide,
+            [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d;
+               reified_of_omega env e2_body e2_constant |])
+  | DIVIDE_AND_APPROX (e1,e2,k,d) :: l ->
+     mkApp (Lazy.force coq_s_div_approx,
+            [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d;
+               reified_of_omega env e2.body e2.constant;
+               reify_trace env env_hyp l |])
+  | EXACT_DIVIDE (e1,k) :: l ->
+     let e2_body = map_eq_linear (fun c -> c / k) e1.body in
+     let e2_constant = floor_div e1.constant k in
+     mkApp (Lazy.force coq_s_exact_divide,
+            [| hyp_idx env_hyp e1.id; Z.mk k;
+               reified_of_omega env e2_body e2_constant;
+               reify_trace env env_hyp l |])
+  | MERGE_EQ(e3,e1,e2) :: l ->
+     mkApp (Lazy.force coq_s_merge_eq,
+            [| hyp_idx env_hyp e1.id; hyp_idx env_hyp e2;
+               reify_trace env (CCEqua e3:: env_hyp) l |])
+  | SUM(e3,(k1,e1),(k2,e2)) :: l ->
+     mkApp (Lazy.force coq_s_sum,
+            [| Z.mk k1; hyp_idx env_hyp e1.id;
+               Z.mk k2; hyp_idx env_hyp e2.id;
+               reify_trace env (CCEqua e3 :: env_hyp) l |])
+  | STATE {st_new_eq=new_eq; st_def =def;
+           st_orig=orig; st_coef=m;
+           st_var=sigma } :: l ->
+     mkApp (Lazy.force coq_s_state,
+            [| Z.mk m; hyp_idx env_hyp orig.id; hyp_idx env_hyp def.id;
+               reify_trace env (CCEqua new_eq.id :: env_hyp) l |])
+  | HYP _ :: l -> reify_trace env env_hyp l
+  | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ ->
+     let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in
+     let r2 = reify_trace env (CCEqua e2 :: env_hyp) l2 in
+     mkApp (Lazy.force coq_s_split_ineq,
+            [| hyp_idx env_hyp e.id; r1 ; r2 |])
+  | (FORGET_C _ | FORGET _ | FORGET_I _) :: l -> reify_trace env env_hyp l
+  | WEAKEN  _ :: l -> failwith "not_treated"
+  | _ -> failwith "bad history"
 
 let rec decompose_tree env ctxt = function
    Tree(i,left,right) ->
@@ -954,7 +936,7 @@ let rec decompose_tree env ctxt = function
   | Leaf s ->
       decompose_tree_hyps s.s_trace env ctxt (IntSet.elements s.s_equa_deps)
 and decompose_tree_hyps trace env ctxt = function
-    [] -> app coq_e_solve [| replay_history env ctxt trace |]
+    [] -> app coq_e_solve [| reify_trace env ctxt trace |]
   | (i::l) ->
       let equation =
         try IntHtbl.find env.equations i