romega: discard constructor D_mono (shorter trace + fix a bug)

 For the bug, see new test test_romega10 in test-suite/success/ROmega0.v.

4 files changed, 40 insertions, 79 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 60c0018c5..1d24c8c21 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -935,6 +935,7 @@ Inductive t_omega : Set :=
 (* \subsubsection{Rules for normalizing the hypothesis} *)
 (* These rules indicate how to normalize useful propositions
    of each useful hypothesis before the decomposition of hypothesis.
+   Negation nodes could be traversed by either [P_LEFT] or [P_RIGHT].
    The rules include the inversion phase for negation removal. *)
 
 Inductive p_step : Set :=
@@ -955,13 +956,12 @@ Inductive h_step : Set :=
 (* \subsubsection{Rules for decomposing the hypothesis} *)
 (* This type allows navigation in the logical constructors that
    form the predicats of the hypothesis in order to decompose them.
-   This allows in particular to extract one hypothesis from a
-   conjunction with possibly the right level of negations. *)
+   This allows in particular to extract one hypothesis from a conjunction.
+   NB: negations are silently traversed. *)
 
 Inductive direction : Set :=
   | D_left : direction
-  | D_right : direction
-  | D_mono : direction.
+  | D_right : direction.
 
 (* This type allows extracting useful components from hypothesis, either
    hypothesis generated by splitting a disjonction, or equations.
@@ -2841,77 +2841,42 @@ Proof.
  intros; apply valid_goal with (2 := H); apply normalize_hyps_valid.
 Qed.
 
-Fixpoint extract_hyp_pos (s : list direction) (p : proposition) {struct s} :
+Fixpoint extract_hyp_pos (s : list direction) (p : proposition) :
  proposition :=
-  match s with
-  | D_left :: l =>
-      match p with
-      | Tand x y => extract_hyp_pos l x
-      | _ => p
-      end
-  | D_right :: l =>
-      match p with
-      | Tand x y => extract_hyp_pos l y
-      | _ => p
-      end
-  | D_mono :: l => match p with
-                   | Tnot x => extract_hyp_neg l x
-                   | _ => p
-                   end
-  | _ => p
+  match p, s with
+  | Tand x y, D_left :: l => extract_hyp_pos l x
+  | Tand x y, D_right :: l => extract_hyp_pos l y
+  | Tnot x, _ => extract_hyp_neg s x
+  | _, _ => p
   end
 
- with extract_hyp_neg (s : list direction) (p : proposition) {struct s} :
+ with extract_hyp_neg (s : list direction) (p : proposition) :
  proposition :=
-  match s with
-  | D_left :: l =>
-      match p with
-      | Tor x y => extract_hyp_neg l x
-      | Timp x y => if decidability x then extract_hyp_pos l x else Tnot p
-      | _ => Tnot p
-      end
-  | D_right :: l =>
-      match p with
-      | Tor x y => extract_hyp_neg l y
-      | Timp x y => extract_hyp_neg l y
-      | _ => Tnot p
-      end
-  | D_mono :: l =>
-      match p with
-      | Tnot x => if decidability x then extract_hyp_pos l x else Tnot p
-      | _ => Tnot p
-      end
-  | _ =>
-      match p with
-      | Tnot x => if decidability x then x else Tnot p
-      | _ => Tnot p
-      end
+  match p, s with
+  | Tor x y, D_left :: l => extract_hyp_neg l x
+  | Tor x y, D_right :: l => extract_hyp_neg l y
+  | Timp x y, D_left :: l =>
+    if decidability x then extract_hyp_pos l x else Tnot p
+  | Timp x y, D_right :: l => extract_hyp_neg l y
+  | Tnot x, _ => if decidability x then extract_hyp_pos s x else Tnot p
+  | _, _ => Tnot p
   end.
 
-Definition co_valid1 (f : proposition -> proposition) :=
-  forall (ep : list Prop) (e : list int) (p1 : proposition),
-  interp_proposition ep e (Tnot p1) -> interp_proposition ep e (f p1).
-
 Theorem extract_valid :
  forall s : list direction,
- valid1 (extract_hyp_pos s) /\ co_valid1 (extract_hyp_neg s).
-Proof.
- unfold valid1, co_valid1; simple induction s.
- - split.
-   + simpl; auto.
-   + intros ep e p1; case p1; simpl; auto; intro p.
-     destruct decidability eqn:H.
-     * generalize (decidable_correct ep e p H);
-       unfold decidable; tauto.
-     * simpl; auto.
- - intros a s' (H1, H2); simpl in H2; split; intros ep e p; case a; auto;
-   case p; auto; simpl; intros;
-    (apply H1; tauto) ||
-      (apply H2; tauto) ||
-        (destruct decidability eqn:H3; try tauto;
-         generalize (decidable_correct ep e p0 H3);
-         unfold decidable; intro H4; apply H1;
-         tauto).
+ valid1 (extract_hyp_pos s).
+Proof.
+ assert (forall p s ep e,
+         (interp_proposition ep e p ->
+          interp_proposition ep e (extract_hyp_pos s p)) /\
+         (interp_proposition ep e (Tnot p) ->
+          interp_proposition ep e (extract_hyp_neg s p))).
+ { induction p; destruct s; simpl; auto; split; try destruct d; try easy;
+   intros; (apply IHp || apply IHp1 || apply IHp2 || idtac); simpl; try tauto;
+   destruct decidability eqn:D; intros; auto;
+   pose proof (decidable_correct ep e _ D); unfold decidable in *;
+   (apply IHp || apply IHp1); tauto. }
+ red. intros. now apply H.
 Qed.
 
 Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
@@ -2960,11 +2925,9 @@ Proof.
              - right; apply H0; simpl; tauto.
              - left; apply H; simpl; tauto. }
           { simpl; auto. }
