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 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'plugins/omega') 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. - -- cgit v1.2.3