Merge PR #10875: [Stdlib] Remove some uses of the “omega” tactic

Reviewed-by: fajb

4 files changed, 26 insertions, 11 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 7c69350db4..ea4062d9fe 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1363,7 +1363,8 @@ Lemma elements_aux_cardinal :
 Proof.
  simple induction m; simpl; intuition.
  rewrite <- H; simpl.
- rewrite <- H0; omega.
+ rewrite <- H0, Nat.add_succ_r, (Nat.add_comm (cardinal t)), Nat.add_assoc.
+ reflexivity.
 Qed.
 
 Lemma elements_cardinal : forall (m:t elt), cardinal m = length (elements m).
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index 0ef356b582..fa553d9fce 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -68,7 +68,7 @@ Hint Constructors avl : core.
 Lemma height_non_negative : forall (s : t elt), avl s ->
  height s >= 0.
 Proof.
- induction s; simpl; intros; auto with zarith.
+ induction s; simpl; intros. now apply Z.le_ge.
  inv avl; intuition; omega_max.
 Qed.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e5133f66b2..342a51b39b 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -476,8 +476,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
    unfold elements.
    intros m; set (p:=1); clearbody p; revert m p.
    induction m; simpl; auto; intros.
-   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)); auto.
-   destruct o; rewrite app_length; simpl; omega.
+   rewrite (IHm1 (append p 2)), (IHm2 (append p 3)).
+   destruct o; rewrite app_length; simpl; auto.
   Qed.
 
   End CompcertSpec.
diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index da504259f5..1983c6caa1 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -17,7 +17,7 @@
     [mem x s=true] instead of [In x s],
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
-Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
+Require Import FSetProperties Zerob Sumbool DecidableTypeEx.
 
 Module WEqProperties_fun (Import E:DecidableType)(M:WSfun E).
 Module Import MP := WProperties_fun E M.
@@ -847,11 +847,16 @@ Proof.
 unfold sum.
 intros f g Hf Hg.
 assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto with fset.
-assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
+assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros x y z.
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (f x) (f y)); reflexivity.
 assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto with fset.
-assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
+assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros x y z.
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm (g x) (g y)); reflexivity.
 assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
-assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
+assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros x y z.
+  set (u := (f x + g x)); set (v := (f y + g y)).
+  rewrite !PeanoNat.Nat.add_assoc, (PeanoNat.Nat.add_comm u).
+  reflexivity.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 intros s;pattern s; apply set_rec.
 intros.
@@ -859,7 +864,10 @@ rewrite <- (fold_equal _ _ st _ fc ft 0 _ _ H).
 rewrite <- (fold_equal _ _ st _ gc gt 0 _ _ H).
 rewrite <- (fold_equal _ _ st _ fgc fgt 0 _ _ H); auto.
 intros; do 3 (rewrite (fold_add _ _ st);auto).
-rewrite H0;simpl;omega.
+rewrite H0;simpl.
+rewrite <- !(PeanoNat.Nat.add_assoc (f x)); f_equal.
+rewrite !PeanoNat.Nat.add_assoc. f_equal.
+apply PeanoNat.Nat.add_comm.
 do 3 rewrite fold_empty;auto.
 Qed.
 
@@ -872,7 +880,11 @@ assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
  repeat red; intros.
  rewrite (Hf _ _ H); auto.
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
- red; intros; omega.
+ red; intros.
+ set (a := if f x then _ else _).
+ rewrite PeanoNat.Nat.add_comm.
+ rewrite <- !PeanoNat.Nat.add_assoc. f_equal.
+ apply PeanoNat.Nat.add_comm.
 intros s;pattern s; apply set_rec.
 intros.
 change elt with E.t.
@@ -921,9 +933,11 @@ Lemma sum_compat :
   forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with fset.
 intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm.
 intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x y z; rewrite !PeanoNat.Nat.add_assoc; f_equal; apply PeanoNat.Nat.add_comm.
 Qed.
 
 End Sum.