diff options
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 208 | ||||
| -rw-r--r-- | plugins/romega/const_omega.ml | 3 | ||||
| -rw-r--r-- | plugins/romega/const_omega.mli | 3 | ||||
| -rw-r--r-- | plugins/romega/refl_omega.ml | 34 |
4 files changed, 134 insertions, 114 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index f95cfe364..d242264a9 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -75,6 +75,18 @@ Module Type Int. (** Btw, lt_0_1 could be deduced from this last axiom *) + (** Now we also require a division function. + It is deliberately underspecified, since that's enough + for the proofs below. But the most appropriate variant + (and the one needed to stay in sync with the omega engine) + is "Floor" (the historical version of Coq's [Z.div]). *) + + Parameter diveucl : t -> t -> t * t. + Notation "i / j" := (fst (diveucl i j)). + Notation "i 'mod' j" := (snd (diveucl i j)). + Axiom diveucl_spec : + forall i j, j<>0 -> i = j * (i/j) + (i mod j). + End Int. @@ -133,6 +145,9 @@ Module Z_as_Int <: Int. Definition le_lt_int := Z.lt_le_pred. + Definition diveucl := Z.div_eucl. + Definition diveucl_spec := Z.div_mod. + End Z_as_Int. @@ -1124,6 +1139,50 @@ Proof. rewrite IHt2. simpl. apply plus_assoc. Qed. +(** Division by a constant + + All the non-constant coefficients should be exactly dividable *) + +Fixpoint scalar_div (t : term) (k : int) : option (term * int) := + match t with + | v * Tint x + l => + let (q,r) := diveucl x k in + if (r =? 0)%I then + match scalar_div l k with + | None => None + | Some (u,c) => Some (v * Tint q + u, c) + end + else None + | Tint x => + let (q,r) := diveucl x k in + Some (Tint q, r) + | _ => None + end%term. + +Lemma scalar_div_stable e t k u c : k<>0 -> + scalar_div t k = Some (u,c) -> + interp_term e (u * Tint k + Tint c) = interp_term e t. +Proof. + revert u c. + induction t; simpl; Simplify; try easy. + - intros u c Hk. assert (H := diveucl_spec t0 k Hk). + simpl in H. + destruct diveucl as (q,r). simpl in H. rewrite H. + injection 1 as <- <-. simpl. f_equal. apply mult_comm. + - intros u c Hk. + destruct t1; simpl; Simplify; try easy. + destruct t1_2; simpl; Simplify; try easy. + assert (H := diveucl_spec t0 k Hk). + simpl in H. + destruct diveucl as (q,r). simpl in H. rewrite H. + case beq_reflect; [intros -> | easy]. + destruct (scalar_div t2 k) as [(u',c')|] eqn:E; [|easy]. + injection 1 as <- ->. simpl. + rewrite <- (IHt2 u' c Hk); simpl; auto. + rewrite plus_0_r , (mult_comm k q). symmetry. apply OMEGA11. +Qed. + + (** Fusion of two equations. From two normalized equations, this fusion will produce @@ -1337,16 +1396,15 @@ 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_NOT_EXACT_DIVIDE i k1 k2 t] : - equation i has a body equivalent to [k1*t+k2] with [0<k2<k1]. + - [O_NOT_EXACT_DIVIDE i k] : + equation i can be factorized as some [k*t+c] with [0<c<k]. Now, the intermediate steps leading to a new hypothesis: - - [O_EXACT_DIVIDE i k1 t cont] : - (dis)equation i has a body equivalent to [k1*t] with [k1<>0], - we change it (in-place) for (dis)equation [0=t]. - - [O_DIV_APPROX i k1 k2 t cont] : - inequation i has a body equivalent to [k1*t+k2] with [0<k1] - and [k2<k1], we change it (in-place) for inequation [0<=t]. + - [O_DIVIDE i k cont] : + the body of hypothesis i could be factorized as [k*t+c] + with either [k<>0] and [c=0] for a (dis)equation, or + [0<k] and [c<k] for an inequation. We change in-place the + body of i for [t]. - [O_SUM k1 i1 k2 i2 cont] : creates a new hypothesis whose kind depends on the kind of hypotheses [i1] and [i2], and whose body is [k1*body(i1) + k2*body(i2)]. Depending of the @@ -1362,10 +1420,9 @@ Definition idx := nat. (** Index of an hypothesis in the list *) Inductive t_omega : Set := | O_BAD_CONSTANT : idx -> t_omega - | O_NOT_EXACT_DIVIDE : idx -> int -> int -> term -> t_omega + | O_NOT_EXACT_DIVIDE : idx -> int -> t_omega - | O_EXACT_DIVIDE : idx -> int -> term -> t_omega -> t_omega - | O_DIV_APPROX : idx -> int -> int -> term -> t_omega -> t_omega + | O_DIVIDE : idx -> int -> 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. @@ -1391,84 +1448,84 @@ Proof. rewrite le_lt_iff. intuition. Qed. -(** [NOT_EXACT_DIVIDE] *) +(** [O_NOT_EXACT_DIVIDE] *) -Definition not_exact_divide (i : nat) (k1 k2 : int) (body : term) - (l : hyps) := +Definition not_exact_divide (i : nat) (k : int) (l : hyps) := match nth_hyps i l with | EqTerm (Tint Nul) b => - if (Nul =? 0) && - (scalar_mult_add body k1 k2 =? b)%term && - (0 <? k2) && - (k2 <? k1) - then absurd + match scalar_div b k with + | Some (body,c) => + if (Nul =? 0) && (0 <? c) && (c <? k) then absurd else l + | None => l + end | _ => l end. -Theorem not_exact_divide_valid : - forall (i : nat)(k1 k2 : int) (body : term), - valid_hyps (not_exact_divide i k1 k2 body). +Theorem not_exact_divide_valid i k : + valid_hyps (not_exact_divide i k). Proof. unfold valid_hyps, not_exact_divide; intros. - generalize (nth_valid ep e i lp); Simplify. - rewrite <-H1, scalar_mult_add_stable. simpl. - intros. - absurd (interp_term e body * k1 + k2 = 0). - - now apply OMEGA4. - - symmetry; auto. + generalize (nth_valid ep e i lp). + destruct (nth_hyps i lp); simpl; auto. + destruct t0; auto. + destruct (scalar_div t1 k) as [(body,c)|] eqn:E; auto. + Simplify. + assert (k <> 0). + { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } + apply (scalar_div_stable e) in E; auto. simpl in E. + intros H'; rewrite <- H' in E; auto. + exfalso. revert E. now apply OMEGA4. Qed. (** Now, the steps generating a new equation. *) -(** [O_EXACT_DIVIDE] *) +(** [O_DIVIDE] *) -Definition exact_divide (k : int) (body : term) (prop : proposition) := +Definition divide (k : int) (prop : proposition) := match prop with | EqTerm (Tint o) b => - if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0) - then EqTerm (Tint 0) body - else TrueTerm + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (c =? 0) && negb (k =? 0) + then EqTerm (Tint 0) body + else TrueTerm + | None => TrueTerm + end | NeqTerm (Tint o) b => - if (o =? 0) && (scalar_mult body k =? b)%term && negb (k =? 0) - then NeqTerm (Tint 0) body - else TrueTerm - | _ => TrueTerm - end. - -Theorem exact_divide_valid : - forall (k : int) (t : term), valid1 (exact_divide k t). -Proof. - unfold valid1, exact_divide; intros k t ep e p1; - Simplify; simpl; auto; subst; - rewrite scalar_mult_stable; simpl; intros. - - destruct (mult_integral _ _ (eq_sym H0)); intuition. - - contradict H0; rewrite <- H0, mult_0_l; auto. -Qed. - -(** [O_DIV_APPROX] *) - -Definition divide_and_approx (k1 k2 : int) (body : term) - (prop : proposition) := - match prop with + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (c =? 0) && negb (k =? 0) + then NeqTerm (Tint 0) body + else TrueTerm + | None => TrueTerm + end | LeqTerm (Tint o) b => - if (o =? 0) && - (scalar_mult_add body k1 k2 =? b)%term && - (0 <? k1) && - (k2 <? k1) + match scalar_div b k with + | Some (body,c) => + if (o =? 0) && (0 <? k) && (c <? k) then LeqTerm (Tint 0) body else prop - | _ => prop + | None => prop + end + | _ => TrueTerm end. -Theorem divide_and_approx_valid : - forall (k1 k2 : int) (body : term), - valid1 (divide_and_approx k1 k2 body). +Theorem divide_valid k : valid1 (divide k). Proof. - unfold valid1, divide_and_approx. - intros k1 k2 body ep e p1. Simplify. subst. - rewrite scalar_mult_add_stable. simpl. - intro H; now apply mult_le_approx with (3 := H). + unfold valid1, divide; intros ep e p; + destruct p; simpl; auto; + destruct t0; simpl; auto; + destruct scalar_div as [(body,c)|] eqn:E; simpl; Simplify; auto. + - apply (scalar_div_stable e) in E; auto. simpl in E. + intros H'; rewrite <- H' in E. rewrite plus_0_r in E. + apply mult_integral in E. intuition. + - apply (scalar_div_stable e) in E; auto. simpl in E. + intros H' H''. now rewrite <- H'', mult_0_l, plus_0_l in E. + - assert (k <> 0). + { intro. apply (lt_not_eq 0 k); eauto using lt_trans. } + apply (scalar_div_stable e) in E; auto. simpl in E. rewrite <- E. + intro H'. now apply mult_le_approx with (3 := H'). Qed. (** [O_SUM]. Invariant: [k1] and [k2] non-nul. *) @@ -1591,12 +1648,9 @@ Qed. Fixpoint execute_omega (t : t_omega) (l : hyps) : lhyps := match t with | O_BAD_CONSTANT i => singleton (bad_constant i 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 => - execute_omega cont (apply_oper_1 n (exact_divide k body) l) - | O_DIV_APPROX n k1 k2 body cont => - execute_omega cont (apply_oper_1 n (divide_and_approx k1 k2 body) l) + | O_NOT_EXACT_DIVIDE i k => singleton (not_exact_divide i k l) + | O_DIVIDE i k cont => + execute_omega cont (apply_oper_1 i (divide k) l) | O_SUM k1 i1 k2 i2 cont => execute_omega cont (apply_oper_2 i1 i2 (sum k1 k2) l) | O_MERGE_EQ i1 i2 cont => @@ -1610,14 +1664,10 @@ 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) - (exact_divide_valid k body) ep e lp H). - - intros m k1 k2 body t' Ht' ep e lp H; apply Ht'; + - intros m k t' Ht' ep e lp H; apply Ht'; apply - (apply_oper_1_valid m (divide_and_approx k1 k2 body) - (divide_and_approx_valid k1 k2 body) ep e lp H). + (apply_oper_1_valid m (divide k) + (divide_valid k) ep e lp H). - intros k1 i1 k2 i2 t' Ht' ep e lp H; apply Ht'; apply (apply_oper_2_valid i1 i2 (sum k1 k2) (sum_valid k1 k2) ep e diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index ce47ef16a..a10ce68b4 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -102,9 +102,8 @@ let coq_p_imp = lazy (constant "Timp") let coq_p_prop = lazy (constant "Tprop") let coq_s_bad_constant = lazy (constant "O_BAD_CONSTANT") -let coq_s_div_approx = lazy (constant "O_DIV_APPROX") +let coq_s_divide = lazy (constant "O_DIVIDE") 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_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 b4599c831..ca23ed6c4 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -43,9 +43,8 @@ val coq_p_imp : Term.constr lazy_t val coq_p_prop : Term.constr lazy_t val coq_s_bad_constant : Term.constr lazy_t -val coq_s_div_approx : Term.constr lazy_t +val coq_s_divide : 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_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 6ef53837c..e56605076 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -365,23 +365,6 @@ let reified_of_proposition env f = let reified_of_eq env (l,r) = app coq_p_eq [| reified_of_formula env l; reified_of_formula env r |] -(* \subsection{Omega vers COQ réifié} *) - -let reified_of_omega env body constant = - let coeff_constant = - app coq_t_int [| Z.mk constant |] in - let mk_coeff {c;v} t = - let coef = - app coq_t_mult - [| reified_of_formula env (Oatom v); - app coq_t_int [| Z.mk c |] |] in - app coq_t_plus [|coef; t |] in - List.fold_right mk_coeff body coeff_constant - -let reified_of_omega env body c = - try reified_of_omega env body c - with reraise -> display_eq display_omega_var (body,c); raise reraise - (* \section{Opérations sur les équations} Ces fonctions préparent les traces utilisées par la tactique réfléchie pour faire des opérations de normalisation sur les équations. *) @@ -873,23 +856,12 @@ let rec reify_trace env env_hyp = function | CONTRADICTION (e1,e2) :: [] -> 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 - let e2_body = map_eq_linear (fun c -> c / k) e1.body in mkApp (Lazy.force coq_s_not_exact_divide, - [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d; - reified_of_omega env e2_body e2_constant |]) - | DIVIDE_AND_APPROX (e1,e2,k,d) :: l -> - mkApp (Lazy.force coq_s_div_approx, - [| hyp_idx env_hyp e1.id; Z.mk k; Z.mk d; - reified_of_omega env e2.body e2.constant; - reify_trace env env_hyp l |]) + [| hyp_idx env_hyp e1.id; Z.mk k |]) + | DIVIDE_AND_APPROX (e1,_,k,_) :: l | EXACT_DIVIDE (e1,k) :: l -> - let e2_body = map_eq_linear (fun c -> c / k) e1.body in - let e2_constant = floor_div e1.constant k in - mkApp (Lazy.force coq_s_exact_divide, + mkApp (Lazy.force coq_s_divide, [| hyp_idx env_hyp e1.id; Z.mk k; - reified_of_omega env e2_body e2_constant; reify_trace env env_hyp l |]) | MERGE_EQ(e3,e1,e2) :: l -> mkApp (Lazy.force coq_s_merge_eq, |