From c98ed6692d16784e531f7eb8dbb1460fa20c7766 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 May 2017 11:13:31 +0200 Subject: Fix #5255: [Context (x : T := y)] should mean [Let x := y]. --- test-suite/bugs/closed/5255.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test-suite/bugs/closed/5255.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5255.v b/test-suite/bugs/closed/5255.v new file mode 100644 index 000000000..5daaf9edb --- /dev/null +++ b/test-suite/bugs/closed/5255.v @@ -0,0 +1,24 @@ +Section foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End foo. + +Module Type Foo. + Context (x := 1). + Definition foo : x = 1 := eq_refl. +End Foo. + +Set Universe Polymorphism. + +Inductive unit := tt. +Inductive eq {A} (x y : A) : Type := eq_refl : eq x y. + +Section bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End bar. + +Module Type Bar. + Context (x := tt). + Definition bar : eq x tt := eq_refl _ _. +End Bar. -- cgit v1.2.3 From 6735a7cbcaa3757e4d9ad60cb5a64fb5197b961e Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 11:46:31 -0400 Subject: fix swapping of ids in tuples, bug 5486 --- pretyping/patternops.ml | 4 ++-- test-suite/bugs/closed/5486.v | 15 +++++++++++++++ 2 files changed, 17 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/5486.v (limited to 'test-suite/bugs') diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 75d3ed30b..79e9c727d 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -360,9 +360,9 @@ let rec pat_of_raw metas vars = function PIf (pat_of_raw metas vars c, pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> - let mkGLambda c na = + let mkGLambda na c = GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in - let c = List.fold_left mkGLambda c nal in + let c = List.fold_right mkGLambda nal c in let cip = { cip_style = LetStyle; cip_ind = None; diff --git a/test-suite/bugs/closed/5486.v b/test-suite/bugs/closed/5486.v new file mode 100644 index 000000000..390133162 --- /dev/null +++ b/test-suite/bugs/closed/5486.v @@ -0,0 +1,15 @@ +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. +Goal forall (T : Type) (p : prod (prod T T) bool) (Fm : Set) (f : Fm) (k : + forall _ : T, Fm), + @eq Fm + (k + match p return T with + | pair p0 swap => fst p0 + end) f. + intros. + (* next statement failed in Bug 5486 *) + match goal with + | [ |- ?f (let (a, b) := ?d in @?e a b) = ?rhs ] + => pose (let (a, b) := d in e a b) as t0 + end. -- cgit v1.2.3 From 8c2c92cf47536b93e8e7377e8cfd89342325dbcc Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 May 2017 12:59:08 -0400 Subject: Fixing bug #5526,allow nonlinear variables in Notation patterns --- test-suite/bugs/closed/5526.v | 3 +++ test-suite/output/Notations3.out | 4 ++++ test-suite/output/Notations3.v | 6 ++++++ toplevel/metasyntax.ml | 22 +++++++++++----------- 4 files changed, 24 insertions(+), 11 deletions(-) create mode 100644 test-suite/bugs/closed/5526.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/5526.v b/test-suite/bugs/closed/5526.v new file mode 100644 index 000000000..88f219be3 --- /dev/null +++ b/test-suite/bugs/closed/5526.v @@ -0,0 +1,3 @@ +Fail Notation "x === x" := (eq_refl x) (at level 10). +Reserved Notation "x === x" (only printing, at level 10). +Notation "x === x" := (eq_refl x) (only printing). diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 360f37967..0cb870c57 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -98,3 +98,7 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0)) : nat -> Prop tele (t : Type) '(y, z) (x : t0) := tt : forall t : Type, nat * nat -> t -> fpack +fun x : ?A => x === x + : forall x : ?A, x = x +where +?A : [x : ?A |- Type] (x cannot be used) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe312..5676fe8c7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 349c05a38..6ad5182e2 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -294,22 +294,22 @@ let is_numeral symbs = | _ -> false -let rec get_notation_vars = function +let rec get_notation_vars onlyprint = function | [] -> [] | NonTerminal id :: sl -> - let vars = get_notation_vars sl in + let vars = get_notation_vars onlyprint sl in if Id.equal id ldots_var then vars else - if Id.List.mem id vars then + (* don't check for nonlinearity if printing only, see Bug 5526 *) + if not onlyprint && Id.List.mem id vars then errorlabstrm "Metasyntax.get_notation_vars" (str "Variable " ++ pr_id id ++ str " occurs more than once.") - else - id::vars - | (Terminal _ | Break _) :: sl -> get_notation_vars sl + else id::vars + | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl | SProdList _ :: _ -> assert false -let analyze_notation_tokens l = +let analyze_notation_tokens ~onlyprint l = let l = raw_analyze_notation_tokens l in - let vars = get_notation_vars l in + let vars = get_notation_vars onlyprint l in let recvars,l = interp_list_parser [] l in recvars, List.subtract Id.equal vars (List.map snd recvars), l @@ -1016,7 +1016,7 @@ let compute_syntax_data df modifiers = if onlyprint && onlyparse then error "A notation cannot be both 'only printing' and 'only parsing'."; let assoc = match assoc with None -> (* default *) Some NonA | a -> a in let toks = split_notation_string df in - let (recvars,mainvars,symbols) = analyze_notation_tokens toks in + let (recvars,mainvars,symbols) = analyze_notation_tokens onlyprint toks in let _ = check_useless_entry_types recvars mainvars etyps in let _ = check_binder_type recvars etyps in let ntn_for_interp = make_notation_key symbols in @@ -1240,7 +1240,7 @@ let add_notation_in_scope local df c mods scope = let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in - let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in + let (recvars,mainvars,symbs) = analyze_notation_tokens onlyprint dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in @@ -1317,7 +1317,7 @@ let add_notation local c ((loc,df),modifiers) sc = let add_notation_extra_printing_rule df k v = let notk = let dfs = split_notation_string df in - let _,_, symbs = analyze_notation_tokens dfs in + let _,_, symbs = analyze_notation_tokens ~onlyprint:true dfs in make_notation_key symbs in Notation.add_notation_extra_printing_rule notk k v -- cgit v1.2.3 From 2125c92aa9d17b27c9a19a59774e7e319e48262b Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 29 May 2017 18:03:19 +0200 Subject: Omega: use "simpl" only on coefficents, not on atoms (fix #4132) Two issues in one: - some focused_simpl were called on the wrong locations - some focused_simpl were done on whole equations In the two cases, this could be bad if "simpl" goes too far with respect to what omega expects: later calls to "occurrence" might fail. This may happen for instance if an atom isn't a variable, but a let-in (b:=5:Z in the example). --- plugins/omega/coq_omega.ml | 44 ++++++++++++++++++++++++++++++++++++------- test-suite/bugs/closed/4132.v | 31 ++++++++++++++++++++++++++++++ 2 files changed, 68 insertions(+), 7 deletions(-) create mode 100644 test-suite/bugs/closed/4132.v (limited to 'test-suite/bugs') 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. -- cgit v1.2.3 From e6c41b96a5ea9f8559acf176cdf997b05ccfb317 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 30 May 2017 12:10:35 +0200 Subject: Fix bug 5550: "typeclasses eauto with" does not work with section variables. --- tactics/class_tactics.ml | 1 + test-suite/bugs/closed/5550.v | 10 ++++++++++ 2 files changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/5550.v (limited to 'test-suite/bugs') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index d1ae85e7b..2c911addf 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -593,6 +593,7 @@ let make_hints g st only_classes sign = List.fold_left (fun hints hyp -> let consider = + not only_classes || let open Context.Named.Declaration in try let t = Global.lookup_named (get_id hyp) |> get_type in (* Section variable, reindex only if the type changed *) diff --git a/test-suite/bugs/closed/5550.v b/test-suite/bugs/closed/5550.v new file mode 100644 index 000000000..bb1222489 --- /dev/null +++ b/test-suite/bugs/closed/5550.v @@ -0,0 +1,10 @@ +Section foo. + + Variable bar : Prop. + Variable H : bar. + + Goal bar. + typeclasses eauto with foobar. + Qed. + +End foo. -- cgit v1.2.3 From 4af77d01c434ff11f0899d504628f4ff91c49142 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:11:28 -0400 Subject: Add opened bug 5019 --- test-suite/bugs/opened/5019.v | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 test-suite/bugs/opened/5019.v (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v new file mode 100644 index 000000000..09622097c --- /dev/null +++ b/test-suite/bugs/opened/5019.v @@ -0,0 +1,4 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Fail Timeout 1 zify. -- cgit v1.2.3 From 1d6a1036a7c472e1f20c5ec586d2484203a2fe2e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 30 May 2017 12:48:47 -0400 Subject: Fix bug #5019 (looping zify on dependent types) This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019), "[zify] loops on dependent types"; before, we would see a `Z.of_nat (S ?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on this. This may not be the "right" fix (there may be cases where `zify` should succeed where it still fails with this change), but this is a pure bugfix in the sense that the only places where it changes the behavior of `zify` are the places where, previously, `zify` looped forever. --- plugins/omega/PreOmega.v | 7 ++++++- test-suite/bugs/closed/5019.v | 5 +++++ test-suite/bugs/opened/5019.v | 4 ---- 3 files changed, 11 insertions(+), 5 deletions(-) create mode 100644 test-suite/bugs/closed/5019.v delete mode 100644 test-suite/bugs/opened/5019.v (limited to 'test-suite/bugs') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 5f5f548f8..6c0e2d776 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -174,12 +174,18 @@ Ltac zify_nat_op := match isnat with | true => simpl (Z.of_nat (S a)) in H | _ => rewrite (Nat2Z.inj_succ a) in H + | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in this one hypothesis *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H end | |- context [ Z.of_nat (S ?a) ] => let isnat := isnatcst a in match isnat with | true => simpl (Z.of_nat (S a)) | _ => rewrite (Nat2Z.inj_succ a) + | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]), + hide [Z.of_nat (S a)] in the goal *) + change (Z.of_nat (S a)) with (Z_of_nat' (S a)) end (* atoms of type nat : we add a positivity condition (if not already there) *) @@ -401,4 +407,3 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *. (** The complete Z-ification tactic *) Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op. - diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v new file mode 100644 index 000000000..7c973f88b --- /dev/null +++ b/test-suite/bugs/closed/5019.v @@ -0,0 +1,5 @@ +Require Import Coq.ZArith.ZArith. +Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. + clear; intros. + Timeout 1 zify. (* used to loop forever; should take < 0.01 s *) +Admitted. diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v deleted file mode 100644 index 09622097c..000000000 --- a/test-suite/bugs/opened/5019.v +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d. - clear; intros. - Fail Timeout 1 zify. -- cgit v1.2.3