ROmega : O_STATE turned into a O_SUM

 We benefit from the fact that we normalize now *all* hypotheses
 even the one defining the "stated" variable: it is produced as
  ...def of v... = v
 and normalized as
  -v + ...def of v... = 0
 which is precisely what we should add to the initial equation during
 a O_STATE.

4 files changed, 26 insertions, 59 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 972070657..f08d62162 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -1175,7 +1175,11 @@ Proof.
  symmetry. apply plus_0_r.
 Qed.
 
-(** Adding a constant *)
+(** Adding a constant
+
+    Instead of using [scalar_norm_add t 1 k], the following
+    definition spares some computations.
+ *)
 
 Fixpoint add_norm (t : term) (k : int) : term :=
   match t with
@@ -1434,7 +1438,6 @@ Qed.
      with one these bodies.
    - [O_SPLIT_INEQ i cont1 cont2] :
      disequation i is split into a disjonction of inequations.
-   - [O_STATE k i j cont] : now shortcut for [O_SUM 1 i k j cont].
 *)
 
 Definition idx := nat. (** Index of an hypothesis in the list *)
@@ -1447,8 +1450,7 @@ Inductive t_omega : Set :=
   | O_DIV_APPROX : idx -> int -> int -> term -> t_omega -> t_omega
   | O_SUM : int -> idx -> int -> idx -> t_omega -> t_omega
   | O_MERGE_EQ : idx -> idx -> t_omega -> t_omega
-  | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega
-  | O_STATE : int -> idx -> idx -> t_omega -> t_omega.
+  | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega.
 
 (** ** Actual resolution steps of an omega normalized goal *)
 
@@ -1662,30 +1664,6 @@ Proof.
     symmetry ; trivial.
 Qed.
 
-
-(** [O_STATE] *)
-
-Definition state (m : int) (prop1 prop2 : proposition) :=
-  match prop1 with
-  | EqTerm (Tint Null) b1 =>
-      match prop2 with
-      | EqTerm (Tint Null') b2 =>
-          if beq Null 0 && beq Null' 0
-          then EqTerm (Tint 0) (fusion b1 b2 1 m)
-          else TrueTerm
-      | _ => TrueTerm
-      end
-  | _ => TrueTerm
-  end.
-
-Theorem state_valid : forall (m : int), valid2 (state m).
-Proof.
- unfold valid2; intros m ep e p1 p2.
- unfold state; Simplify; simpl; auto.
- rewrite <- fusion_stable. simpl in *. intros H H'.
- rewrite <- H, <- H'. now rewrite !mult_0_l, plus_0_l.
-Qed.
-
 (** ** Replaying the resolution trace *)
 
 Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps :=
@@ -1703,8 +1681,6 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps :=
       execute_omega cont (apply_oper_2 i1 i2 merge_eq l)
   | O_SPLIT_INEQ i cont1 cont2 =>
       split_ineq i (execute_omega cont1) (execute_omega cont2) l
-  | O_STATE m i1 i2 cont =>
-      execute_omega cont (apply_oper_2 i1 i2 (state m) l)
   end.
 
 Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr).
@@ -1712,7 +1688,6 @@ Proof.
  simple induction tr; unfold valid_list_hyps, valid_hyps; simpl.
  - intros; left; now apply bad_constant_valid.
  - intros; left; now apply not_exact_divide_valid.
-
  - intros m k body t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_1_valid m (exact_divide k body)
@@ -1733,8 +1708,6 @@ Proof.
     apply
      (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e
         lp H).
- - intros m i1 i2 t' Ht' ep e lp H; apply Ht';
-    apply (apply_oper_2_valid i1 i2 (state m) (state_valid m) ep e lp H).
 Qed.
 
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 6e2fa5ed3..ce47ef16a 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -106,7 +106,6 @@ 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")
 let coq_s_sum = lazy (constant  "O_SUM")
