From 58c5513ad85c93709554cde95ad19241d4109adb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Jul 2016 11:35:59 -0700 Subject: Fix ListUtil for Coq 8.4 --- src/Util/NatUtil.v | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) (limited to 'src/Util/NatUtil.v') diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index d1e7bbd41..2dd1ce6b5 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -9,14 +9,14 @@ Proof. apply Min.min_case_strong; omega. Qed. Lemma max_def {x y} : max x y = x + (y - x). Proof. apply Max.max_case_strong; omega. Qed. Ltac coq_omega := omega. -Ltac handle_min_max_for_omega := +Ltac handle_min_max_for_omega_gen min max := repeat match goal with - | [ H : context[min _ _] |- _ ] => rewrite !min_def in H - | [ H : context[max _ _] |- _ ] => rewrite !max_def in H - | [ |- context[min _ _] ] => rewrite !min_def - | [ |- context[max _ _] ] => rewrite !max_def + | [ H : context[min _ _] |- _ ] => rewrite !min_def in H || setoid_rewrite min_def in H + | [ H : context[max _ _] |- _ ] => rewrite !max_def in H || setoid_rewrite max_def in H + | [ |- context[min _ _] ] => rewrite !min_def || setoid_rewrite min_def + | [ |- context[max _ _] ] => rewrite !max_def || setoid_rewrite max_def end. -Ltac handle_min_max_for_omega_case := +Ltac handle_min_max_for_omega_case_gen min max := repeat match goal with | [ H : context[min _ _] |- _ ] => revert H | [ H : context[max _ _] |- _ ] => revert H @@ -24,11 +24,24 @@ Ltac handle_min_max_for_omega_case := | [ |- context[max _ _] ] => apply Max.max_case_strong end; intros. +Ltac handle_min_max_for_omega := handle_min_max_for_omega_gen min max. +Ltac handle_min_max_for_omega_case := handle_min_max_for_omega_case_gen min max. +(* In 8.4, Nat.min is a definition, so we need to unfold it *) +Ltac handle_min_max_for_omega_compat_84 := + let min := (eval cbv [min] in min) in + let max := (eval cbv [max] in max) in + handle_min_max_for_omega_gen min max. +Ltac handle_min_max_for_omega_case_compat_84 := + let min := (eval cbv [min] in min) in + let max := (eval cbv [max] in max) in + handle_min_max_for_omega_case_gen min max. Ltac omega_with_min_max := handle_min_max_for_omega; + try handle_min_max_for_omega_compat_84; omega. Ltac omega_with_min_max_case := handle_min_max_for_omega_case; + try handle_min_max_for_omega_case_compat_84; omega. Tactic Notation "omega" := coq_omega. Tactic Notation "omega" "*" := omega_with_min_max_case. -- cgit v1.2.3