diff options
-rw-r--r-- | plugins/omega/coq_omega.ml | 44 | ||||
-rw-r--r-- | test-suite/bugs/closed/4132.v | 31 |
2 files changed, 68 insertions, 7 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d625e3076..cefd48538 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -666,6 +666,36 @@ let clever_rewrite p vpath t gl = let t' = applist(t, (vargs @ [abstracted])) in exact (applist(t',[mkNewMeta()])) gl +(** simpl_coeffs : + The subterm at location [path_init] in the current goal should + look like [(v1*c1 + (v2*c2 + ... (vn*cn + k)))], and we reduce + via "simpl" each [ci] and the final constant [k]. + The path [path_k] gives the location of constant [k]. + Earlier, the whole was a mere call to [focused_simpl], + leading to reduction inside the atoms [vi], which is bad, + for instance when the atom is an evaluable definition + (see #4132). *) + +let simpl_coeffs path_init path_k gl = + let rec loop n t = + if Int.equal n 0 then pf_nf gl t + else + (* t should be of the form ((v * c) + ...) *) + match kind_of_term t with + | App(f,[|t1;t2|]) -> + (match kind_of_term t1 with + | App (g,[|v;c|]) -> + let c' = pf_nf gl c in + let t2' = loop (pred n) t2 in + mkApp (f,[|mkApp (g,[|v;c'|]);t2'|]) + | _ -> assert false) + | _ -> assert false + in + let n = Pervasives.(-) (List.length path_k) (List.length path_init) in + let newc = context (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) + in + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl + let rec shuffle p (t1,t2) = match t1,t2 with | Oplus(l1,r1), Oplus(l2,r2) -> @@ -728,7 +758,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = let tac' = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -763,7 +793,7 @@ let shuffle_mult p_init k1 e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -786,7 +816,7 @@ let shuffle_mult_right p_init e1 k2 e2 = clever_rewrite p [[P_APP 1;P_APP 1];[P_APP 2]] (Lazy.force coq_fast_Zred_factor5) in - tac :: focused_simpl (P_APP 1::P_APP 2:: p) :: tac' :: + tac :: focused_simpl (P_APP 2::P_APP 1:: p) :: tac' :: loop p (l1,l2) else tac :: loop (P_APP 2 :: p) (l1,l2) else if v1 > v2 then @@ -813,7 +843,7 @@ let shuffle_mult_right p_init e1 k2 e2 = [P_APP 2; P_APP 2]] (Lazy.force coq_fast_OMEGA12) :: loop (P_APP 2 :: p) ([],l2) - | [],[] -> [focused_simpl p_init] + | [],[] -> [simpl_coeffs p_init p] in loop p_init (e1,e2) @@ -854,7 +884,7 @@ let rec scalar p n = function let scalar_norm p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | (_::l) -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1];[P_APP 1; P_APP 1; P_APP 2]; @@ -865,7 +895,7 @@ let scalar_norm p_init = let norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _:: l -> clever_rewrite p [[P_APP 1;P_APP 1]; [P_APP 1; P_APP 2];[P_APP 2]] (Lazy.force coq_fast_Zplus_assoc_reverse) :: @@ -875,7 +905,7 @@ let norm_add p_init = let scalar_norm_add p_init = let rec loop p = function - | [] -> [focused_simpl p_init] + | [] -> [simpl_coeffs p_init p] | _ :: l -> clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1]; diff --git a/test-suite/bugs/closed/4132.v b/test-suite/bugs/closed/4132.v new file mode 100644 index 000000000..806ffb771 --- /dev/null +++ b/test-suite/bugs/closed/4132.v @@ -0,0 +1,31 @@ + +Require Import ZArith Omega. +Open Scope Z_scope. + +(** bug 4132: omega was using "simpl" either on whole equations, or on + delimited but wrong spots. This was leading to unexpected reductions + when one atom (here [b]) is an evaluable reference instead of a variable. *) + +Lemma foo + (x y x' zxy zxy' z : Z) + (b := 5) + (Ry : - b <= y < b) + (Bx : x' <= b) + (H : - zxy' <= zxy) + (H' : zxy' <= x') : - b <= zxy. +Proof. +omega. (* was: Uncaught exception Invalid_argument("index out of bounds"). *) +Qed. + +Lemma foo2 x y (b := 5) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "index out of bounds" in the past, + but I never managed to reproduce that in any version, + even before my fix. *) +Qed. + +Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b. +omega. (* Pierre L: according to a comment of bug report #4132, + this might have triggered "Failure(occurence 2)" in the past, + but I never managed to reproduce that. *) +Qed. |