-    + elim (extract_valid l); intros H2 H3.
-      apply H2, nth_valid; auto.
+    + apply extract_valid, nth_valid; auto.
  - intros; apply H; simpl; split; auto.
-   elim (extract_valid l); intros H2 H3.
-   apply H2; apply nth_valid; auto.
+   apply extract_valid, nth_valid; auto.
  - apply omega_valid with (1 := H).
 Qed.
 
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 8d7ae51fc..cf5d20aeb 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -165,7 +165,6 @@ let coq_s_negate_contradict_inv =lazy (constant  "O_NEGATE_CONTRADICT_INV")
 let coq_direction = lazy  (constant  "direction")
 let coq_d_left = lazy  (constant  "D_left")
 let coq_d_right = lazy  (constant  "D_right")
-let coq_d_mono = lazy  (constant  "D_mono")
 
 let coq_e_split = lazy  (constant  "E_SPLIT")
 let coq_e_extract = lazy  (constant  "E_EXTRACT")
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index ee7ff451a..1c67af806 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -99,7 +99,6 @@ 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
 val coq_d_right : Term.constr lazy_t
-val coq_d_mono : Term.constr lazy_t
 
 val coq_e_split : Term.constr lazy_t
 val coq_e_extract : Term.constr lazy_t
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index bb4ab37ff..af396d489 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1029,8 +1029,11 @@ let find_path {o_hyp=id;o_path=p} env =
 
 let mk_direction_list l =
   let trans = function
-      O_left -> coq_d_left | O_right -> coq_d_right | O_mono -> coq_d_mono in
-  mk_list (Lazy.force coq_direction) (List.map (fun d-> Lazy.force(trans d)) l)
+    | O_left -> Some (Lazy.force coq_d_left)
+    | O_right -> Some (Lazy.force coq_d_right)
+    | O_mono -> None (* No more [D_mono] constructor now *)
+  in
+  mk_list (Lazy.force coq_direction) (List.map_filter trans l)
 
 
 (* \section{Rejouer l'historique} *)
@@ -1156,13 +1159,10 @@ and decompose_tree_hyps trace env ctxt = function
         with Not_found ->
 	  failwith (Printf.sprintf "Cannot find equation %d" i) in
       let (index,path) = find_path equation.e_origin ctxt in
-      let full_path = if equation.e_negated then path @ [O_mono] else path in
       let cont =
 	decompose_tree_hyps trace env
 	   (CCEqua equation.e_omega.id :: ctxt) l in
-      app coq_e_extract [|mk_nat index;
-			  mk_direction_list full_path;
-			  cont |]
+      app coq_e_extract [|mk_nat index; mk_direction_list path; cont |]
 
 (* \section{La fonction principale} *)
  (* Cette fonction construit la