ROmega: division-aware ReflOmegaCore, allowing trace without terms

 The trace only mentions the constant k by which we want to divide
 the equation, not anymore the equation we obtain after the division.
 Shorter trace, and it won't take much more time to perform the few
 Z.div than checking as currently the equality of the initial equation
 and the final equation multiplied by k.

4 files changed, 134 insertions, 114 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index f95cfe364..d242264a9 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -75,6 +75,18 @@ Module Type Int.
 
   (** Btw, lt_0_1 could be deduced from this last axiom *)
 
+  (** Now we also require a division function.
+      It is deliberately underspecified, since that's enough
+      for the proofs below. But the most appropriate variant
+      (and the one needed to stay in sync with the omega engine)
+      is "Floor" (the historical version of Coq's [Z.div]). *)
+
+  Parameter diveucl : t -> t -> t * t.
+  Notation "i / j" := (fst (diveucl i j)).
+  Notation "i 'mod' j" := (snd (diveucl i j)).
+  Axiom diveucl_spec :
+    forall i j, j<>0 -> i = j * (i/j) + (i mod j).
+
 End Int.
 
 
@@ -133,6 +145,9 @@ Module Z_as_Int <: Int.
 
   Definition le_lt_int := Z.lt_le_pred.
 
+  Definition diveucl := Z.div_eucl.
+  Definition diveucl_spec := Z.div_mod.
+
 End Z_as_Int.
 
 
@@ -1124,6 +1139,50 @@ Proof.
  rewrite IHt2. simpl. apply plus_assoc.
 Qed.
 
+(** Division by a constant
+
+    All the non-constant coefficients should be exactly dividable *)
+
+Fixpoint scalar_div (t : term) (k : int) : option (term * int) :=
+  match t with
+  | v * Tint x + l =>
+    let (q,r) := diveucl x k in
+    if (r =? 0)%I then
+      match scalar_div l k with
+      | None => None
+      | Some (u,c) => Some (v * Tint q + u, c)
+      end
+    else None
+  | Tint x =>
+    let (q,r) := diveucl x k in
+    Some (Tint q, r)
+  | _ => None
+  end%term.
+
+Lemma scalar_div_stable e t k u c : k<>0 ->
+  scalar_div t k = Some (u,c) ->
+  interp_term e (u * Tint k + Tint c) = interp_term e t.
+Proof.
+ revert u c.
+ induction t; simpl; Simplify; try easy.
+ - intros u c Hk. assert (H := diveucl_spec t0 k Hk).
+   simpl in H.
+   destruct diveucl as (q,r). simpl in H. rewrite H.
+   injection 1 as <- <-. simpl. f_equal. apply mult_comm.
+ - intros u c Hk.
+   destruct t1; simpl; Simplify; try easy.
+   destruct t1_2; simpl; Simplify; try easy.
+   assert (H := diveucl_spec t0 k Hk).
+   simpl in H.
+   destruct diveucl as (q,r). simpl in H. rewrite H.
+   case beq_reflect; [intros -> | easy].
+   destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy].
+   injection 1 as <- ->. simpl.
+   rewrite <- (IHt2 u' c Hk); simpl; auto.
+   rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11.
+Qed.
+
+
 (** Fusion of two equations.
 
     From two normalized equations, this fusion will produce
@@ -1337,16 +1396,15 @@ Qed.
    First, the final steps leading to a contradiction:
    - [O_BAD_CONSTANT i] : hypothesis i has a constant body
      and this constant is not compatible with the kind of i.
-   - [O_NOT_EXACT_DIVIDE i k1 k2 t] :
-     equation i has a body equivalent to [k1*t+k2] with [0<k2<k1].
+   - [O_NOT_EXACT_DIVIDE i k] :
+     equation i can be factorized as some [k*t+c] with [0<c<k].
 
    Now, the intermediate steps leading to a new hypothesis:
-   - [O_EXACT_DIVIDE i k1 t cont] :
-     (dis)equation i has a body equivalent to [k1*t] with [k1<>0],
-     we change it (in-place) for (dis)equation [0=t].
-   - [O_DIV_APPROX i k1 k2 t cont] :
-     inequation i has a body equivalent to [k1*t+k2] with [0<k1]
-     and [k2<k1], we change it (in-place) for inequation [0<=t].
+   - [O_DIVIDE i k cont] :
+     the body of hypothesis i could be factorized as [k*t+c]
+     with either [k<>0] and [c=0] for a (dis)equation, or
+     [0<k] and [c<k] for an inequation. We change in-place the
+     body of i for [t].
    - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose
      kind depends on the kind of hypotheses [i1] and [i2], and
      whose body is [k1*body(i1) + k2*body(i2)]. Depending of the
@@ -1362,10 +1420,9 @@ Definition idx := nat. (** Index of an hypothesis in the list *)
 
 Inductive t_omega : Set :=
   | O_BAD_CONSTANT : idx -> t_omega
-  | O_NOT_EXACT_DIVIDE : idx -> int -> int -> term -> t_omega
+  | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega
 
-  | O_EXACT_DIVIDE : idx -> int -> term -> t_omega -> t_omega
-  | O_DIV_APPROX : idx -> int -> int -> term -> t_omega -> t_omega
+  | O_DIVIDE : idx -> int -> 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.
@@ -1391,84 +1448,84 @@ Proof.
  rewrite le_lt_iff. intuition.
 Qed.
 
-(** [NOT_EXACT_DIVIDE] *)
+(** [O_NOT_EXACT_DIVIDE] *)
 
-Definition not_exact_divide (i : nat) (k1 k2 : int) (body : term)
-  (l : hyps) :=
+Definition not_exact_divide (i : nat) (k : int) (l : hyps) :=
   match nth_hyps i l with
   | EqTerm (Tint Nul) b =>
-      if (Nul =? 0) &&
-         (scalar_mult_add body k1 k2 =? b)%term &&
-         (0 <? k2) &&
-         (k2 <? k1)
-      then absurd
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (Nul =? 0) && (0 <? c) && (c <? k) then absurd
       else l
+    | None => l
+    end
   | _ => l
   end.
 
-Theorem not_exact_divide_valid :
- forall (i : nat)(k1 k2 : int) (body : term),
- valid_hyps (not_exact_divide i k1 k2 body).
+Theorem not_exact_divide_valid i k :
+ valid_hyps (not_exact_divide i k).
 Proof.
  unfold valid_hyps, not_exact_divide; intros.
- generalize (nth_valid ep e i lp); Simplify.
- rewrite <-H1, scalar_mult_add_stable. simpl.
- intros.
- absurd (interp_term e body * k1 + k2 = 0).
- - now apply OMEGA4.
- - symmetry; auto.
+ generalize (nth_valid ep e i lp).
+ destruct (nth_hyps i lp); simpl; auto.
+ destruct t0; auto.
+ destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto.
+ Simplify.
+ assert (k <> 0).
+ { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
+ apply (scalar_div_stable e) in E; auto. simpl in E.
+ intros H'; rewrite <- H' in E; auto.
+ exfalso. revert E. now apply OMEGA4.
 Qed.
 
 (** Now, the steps generating a new equation. *)
 
-(** [O_EXACT_DIVIDE] *)
+(** [O_DIVIDE] *)
 
-Definition exact_divide (k : int) (body : term) (prop : proposition) :=
+Definition divide (k : int) (prop : proposition) :=
   match prop with
   | EqTerm (Tint o) b =>
-    if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0)
-    then EqTerm (Tint 0) body
-    else TrueTerm
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (c =? 0) && negb (k =? 0)
+      then EqTerm (Tint 0) body
+      else TrueTerm
+    | None => TrueTerm
+    end
   | NeqTerm (Tint o) b =>
-    if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0)
-    then NeqTerm (Tint 0) body
-    else TrueTerm
-  | _ => TrueTerm
-  end.
-
-Theorem exact_divide_valid :
- forall (k : int) (t : term), valid1 (exact_divide k t).
-Proof.
- unfold valid1, exact_divide; intros k t ep e p1;
- Simplify; simpl; auto; subst;
- rewrite scalar_mult_stable; simpl; intros.
- - destruct (mult_integral _ _ (eq_sym H0)); intuition.
- - contradict H0; rewrite <- H0, mult_0_l; auto.
-Qed.
-
-(** [O_DIV_APPROX] *)
-
-Definition divide_and_approx (k1 k2 : int) (body : term)
-  (prop : proposition) :=
-  match prop with
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (c =? 0) && negb (k =? 0)
+      then NeqTerm (Tint 0) body
+      else TrueTerm
+    | None => TrueTerm
+    end
   | LeqTerm (Tint o) b =>
-      if (o =? 0) &&
-         (scalar_mult_add body k1 k2 =? b)%term &&
-         (0 <? k1) &&
-         (k2 <? k1)
+    match scalar_div b k with
+    | Some (body,c) =>
+      if (o =? 0) && (0 <? k) && (c <? k)
       then LeqTerm (Tint 0) body
       else prop
-  | _ => prop
+    | None => prop
+    end
+  | _ => TrueTerm
   end.
 
-Theorem divide_and_approx_valid :
- forall (k1 k2 : int) (body : term),
- valid1 (divide_and_approx k1 k2 body).
+Theorem divide_valid k : valid1 (divide k).
 Proof.
- unfold valid1, divide_and_approx.
- intros k1 k2 body ep e p1. Simplify. subst.
- rewrite scalar_mult_add_stable. simpl.
- intro H; now apply mult_le_approx with (3 := H).
+ unfold valid1, divide; intros ep e p;
+ destruct p; simpl; auto;
+ destruct t0; simpl; auto;
+ destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto.
+ - apply (scalar_div_stable e) in E; auto. simpl in E.
+   intros H'; rewrite <- H' in E. rewrite plus_0_r in E.
+   apply mult_integral in E. intuition.
+ - apply (scalar_div_stable e) in E; auto. simpl in E.
+   intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E.
+ - assert (k <> 0).
+   { intro. apply (lt_not_eq 0 k); eauto using lt_trans. }
+   apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E.
+   intro H'. now apply mult_le_approx with (3 := H').
 Qed.
 
 (** [O_SUM]. Invariant: [k1] and [k2] non-nul. *)
@@ -1591,12 +1648,9 @@ Qed.
 Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps :=
   match t with
   | O_BAD_CONSTANT i => singleton (bad_constant i l)
-  | O_NOT_EXACT_DIVIDE i k1 k2 body =>
-      singleton (not_exact_divide i k1 k2 body l)
-  | O_EXACT_DIVIDE n k body cont =>
-      execute_omega cont (apply_oper_1 n (exact_divide k body) l)
-  | O_DIV_APPROX n k1 k2 body cont =>
-      execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body) l)
+  | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l)
+  | O_DIVIDE i k cont =>
+      execute_omega cont (apply_oper_1 i (divide k) l)
   | O_SUM k1 i1 k2 i2 cont =>
       execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l)
   | O_MERGE_EQ i1 i2 cont =>
