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 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