-let coq_s_state = lazy (constant  "O_STATE")
 let coq_s_merge_eq = lazy (constant  "O_MERGE_EQ")
 let coq_s_split_ineq =lazy (constant  "O_SPLIT_INEQ")
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index b00525561..b4599c831 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -47,7 +47,6 @@ 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
 val coq_s_sum : Term.constr lazy_t
-val coq_s_state : Term.constr lazy_t
 val coq_s_merge_eq : Term.constr lazy_t
 val coq_s_split_ineq : Term.constr lazy_t
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 48e06a93e..95cf2083c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -214,17 +214,15 @@ let new_omega_var, rst_omega_var =
 
 let display_omega_var i = Printf.sprintf "OV%d" i
 
-(* Register a new internal variable corresponding to some oformula
-   (normally an [Oatom]). *)
-
-let add_omega_var env t =
-  let v = new_omega_var () in
-  env.om_vars <- (v,t) :: env.om_vars
-
-(* Ajout forcé d'un lien entre un terme et une variable  Cas où la
-   variable est créée par Omega et où il faut la lier après coup à un atome
-   réifié introduit de force *)
-let force_omega_var env t v =
+(* Register an internal variable corresponding to some oformula
+   (normally an [Oatom]). This omega variable could be a new one,
+   or one already created during the omega resolution (cf. STATE). *)
+
+let add_omega_var env t ov =
+  let v = match ov with
+    | None -> new_omega_var ()
+    | Some v -> v
+  in
   env.om_vars <- (v,t) :: env.om_vars
 
 (* Récupère le terme associé à une variable omega *)
@@ -238,12 +236,12 @@ let unintern_omega env v =
    l'environnement initial contenant tout. Il faudra le réduire après
    calcul des variables utiles. *)
 
-let add_reified_atom sync t env =
+let add_reified_atom opt_omega_var t env =
   try List.index0 Term.eq_constr t env.terms
   with Not_found ->
     let i = List.length env.terms in
     (* synchronize atom indexes and omega variables *)
-    let () = if sync then add_omega_var env (Oatom i) in
+    add_omega_var env (Oatom i) opt_omega_var;
     env.terms <- env.terms @ [t]; i
 
 let get_reified_atom env =
@@ -514,11 +512,11 @@ let rec oformula_of_constr env t =
         | None ->
            match Z.get_scalar t2 with
            | Some n -> Omult (oformula_of_constr env t1, Oint n)
-           | None -> Oatom (add_reified_atom true t env))
+           | None -> Oatom (add_reified_atom None t env))
     | Topp t -> Oopp(oformula_of_constr env t)
     | Tsucc t -> Oplus(oformula_of_constr env t, Oint one)
     | Tnum n -> Oint n
-    | Tother -> Oatom (add_reified_atom true t env)
+    | Tother -> Oatom (add_reified_atom None t env)
 
 and binop env c t1 t2 =
   let t1' = oformula_of_constr env t1 in
@@ -713,14 +711,12 @@ let add_stated_equations env tree =
     (* Notez que si l'ordre de création des variables n'est pas respecté,
      * ca va planter *)
     let coq_v = coq_of_formula env v_def in
-    let v = add_reified_atom false coq_v env in
+    let v = add_reified_atom (Some st.st_var) coq_v env in
     (* Le terme qu'il va falloir introduire *)
     let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in
     (* sa représentation sous forme d'équation mais non réifié car on n'a pas
      * l'environnement pour le faire correctement *)
     let term_to_reify = (v_def,Oatom v) in
-    (* enregistre le lien entre la variable omega et la variable Coq *)
-    force_omega_var env (Oatom v) st.st_var;
     (v, term_to_generalize,term_to_reify,st.st_def.id) in
  List.map add_env stated_equations
 
@@ -909,12 +905,12 @@ let rec reify_trace env env_hyp = function
             [| 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 |])
+  | STATE {st_new_eq; st_def; st_orig; st_coef } :: l ->
+     (* we now produce a [O_SUM] here *)
+     mkApp (Lazy.force coq_s_sum,
+            [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id;
+               Z.mk st_coef; hyp_idx env_hyp st_def.id;
+               reify_trace env (CCEqua st_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