diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-18 13:41:25 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-18 13:41:25 -0700 |
| commit | dc585913d86991a12826e181a66f9c3a02afbd8f (patch) | |
| tree | 17c7da4fcf5d17a64406a722fa97b7e398d7f567 /src/Util/NatUtil.v | |
| parent | 19dbf8eb3fd57262c6c66677f71e7a6617e0df9d (diff) | |
Fix for Coq 8.4 (omega used to be weaker)
Diffstat (limited to 'src/Util/NatUtil.v')
| -rw-r--r-- | src/Util/NatUtil.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v index b957c39d1..3eef976b2 100644 --- a/src/Util/NatUtil.v +++ b/src/Util/NatUtil.v @@ -217,8 +217,8 @@ Proof. | eexists; reflexivity | eexists; reflexivity | ]. - { specialize (IHm n (fun e => pf0 (f_equal_nat nat S n m e))). - destruct IHm as [? IHm]. + { specialize (IHm n). + destruct IHm as [? IHm]; [ omega | ]. eexists; rewrite IHm; reflexivity. } Qed. @@ -254,7 +254,7 @@ Proof. edestruct lt_dec_right_val; assumption. Qed. Hint Rewrite lt_dec_irrefl : natsimplify. Lemma not_lt_n_pred_n n : ~n < pred n. -Proof. omega. Qed. +Proof. destruct n; simpl; omega. Qed. Lemma lt_dec_n_pred_n n : lt_dec n (pred n) = right (proj1_sig (@lt_dec_right_val _ _ (not_lt_n_pred_n n))). Proof. edestruct lt_dec_right_val; assumption. Qed. @@ -269,17 +269,17 @@ Hint Rewrite le_dec_refl : natsimplify. Lemma le_dec_pred_l n : le_dec (pred n) n = left (le_pred_l n). Proof. - edestruct le_dec; try omega. + edestruct le_dec; [ | destruct n; simpl in *; omega ]. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_l : natsimplify. Lemma le_pred_plus_same n : n <= pred (n + n). -Proof. omega. Qed. +Proof. destruct n; simpl; omega. Qed. Lemma le_dec_pred_plus_same n : le_dec n (pred (n + n)) = left (le_pred_plus_same n). Proof. - edestruct le_dec; try omega. + edestruct le_dec; [ | destruct n; simpl in *; omega ]. apply f_equal, le_unique. Qed. Hint Rewrite le_dec_pred_plus_same : natsimplify. |