aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-30 12:48:47 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-06-01 03:55:05 -0400
commit1d6a1036a7c472e1f20c5ec586d2484203a2fe2e (patch)
tree582c15703090acc0f79d930f0f0c81d5ed2b9440 /plugins
parent4af77d01c434ff11f0899d504628f4ff91c49142 (diff)
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.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/omega/PreOmega.v7
1 files changed, 6 insertions, 1 deletions
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.
-