ROmega: less contructors in the final omega trace

 Now that O_SUM is properly optimized (cf. the [fusion] function),
 we could use it to encode CONTRADICTION and NEGATE_CONTRADICT(_INV).
 This way, the trace has almost the same size, but ReflOmegaCore.v
 is shorter and easier to maintain.

4 files changed, 13 insertions, 184 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 057752271..972070657 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -302,16 +302,6 @@ Module IntProperties (I:Int).
   intros; autorewrite with int; now rewrite plus_permute.
  Qed.
 
- Lemma OMEGA13 :
-  forall v l1 l2 x : int,
-  v * -x + l1 + (v * x + l2) = l1 + l2.
- Proof.
- intros; autorewrite with int.
- rewrite plus_permute; f_equal.
- rewrite plus_assoc.
- now rewrite <- mult_plus_distr_l, plus_opp_l, mult_comm, mult_0_l, plus_0_l.
- Qed.
-
  Lemma sum1 : forall a b c d : int, 0 = a -> 0 = b -> 0 = a * c + b * d.
  Proof.
  intros; elim H; elim H0; simpl; auto.
@@ -601,14 +591,6 @@ Module IntProperties (I:Int).
     now rewrite plus_opp_r.
  Qed.
 
- Lemma OMEGA2 : forall x y, 0 <= x -> 0 <= y -> 0 <= x + y.
- Proof.
- intros.
- replace 0 with (0+0).
- apply plus_le_compat; auto.
- rewrite plus_0_l; auto.
- Qed.
-
  Lemma OMEGA8 : forall x y, 0 <= x -> 0 <= y -> x = - y -> x = 0.
  Proof.
  intros.
@@ -1288,29 +1270,6 @@ Proof.
  - rewrite <- opp_eq_mult_neg_1. now f_equal.
 Qed.
 
-(** Fusion by cancellation.
-    Particular case of [fusion] where the final result should
-    be a constant. *)
-
-Fixpoint fusion_cancel (t1 t2 : term) : term :=
-  match t1, t2 with
-  | (v1 * Tint x1 + l1)%term, (v2 * Tint x2 + l2)%term =>
-    if eq_term v1 v2 && beq x1 (-x2)
-    then fusion_cancel l1 l2
-    else (t1+t2)%term (* should not happen *)
-  | Tint x1, Tint x2 => Tint (x1+x2)
-  | _, _ => (t1+t2)%term (* should not happen *)
-  end.
-
-Theorem fusion_cancel_stable e t1 t2 :
- interp_term e (t1+t2)%term = interp_term e (fusion_cancel t1 t2).
-Proof.
- revert t2. induction t1; destruct t2; simpl; Simplify; auto.
- simpl in *.
- rewrite <- IHt1_2.
- apply OMEGA13.
-Qed.
-
 (** ** Normalization of a proposition.
 
     The only basic facts left after normalization are
@@ -1456,15 +1415,6 @@ 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_CONTRADICTION i j] :
-     inequations i and j have a sum which is a negative constant.
-     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_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_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].
 
@@ -1491,9 +1441,6 @@ Definition idx := nat. (** Index of an hypothesis in the list *)
 
 Inductive t_omega : Set :=
   | 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
   | O_NOT_EXACT_DIVIDE : idx -> int -> int -> term -> t_omega
 
   | O_EXACT_DIVIDE : idx -> int -> term -> t_omega -> t_omega
@@ -1524,117 +1471,6 @@ Proof.
  rewrite gt_lt_iff in *. rewrite le_lt_iff. intuition.
 Qed.
 
