diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 105 | ||||
| -rw-r--r-- | plugins/romega/const_omega.ml | 1 | ||||
| -rw-r--r-- | plugins/romega/const_omega.mli | 1 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 12 |
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 |