From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 29 Mar 2021 11:12:07 +0200 Subject: replacing omega with lia in some file --- lib/Integers.v | 41 +++++++++++++++++++++-------------------- lib/IterList.v | 25 +++++++++++++------------ 2 files changed, 34 insertions(+), 32 deletions(-) (limited to 'lib') diff --git a/lib/Integers.v b/lib/Integers.v index c48af2fc..6143ab55 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec Zquot Zwf. Require Import Coqlib Zbits Axioms. Require Archi. +Require Import Lia. (** * Comparisons *) @@ -1205,20 +1206,20 @@ Proof. simpl. pose proof half_modulus_pos as HMOD. destruct (zlt 0 half_modulus) as [HMOD' | HMOD']. - 2: omega. + 2: lia. clear HMOD'. destruct (zlt (intval x) half_modulus) as [ LOW | HIGH]. { destruct x as [ix RANGE]. simpl in *. - destruct (zlt ix 0). omega. + destruct (zlt ix 0). lia. reflexivity. } destruct (zlt _ _) as [LOW' | HIGH']; trivial. destruct x as [ix RANGE]. simpl in *. rewrite half_modulus_modulus in *. - omega. + lia. Qed. Local Opaque repr. @@ -2482,20 +2483,20 @@ Proof. clear H. rewrite two_power_nat_two_p. split. - omega. + lia. set (w := (Z.of_nat wordsize)) in *. assert ((two_p 2) <= (two_p w)) as MONO. { apply two_p_monotone. - omega. + lia. } change (two_p 2) with 4 in MONO. - omega. + lia. } generalize wordsize_max_unsigned. fold zwordsize. generalize wordsize_pos. - omega. + lia. } rewrite unsigned_repr by assumption. simpl. @@ -3677,27 +3678,27 @@ Lemma shr'63: Proof. intro. unfold shr', mone, zero. - rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). apply same_bits_eq. intros i BIT. rewrite testbit_repr by assumption. - rewrite Z.shiftr_spec by omega. - rewrite bits_signed by omega. + rewrite Z.shiftr_spec by lia. + rewrite bits_signed by lia. simpl. change zwordsize with 64 in *. destruct (zlt _ _) as [LT | GE]. { - replace i with 0 in * by omega. + replace i with 0 in * by lia. change (0 + 63) with (zwordsize - 1). rewrite sign_bit_of_signed. destruct (lt x _). - all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). all: simpl; reflexivity. } change (64 - 1) with (zwordsize - 1). rewrite sign_bit_of_signed. destruct (lt x _). - all: rewrite testbit_repr by (change zwordsize with 64 in *; omega). + all: rewrite testbit_repr by (change zwordsize with 64 in *; lia). { symmetry. apply Ztestbit_m1. tauto. @@ -3711,11 +3712,11 @@ Lemma shru'63: Proof. intro. unfold shru'. - rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; omega). + rewrite Int.unsigned_repr by (change Int.max_unsigned with 4294967295; lia). apply same_bits_eq. intros i BIT. rewrite testbit_repr by assumption. - rewrite Z.shiftr_spec by omega. + rewrite Z.shiftr_spec by lia. unfold lt. rewrite signed_zero. unfold one, zero. @@ -3728,15 +3729,15 @@ Proof. rewrite sign_bit_of_signed. unfold lt. rewrite signed_zero. - destruct (zlt _ _); try omega. + destruct (zlt _ _); try lia. reflexivity. } change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i+63)). - rewrite bits_above by (change zwordsize with 64; omega). + rewrite bits_above by (change zwordsize with 64; lia). rewrite Ztestbit_1. destruct (zeq i 0); trivial. subst i. - omega. + lia. } destruct (zeq i 0) as [IZERO | INONZERO]. { subst i. @@ -3745,14 +3746,14 @@ Proof. unfold lt. rewrite signed_zero. rewrite bits_zero. - destruct (zlt _ _); try omega. + destruct (zlt _ _); try lia. reflexivity. } change (Z.testbit (unsigned x) (i + 63)) with (testbit x (i + 63)). rewrite bits_zero. apply bits_above. change zwordsize with 64. - omega. + lia. Qed. Theorem shrx'1_shr': diff --git a/lib/IterList.v b/lib/IterList.v index bde47068..d28124c7 100644 --- a/lib/IterList.v +++ b/lib/IterList.v @@ -1,4 +1,5 @@ Require Import Coqlib. +Require Import Lia. (** TODO: are these def and lemma already defined in the standard library ? @@ -55,17 +56,17 @@ Qed. Lemma length_iter_tail {A} (n:nat): forall (l: list A), (n <= List.length l)%nat -> (List.length l = n + List.length (iter_tail n l))%nat. Proof. unfold iter_tail; induction n; auto. - intros l; destruct l. { simpl; omega. } + intros l; destruct l. { simpl; lia. } intros; simpl. erewrite IHn; eauto. - simpl in *; omega. + simpl in *; lia. Qed. Lemma iter_tail_S_ex {A} (n:nat): forall (l: list A), (n < length l)%nat -> exists x, iter_tail n l = x::(iter_tail (S n) l). Proof. unfold iter_tail; induction n; simpl. - - intros l; destruct l; simpl; omega || eauto. + - intros l; destruct l; simpl; lia || eauto. - intros l H; destruct (IHn (tl l)) as (x & H1). - + destruct l; simpl in *; try omega. + + destruct l; simpl in *; try lia. + rewrite H1; eauto. Qed. @@ -74,20 +75,20 @@ Proof. intros H1 H2 EQ; exploit (length_iter_tail n1 l); eauto. rewrite EQ. rewrite (length_iter_tail n2 l); eauto. - omega. + lia. Qed. Lemma iter_tail_nil_inject {A} (n:nat) (l: list A): iter_tail n l = nil -> (List.length l <= n)%nat. Proof. - destruct (le_lt_dec n (List.length l)); try omega. - intros; exploit (iter_tail_inject1 n (length l) l); try omega. + destruct (le_lt_dec n (List.length l)); try lia. + intros; exploit (iter_tail_inject1 n (length l) l); try lia. rewrite iter_tail_reach_nil. auto. Qed. Lemma list_length_z_nat (A: Type) (l: list A): list_length_z l = Z.of_nat (length l). Proof. induction l; auto. - rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. omega. + rewrite list_length_z_cons. simpl. rewrite Zpos_P_of_succ_nat. lia. Qed. Lemma list_length_nat_z (A: Type) (l: list A): length l = Z.to_nat (list_length_z l). @@ -99,13 +100,13 @@ Lemma is_tail_list_nth_z A (l1 l2: list A): is_tail l1 l2 -> list_nth_z l2 ((list_length_z l2) - (list_length_z l1)) = list_nth_z l1 0. Proof. induction 1; simpl. - - replace (list_length_z c - list_length_z c) with 0; omega || auto. + - replace (list_length_z c - list_length_z c) with 0; lia || auto. - assert (X: list_length_z (i :: c2) > list_length_z c1). { rewrite !list_length_z_nat, <- Nat2Z.inj_gt. exploit is_tail_bound; simpl; eauto. - omega. } - destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try omega. + lia. } + destruct (zeq (list_length_z (i :: c2) - list_length_z c1) 0) as [Y|Y]; try lia. replace (Z.pred (list_length_z (i :: c2) - list_length_z c1)) with (list_length_z c2 - list_length_z c1); auto. rewrite list_length_z_cons. - omega. + lia. Qed. -- cgit