-(** [O_CONTRADICTION] *)
-
-Definition contradiction (i j : nat) (l : hyps) :=
-  match nth_hyps i l with
-  | LeqTerm (Tint Nul) b1 =>
-      match nth_hyps j l with
-      | LeqTerm (Tint Nul') b2 =>
-          match fusion_cancel b1 b2 with
-          | Tint k => if beq Nul 0 && beq Nul' 0 && bgt 0 k
-                      then absurd
-                      else l
-          | _ => l
-          end
-      | _ => l
-      end
-  | _ => l
-  end.
-
-Theorem contradiction_valid (i j : nat) : valid_hyps (contradiction i j).
-Proof.
- unfold valid_hyps, contradiction; intros ep e l H.
- generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H).
- case (nth_hyps i l); trivial. intros t1 t2.
- case t1; trivial. clear t1; intros x1.
- case (nth_hyps j l); trivial. intros t3 t4.
- case t3; trivial. clear t3; intros x3.
- destruct fusion_cancel as [ t0 | | | | | ] eqn:E; trivial.
- change t0 with (interp_term e (Tint t0)).
- rewrite <- E, <- fusion_cancel_stable.
- Simplify.
- intros H1 H2.
- generalize (OMEGA2 _ _ H1 H2).
- rewrite gt_lt_iff in *; rewrite le_lt_iff. intuition.
-Qed.
-
-(** [O_NEGATE_CONTRADICT] *)
-
-Definition negate_contradict (i1 i2 : nat) (h : hyps) :=
-  match nth_hyps i1 h with
-  | EqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
-          then absurd
-          else h
-      | _ => h
-      end
-  | NeqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 && eq_term b1 b2
-          then absurd
-          else h
-      | _ => h
-      end
-  | _ => h
-  end.
-
-Theorem negate_contradict_valid :
- forall i j : nat, valid_hyps (negate_contradict i j).
-Proof.
- unfold valid_hyps, negate_contradict; intros i j ep e l H;
- generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1;
- auto; intros z; auto; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros; Simplify.
-Qed.
-
-(** [O_NEGATE_CONTRADICT_INV] *)
-
-Definition negate_contradict_inv (i1 i2 : nat) (h : hyps) :=
-  match nth_hyps i1 h with
-  | EqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | NeqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 &&
-             eq_term b1 (scalar_norm b2 (-(1)))
-          then absurd
-          else h
-      | _ => h
-      end
-  | NeqTerm (Tint Nul) b1 =>
-      match nth_hyps i2 h with
-      | EqTerm (Tint Nul') b2 =>
-          if beq Nul 0 && beq Nul' 0 &&
-             eq_term b1 (scalar_norm b2 (-(1)))
-          then absurd
-          else h
-      | _ => h
-      end
-  | _ => h
-  end.
-
-Theorem negate_contradict_inv_valid :
- forall i j : nat, valid_hyps (negate_contradict_inv i j).
-Proof.
- unfold valid_hyps, negate_contradict_inv; intros i j ep e l H;
- generalize (nth_valid _ _ i _ H) (nth_valid _ _ j _ H);
- case (nth_hyps i l); auto; intros t1 t2; case t1;
- auto; intros z; auto; case (nth_hyps j l);
- auto; intros t3 t4; case t3; auto; intros z';
- auto; simpl; intros H1 H2; Simplify.
- - rewrite <- scalar_norm_stable in H1; simpl in *;
-   elim (mult_integral (interp_term e t4) (-(1))); intuition;
-   elim minus_one_neq_zero; auto.
- - elim H1; clear H1;
-   rewrite <- scalar_norm_stable; simpl in *;
-   now rewrite <- H2, mult_0_l.
-Qed.
-
 (** [NOT_EXACT_DIVIDE] *)
 
 Definition not_exact_divide (i : nat) (k1 k2 : int) (body : term)
@@ -1852,13 +1688,9 @@ Qed.
 
 (** ** Replaying the resolution trace *)
 
-Fixpoint execute_omega (t : t_omega) (l : hyps) {struct t} : lhyps :=
+Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps :=
   match t with
   | 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 =>
-      singleton (negate_contradict_inv i j 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 =>
@@ -1879,9 +1711,6 @@ 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 bad_constant_valid.
- - intros; left; now apply contradiction_valid.
- - intros; left; now apply negate_contradict_valid.
- - intros; left; now apply negate_contradict_inv_valid.
  - intros; left; now apply not_exact_divide_valid.
 
  - intros m k body t' Ht' ep e lp H; apply Ht';
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index fa92903ba..6e2fa5ed3 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -107,11 +107,8 @@ 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_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_negate_contradict =lazy (constant  "O_NEGATE_CONTRADICT")
-let coq_s_negate_contradict_inv =lazy (constant  "O_NEGATE_CONTRADICT_INV")
 
 (* construction for the [extract_hyp] tactic *)
 let coq_direction = lazy  (constant  "direction")
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index ba8b097fe..b00525561 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -48,11 +48,8 @@ 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_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_negate_contradict : Term.constr lazy_t
-val coq_s_negate_contradict_inv : Term.constr lazy_t
 
 val coq_direction : Term.constr lazy_t
 val coq_d_left : Term.constr lazy_t
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 45b141f92..48e06a93e 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -862,19 +862,25 @@ let hyp_idx env_hyp i =
     | _ :: l -> loop (succ count) l
   in loop 0 env_hyp
 
+
+(* We now expand NEGATE_CONTRADICT and CONTRADICTION into
+   a O_SUM followed by a O_BAD_CONSTANT *)
+
+let sum_bad inv i1 i2 =
+  mkApp (Lazy.force coq_s_sum,
+         [| Z.mk Bigint.one; i1;
+            Z.mk (if inv then negone else Bigint.one); i2;
+            mkApp (Lazy.force coq_s_bad_constant, [| mk_nat 0 |])|])
+
 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 |])
+     sum_bad direct (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 |])
+     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