From 7cc2810b4b1ea92a8f8a8739f69a94d5578e7b9d Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 29 Mar 2021 11:12:07 +0200
Subject: replacing omega with lia in some file

---
 lib/IterList.v | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'lib/IterList.v')

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