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

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

1 files changed, 34 insertions, 71 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.