From 83a3abfa7de680f1a3279710e8f84721c32b7668 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 23 May 2017 16:33:14 +0200 Subject: zify: confusion between Pos2Z.inj_sub and Pos2Z.inj_sub_max (fix #5336) --- plugins/omega/PreOmega.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 6c0e2d776..d301217fa 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -264,8 +264,8 @@ Ltac zify_positive_op := | |- context [ Zpos (Pos.max ?a ?b) ] => rewrite (Pos2Z.inj_max a b) (* Pos.sub -> Z.max 1 (Z.sub ... ...) *) - | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub a b) in H - | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub a b) + | H : context [ Zpos (Pos.sub ?a ?b) ] |- _ => rewrite (Pos2Z.inj_sub_max a b) in H + | |- context [ Zpos (Pos.sub ?a ?b) ] => rewrite (Pos2Z.inj_sub_max a b) (* Pos.succ -> Z.succ *) | H : context [ Zpos (Pos.succ ?a) ] |- _ => rewrite (Pos2Z.inj_succ a) in H -- cgit v1.2.3 From 1fe90249916bcce13aa39f36aa39f90b0f98bf50 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 24 May 2017 10:31:30 +0200 Subject: zify: force reduction of (Z.max 0 0) and similar (fix #5439) Turn some "simpl" into "compute". Also do the same for the few "simpl (Z.of_nat ...)". This way, definition like Z.max are properly reduced, and moreover zify isn't sensible anymore to the "Arguments Z.of_nat : simpl never" that some user want (see also #5039). Unfortunately, the compute we're using now still honor the "Opaque" declarations, so a "Opaque Z.max" will block things again (see also #5374). --- plugins/omega/PreOmega.v | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'plugins/omega') diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index d301217fa..2780be4aa 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -48,10 +48,13 @@ Ltac zify_unop_var_or_term t thm a := (remember a as za; zify_unop_core t thm za). Ltac zify_unop t thm a := - (* if a is a scalar, we can simply reduce the unop *) + (* If a is a scalar, we can simply reduce the unop. *) + (* Note that simpl wasn't enough to reduce [Z.max 0 0] (#5439) *) let isz := isZcst a in match isz with - | true => simpl (t a) in * + | true => + let u := eval compute in (t a) in + change (t a) with u in * | _ => zify_unop_var_or_term t thm a end. @@ -165,14 +168,16 @@ Ltac zify_nat_op := rewrite (Nat2Z.inj_mul a b) in * (* O -> Z0 *) - | H : context [ Z.of_nat O ] |- _ => simpl (Z.of_nat O) in H - | |- context [ Z.of_nat O ] => simpl (Z.of_nat O) + | H : context [ Z.of_nat O ] |- _ => change (Z.of_nat O) with Z0 in H + | |- context [ Z.of_nat O ] => change (Z.of_nat O) with Z0 (* S -> number or Z.succ *) | H : context [ Z.of_nat (S ?a) ] |- _ => let isnat := isnatcst a in match isnat with - | true => simpl (Z.of_nat (S a)) in H + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t 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 *) @@ -181,7 +186,9 @@ Ltac zify_nat_op := | |- context [ Z.of_nat (S ?a) ] => let isnat := isnatcst a in match isnat with - | true => simpl (Z.of_nat (S a)) + | true => + let t := eval compute in (Z.of_nat (S a)) in + change (Z.of_nat (S a)) with t | _ => 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 *) -- cgit v1.2.3