From d992ae9fc539bdadd9214d2c92d83bd08b68ef33 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 17 May 2017 15:22:49 +0200 Subject: ROmega : O_STATE turned into a O_SUM We benefit from the fact that we normalize now *all* hypotheses even the one defining the "stated" variable: it is produced as ...def of v... = v and normalized as -v + ...def of v... = 0 which is precisely what we should add to the initial equation during a O_STATE. --- plugins/romega/ReflOmegaCore.v | 39 ++++++------------------------------- plugins/romega/const_omega.ml | 1 - plugins/romega/const_omega.mli | 1 - plugins/romega/refl_omega.ml | 44 +++++++++++++++++++----------------------- 4 files changed, 26 insertions(+), 59 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 972070657..f08d62162 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -1175,7 +1175,11 @@ Proof. symmetry. apply plus_0_r. Qed. -(** Adding a constant *) +(** Adding a constant + + Instead of using [scalar_norm_add t 1 k], the following + definition spares some computations. + *) Fixpoint add_norm (t : term) (k : int) : term := match t with @@ -1434,7 +1438,6 @@ Qed. with one these bodies. - [O_SPLIT_INEQ i cont1 cont2] : disequation i is split into a disjonction of inequations. - - [O_STATE k i j cont] : now shortcut for [O_SUM 1 i k j cont]. *) Definition idx := nat. (** Index of an hypothesis in the list *) @@ -1447,8 +1450,7 @@ Inductive t_omega : Set := | O_DIV_APPROX : idx -> int -> int -> term -> 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 - | O_STATE : int -> idx -> idx -> t_omega -> t_omega. + | O_SPLIT_INEQ : idx -> t_omega -> t_omega -> t_omega. (** ** Actual resolution steps of an omega normalized goal *) @@ -1662,30 +1664,6 @@ Proof. symmetry ; trivial. Qed. - -(** [O_STATE] *) - -Definition state (m : int) (prop1 prop2 : proposition) := - match prop1 with - | EqTerm (Tint Null) b1 => - match prop2 with - | EqTerm (Tint Null') b2 => - if beq Null 0 && beq Null' 0 - then EqTerm (Tint 0) (fusion b1 b2 1 m) - else TrueTerm - | _ => TrueTerm - end - | _ => TrueTerm - end. - -Theorem state_valid : forall (m : int), valid2 (state m). -Proof. - unfold valid2; intros m ep e p1 p2. - unfold state; Simplify; simpl; auto. - rewrite <- fusion_stable. simpl in *. intros H H'. - rewrite <- H, <- H'. now rewrite !mult_0_l, plus_0_l. -Qed. - (** ** Replaying the resolution trace *) Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := @@ -1703,8 +1681,6 @@ Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := execute_omega cont (apply_oper_2 i1 i2 merge_eq l) | O_SPLIT_INEQ i cont1 cont2 => split_ineq i (execute_omega cont1) (execute_omega cont2) l - | O_STATE m i1 i2 cont => - execute_omega cont (apply_oper_2 i1 i2 (state m) l) end. Theorem omega_valid : forall tr : t_omega, valid_list_hyps (execute_omega tr). @@ -1712,7 +1688,6 @@ 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) @@ -1733,8 +1708,6 @@ Proof. apply (split_ineq_valid i (execute_omega k1) (execute_omega k2) H1 H2 ep e lp H). - - intros m i1 i2 t' Ht' ep e lp H; apply Ht'; - apply (apply_oper_2_valid i1 i2 (state m) (state_valid m) ep e lp H). Qed. diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 6e2fa5ed3..ce47ef16a 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -106,7 +106,6 @@ let coq_s_div_approx = lazy (constant "O_DIV_APPROX") 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_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 b00525561..b4599c831 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -47,7 +47,6 @@ val coq_s_div_approx : 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_state : 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 48e06a93e..95cf2083c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -214,17 +214,15 @@ let new_omega_var, rst_omega_var = let display_omega_var i = Printf.sprintf "OV%d" i -(* Register a new internal variable corresponding to some oformula - (normally an [Oatom]). *) - -let add_omega_var env t = - let v = new_omega_var () in - env.om_vars <- (v,t) :: env.om_vars - -(* Ajout forcé d'un lien entre un terme et une variable Cas où la - variable est créée par Omega et où il faut la lier après coup à un atome - réifié introduit de force *) -let force_omega_var env t v = +(* Register an internal variable corresponding to some oformula + (normally an [Oatom]). This omega variable could be a new one, + or one already created during the omega resolution (cf. STATE). *) + +let add_omega_var env t ov = + let v = match ov with + | None -> new_omega_var () + | Some v -> v + in env.om_vars <- (v,t) :: env.om_vars (* Récupère le terme associé à une variable omega *) @@ -238,12 +236,12 @@ let unintern_omega env v = l'environnement initial contenant tout. Il faudra le réduire après calcul des variables utiles. *) -let add_reified_atom sync t env = +let add_reified_atom opt_omega_var t env = try List.index0 Term.eq_constr t env.terms with Not_found -> let i = List.length env.terms in (* synchronize atom indexes and omega variables *) - let () = if sync then add_omega_var env (Oatom i) in + add_omega_var env (Oatom i) opt_omega_var; env.terms <- env.terms @ [t]; i let get_reified_atom env = @@ -514,11 +512,11 @@ let rec oformula_of_constr env t = | None -> match Z.get_scalar t2 with | Some n -> Omult (oformula_of_constr env t1, Oint n) - | None -> Oatom (add_reified_atom true t env)) + | None -> Oatom (add_reified_atom None t env)) | Topp t -> Oopp(oformula_of_constr env t) | Tsucc t -> Oplus(oformula_of_constr env t, Oint one) | Tnum n -> Oint n - | Tother -> Oatom (add_reified_atom true t env) + | Tother -> Oatom (add_reified_atom None t env) and binop env c t1 t2 = let t1' = oformula_of_constr env t1 in @@ -713,14 +711,12 @@ let add_stated_equations env tree = (* Notez que si l'ordre de création des variables n'est pas respecté, * ca va planter *) let coq_v = coq_of_formula env v_def in - let v = add_reified_atom false coq_v env in + let v = add_reified_atom (Some st.st_var) coq_v env in (* Le terme qu'il va falloir introduire *) let term_to_generalize = app coq_refl_equal [|Lazy.force Z.typ; coq_v|] in (* sa représentation sous forme d'équation mais non réifié car on n'a pas * l'environnement pour le faire correctement *) let term_to_reify = (v_def,Oatom v) in - (* enregistre le lien entre la variable omega et la variable Coq *) - force_omega_var env (Oatom v) st.st_var; (v, term_to_generalize,term_to_reify,st.st_def.id) in List.map add_env stated_equations @@ -909,12 +905,12 @@ let rec reify_trace env env_hyp = function [| Z.mk k1; hyp_idx env_hyp e1.id; Z.mk k2; hyp_idx env_hyp e2.id; reify_trace env (CCEqua e3 :: env_hyp) l |]) - | STATE {st_new_eq=new_eq; st_def =def; - st_orig=orig; st_coef=m; - st_var=sigma } :: l -> - mkApp (Lazy.force coq_s_state, - [| Z.mk m; hyp_idx env_hyp orig.id; hyp_idx env_hyp def.id; - reify_trace env (CCEqua new_eq.id :: env_hyp) l |]) + | STATE {st_new_eq; st_def; st_orig; st_coef } :: l -> + (* we now produce a [O_SUM] here *) + mkApp (Lazy.force coq_s_sum, + [| Z.mk Bigint.one; hyp_idx env_hyp st_orig.id; + Z.mk st_coef; hyp_idx env_hyp st_def.id; + reify_trace env (CCEqua st_new_eq.id :: env_hyp) l |]) | HYP _ :: l -> reify_trace env env_hyp l | SPLIT_INEQ(e,(e1,l1),(e2,l2)) :: _ -> let r1 = reify_trace env (CCEqua e1 :: env_hyp) l1 in -- cgit v1.2.3