Fix ListUtil for Coq 8.4

2 files changed, 36 insertions, 7 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 50927c2a4..b83d4c2a5 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -197,7 +197,7 @@ Lemma update_nth_id_eq_specific {T} f n
     update_nth n f xs = xs.
 Proof.
   induction n; destruct xs; simpl; intros;
-    try rewrite IHn; try rewrite H;
+    try rewrite IHn; try rewrite H; unfold value in *;
       try congruence; assumption.
 Qed.
 
@@ -233,6 +233,21 @@ Proof.
   induction i, xs; boring.
 Qed.
 
+(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *)
+Lemma nth_error_None : forall (A : Type) (l : list A) (n : nat), nth_error l n = None <-> length l <= n.
+Proof.
+  intros A l n.
+  destruct (le_lt_dec (length l) n) as [H|H];
+    split; intro H';
+      try omega;
+      try (apply nth_error_length_error in H; tauto);
+      try (apply nth_error_error_length in H'; omega).
+Qed.
+
+(** TODO: this is in the stdlib in 8.5; remove this when we move to 8.5-only *)
+Lemma nth_error_Some : forall (A : Type) (l : list A) (n : nat), nth_error l n <> None <-> n < length l.
+Proof. intros; rewrite nth_error_None; split; omega. Qed.
+
 Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x,
   nth_error (set_nth m x xs) n =
   if eq_nat_dec n m
@@ -240,6 +255,7 @@ Lemma nth_set_nth : forall m {T} (xs:list T) (n:nat) x,
   else nth_error xs n.
 Proof.
   intros; unfold set_nth; rewrite nth_update_nth.
+
   destruct (nth_error xs n) eqn:?, (lt_dec n (length xs)) as [p|p];
     rewrite <- nth_error_Some in p;
     solve [ reflexivity
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.