Zgcd_alt: use “lia” rather than “omega”

1 files changed, 24 insertions, 42 deletions

diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 0cc137ef5d..da2df40572 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -25,7 +25,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
 Require Import Znumtheory.
-Require Import Omega.
+Require Import Lia.
 
 Open Scope Z_scope.
 
@@ -76,8 +76,7 @@ Open Scope Z_scope.
    Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b).
  Proof.
    induction n.
-   simpl; intros.
-   exfalso; generalize (Z.abs_nonneg a); omega.
+   intros; lia.
    destruct a; intros; simpl;
      [ generalize (Zis_gcd_0_abs b); intuition | | ];
    unfold Z.modulo;
@@ -85,8 +84,7 @@ Open Scope Z_scope.
    destruct (Z.div_eucl b (Zpos p)) as (q,r);
    intros (H0,H1);
    rewrite Nat2Z.inj_succ in H; simpl Z.abs in H;
-   (assert (H2: Z.abs r < Z.of_nat n) by
-    (rewrite Z.abs_eq; auto with zarith));
+   (assert (H2: Z.abs r < Z.of_nat n) by lia);
     assert (IH:=IHn r (Zpos p) H2); clear IHn;
     simpl in IH |- *;
     rewrite H0.
@@ -108,15 +106,11 @@ Open Scope Z_scope.
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
    enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.
-   induction N.
-   inversion 1.
+   induction N. intros; lia.
+   intros [ | [ | n ] ]. 1-2: simpl; lia.
    intros.
-   destruct n.
-   simpl; auto with zarith.
-   destruct n.
-   simpl; auto with zarith.
    change (0 <= fibonacci (S n) + fibonacci n).
-   generalize (IHN n) (IHN (S n)); omega.
+   generalize (IHN n) (IHN (S n)); lia.
  Qed.
 
  Lemma fibonacci_incr :
@@ -129,7 +123,7 @@ Open Scope Z_scope.
    destruct m.
    simpl; auto with zarith.
    change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
-   generalize (fibonacci_pos m); omega.
+   generalize (fibonacci_pos m); lia.
  Qed.
 
  (** 3) We prove that fibonacci numbers are indeed worst-case:
@@ -144,8 +138,8 @@ Open Scope Z_scope.
    fibonacci (S (S n)) <= b.
  Proof.
    induction n.
-   intros [|a|a]; intros; simpl; omega.
-   intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ].
+   intros [|a|a]; intros; simpl; lia.
+   intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ].
    remember (S n) as m.
    rewrite Heqm at 2. simpl Zgcdn.
    unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl).
@@ -161,20 +155,13 @@ Open Scope Z_scope.
        apply Zis_gcd_sym.
        apply Zis_gcd_for_euclid2; auto.
        apply Zis_gcd_sym; auto.
-     + split; auto.
-       rewrite EQ.
-       apply Z.add_le_mono; auto.
-       apply Z.le_trans with (Zpos a * 1); auto.
-       now rewrite Z.mul_1_r.
-       apply Z.mul_le_mono_nonneg_l; auto with zarith.
-       change 1 with (Z.succ 0). apply Z.le_succ_l.
-       destruct q; auto with zarith.
-       assert (Zpos a * Zneg p < 0) by now compute. omega.
+     + split. auto.
+       destruct q. lia. 1-2: nia.
    - (* r = 0 *)
      clear IHn EQ Hr'; intros _.
      subst r; simpl; rewrite Heqm.
      destruct n.
-     + simpl. omega.
+     + simpl. lia.
      + now destruct 1.
  Qed.
 
@@ -184,7 +171,7 @@ Open Scope Z_scope.
    0 < a < b -> a < fibonacci (S n) ->
    Zis_gcd a b (Zgcdn n a b).
  Proof.
-   destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate].
+   destruct a. 1,3 : intros; lia.
    cut (forall k n b,
      k = (S (Pos.to_nat p) - n)%nat ->
      0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
@@ -192,22 +179,17 @@ Open Scope Z_scope.
    destruct 2; eauto.
    clear n; induction k.
    intros.
-   assert (Pos.to_nat p < n)%nat by omega.
    apply Zgcdn_linear_bound.
-   simpl.
-   generalize (inj_le _ _ H2).
-   rewrite Nat2Z.inj_succ.
-   rewrite positive_nat_Z; auto.
-   omega.
+   lia.
    intros.
    generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
    assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
    apply IHk; auto.
-   omega.
+   lia.
    replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
-   generalize (fibonacci_pos n); omega.
+   generalize (fibonacci_pos n); lia.
    replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto.
-   generalize (H2 H3); clear H2 H3; omega.
+   generalize (H2 H3); clear H2 H3; lia.
  Qed.
 
  (** 4) The proposed bound leads to a fibonacci number that is big enough. *)
@@ -215,7 +197,7 @@ Open Scope Z_scope.
  Lemma Zgcd_bound_fibonacci :
    forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
  Proof.
-   destruct a; [omega| | intro H; discriminate].
+   destruct a; [lia| | intro H; discriminate].
    intros _.
    induction p; [ | | compute; auto ];
     simpl Zgcd_bound in *;
@@ -224,10 +206,10 @@ Open Scope Z_scope.
     assert (n <> O) by (unfold n; destruct p; simpl; auto).
 
    destruct n as [ |m]; [elim H; auto| ].
-   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega.
+   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia.
 
    destruct n as [ |m]; [elim H; auto| ].
-   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega.
+   generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; lia.
  Qed.
 
  (* 5) the end: we glue everything together and take care of
@@ -265,10 +247,10 @@ Open Scope Z_scope.
   Z.le_elim H1.
   + apply Zgcdn_ok_before_fibonacci; auto.
     apply Z.lt_le_trans with (fibonacci (S m));
-    [ omega | apply fibonacci_incr; auto].
+    [ lia | apply fibonacci_incr; auto].
   + subst r; simpl.
-    destruct m as [ |m]; [exfalso; omega| ].
-    destruct n as [ |n]; [exfalso; omega| ].
+    destruct m as [ |m]; [ lia | ].
+    destruct n as [ |n]; [ lia | ].
     simpl; apply Zis_gcd_sym; apply Zis_gcd_0.
  Qed.
 
@@ -277,7 +259,7 @@ Open Scope Z_scope.
  Proof.
    destruct a.
    - simpl; intros.
-     destruct n; [exfalso; omega | ].
+     destruct n; [ lia | ].
      simpl; generalize (Zis_gcd_0_abs b); intuition.
    - apply Zgcdn_is_gcd_pos.
    - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp.