diff options
| author | Vincent Laporte | 2019-10-28 12:40:19 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-11-25 08:40:38 +0000 |
| commit | acf89f2db9a3c87afaceda20135539b5c4013585 (patch) | |
| tree | 7bca074905970a8337298777829be96b93ebebf3 /plugins/btauto/Reflect.v | |
| parent | 791ea687b5bbcca4cfc3dc53a57a3ff10037229e (diff) | |
btauto: use “lia” rather than “omega”
Diffstat (limited to 'plugins/btauto/Reflect.v')
| -rw-r--r-- | plugins/btauto/Reflect.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v index 98f5ab067a..867fe69550 100644 --- a/plugins/btauto/Reflect.v +++ b/plugins/btauto/Reflect.v @@ -1,4 +1,4 @@ -Require Import Bool DecidableClass Algebra Ring PArith Omega. +Require Import Bool DecidableClass Algebra Ring PArith Lia. Section Bool. @@ -80,7 +80,7 @@ Qed. Hint Extern 5 => change 0 with (min 0 0) : core. Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. Local Hint Constructors valid : core. -Hint Extern 5 => zify; omega : core. +Hint Extern 5 => lia : core. (* Compatibility with validity *) @@ -203,7 +203,7 @@ intros A n; induction n using Pos.peano_rect; intros i x def Hd; + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def). induction i using Pos.peano_case. - rewrite list_nth_base; reflexivity. - - rewrite list_nth_succ; apply IHn; zify; omega. + - rewrite list_nth_succ; apply IHn; lia. Qed. Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x. @@ -226,7 +226,7 @@ intros var; induction var; intros i j x Hd; simpl. - rewrite Pos.peano_rect_succ. induction i using Pos.peano_rect. { rewrite 2list_nth_base; reflexivity. } - { rewrite 2list_nth_succ; apply IHvar; zify; omega. } + { rewrite 2list_nth_succ; apply IHvar; lia. } Qed. Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x. @@ -251,10 +251,10 @@ intros k p Hl Hp; induction Hl; simpl. assert (Hrw : b = true); [|rewrite Hrw; reflexivity] end. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. - now intros j Hd; apply list_replace_nth_1; zify; omega. + now intros j Hd; apply list_replace_nth_1; lia. rewrite list_replace_nth_2, xorb_false_r. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. - now intros j Hd; apply list_replace_nth_1; zify; omega. + now intros j Hd; apply list_replace_nth_1; lia. Qed. (* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *) |