@@ -1610,14 +1664,10 @@ 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)
-        (exact_divide_valid k body) ep e lp H).
- - intros m k1 k2 body t' Ht' ep e lp H; apply Ht';
+ - intros m k t' Ht' ep e lp H; apply Ht';
     apply
-     (apply_oper_1_valid m (divide_and_approx k1 k2 body)
-        (divide_and_approx_valid k1 k2 body) ep e lp H).
+     (apply_oper_1_valid m (divide k)
+        (divide_valid k) ep e lp H).
  - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht';
     apply
      (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index ce47ef16a..a10ce68b4 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -102,9 +102,8 @@ let coq_p_imp = lazy (constant  "Timp")
 let coq_p_prop = lazy (constant  "Tprop")
 
 let coq_s_bad_constant = lazy (constant  "O_BAD_CONSTANT")
-let coq_s_div_approx = lazy (constant  "O_DIV_APPROX")
+let coq_s_divide = lazy (constant  "O_DIVIDE")
 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_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 b4599c831..ca23ed6c4 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -43,9 +43,8 @@ val coq_p_imp : Term.constr lazy_t
 val coq_p_prop : 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_divide : 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_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 6ef53837c..e56605076 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -365,23 +365,6 @@ let reified_of_proposition env f =
 let reified_of_eq env (l,r) =
   app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |]
 
-(* \subsection{Omega vers COQ réifié} *)
-
-let reified_of_omega env body constant =
-  let coeff_constant =
-    app coq_t_int [| Z.mk constant |] in
-  let mk_coeff {c;v} t =
-    let coef =
-      app coq_t_mult
-          [| reified_of_formula env (Oatom v);
-             app coq_t_int [| Z.mk c |] |] in
-    app coq_t_plus [|coef; t |] in
-  List.fold_right mk_coeff body coeff_constant
-
-let reified_of_omega env body c  =
-  try reified_of_omega env body c
-  with reraise -> display_eq display_omega_var (body,c); raise reraise
-
 (* \section{Opérations sur les équations}
 Ces fonctions préparent les traces utilisées par la tactique réfléchie
 pour faire des opérations de normalisation sur les équations.  *)
@@ -873,23 +856,12 @@ let rec reify_trace env env_hyp = function
   | CONTRADICTION (e1,e2) :: [] ->
      sum_bad false (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 |])
+            [| hyp_idx env_hyp e1.id; Z.mk k |])
+  | DIVIDE_AND_APPROX (e1,_,k,_) :: 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,
+     mkApp (Lazy.force coq_s_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,