Port Coq code to use 'done' tactic instead of 'easy' and benchmark

implementations/ZType_integers.v

@@ -1,6 +1,6 @@
 Require
   MathClasses.implementations.stdlib_binary_integers MathClasses.theory.integers MathClasses.orders.semirings.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Bignums.SpecViaZ.ZSig Bignums.SpecViaZ.ZSigZAxioms Coq.NArith.NArith Coq.ZArith.ZArith
   MathClasses.implementations.nonneg_integers_naturals MathClasses.interfaces.orders
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations.
@@ -52,7 +52,7 @@ Instance inject_ZType_Z: Cast t Z := to_Z.
 
 #[global]
 Instance: Proper ((=) ==> (=)) to_Z.
-Proof. intros x y E. easy. Qed.
+Proof. intros x y E. done. Qed.
 
 #[global]
 Instance: SemiRing_Morphism to_Z.
@@ -211,7 +211,7 @@ Proof.
    intros x1. apply axioms.pow_0_r.
   intros x [n ?].
   unfold_equiv. unfold "^", ZType_pow. simpl.
-  rewrite <-axioms.pow_succ_r; try easy.
+  rewrite <-axioms.pow_succ_r; try done.
   now rewrite ZType_succ_1_plus.
 Qed.
 
@@ -230,7 +230,7 @@ Proof.
   rewrite spec_mul, 2!spec_pow_N.
   rewrite rings.preserves_plus, Z.pow_add_r.
     now rewrite rings.preserves_1, Z.pow_1_r.
-   easy.
+   done.
   now apply Z_of_N_le_0.
 Qed.
 

implementations/dyadics.v

@@ -3,8 +3,8 @@
    for some [Integers] implementation [Z]. These numbers form a ring and can be
    embedded into any [Rationals] implementation [Q].
 *)
-Require Import
-  Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra
+Require Import 
+  Coq.setoid_ring.Ring  MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.integers MathClasses.interfaces.naturals MathClasses.interfaces.rationals
   MathClasses.interfaces.additional_operations MathClasses.interfaces.orders
   MathClasses.orders.minmax MathClasses.orders.integers MathClasses.orders.rationals

implementations/list.v

@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads.
 Import ListNotations.
 
@@ -29,7 +29,7 @@ Section equivlistA_misc.
   Proof. intros E. now eapply InA_nil, E, InA_cons_hd. Qed.
 
   Lemma equivlistA_nil_eq l : equivlistA eqA l [] → l ≡ [].
-  Proof. induction l. easy. intros E. edestruct equivlistA_cons_nil; eauto. Qed.
+  Proof. induction l. done. intros E. edestruct equivlistA_cons_nil; eauto. Qed.
 
   Lemma InA_double_head z x l : InA eqA z (x :: x :: l) ↔ InA eqA z (x :: l).
   Proof. split; intros E1; auto. inversion_clear E1; auto. Qed.
@@ -91,14 +91,14 @@ Section equivlistA_misc.
 
   Lemma PermutationA_app_head l₁ l₂ k :
     PermutationA l₁ l₂ → PermutationA (k ++ l₁) (k ++ l₂).
-  Proof. intros. induction k. easy. apply permA_skip; intuition. Qed.
+  Proof. intros. induction k. done. apply permA_skip; intuition. Qed.
 
   Global Instance PermutationA_app :
     Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
   Proof.
     intros  l₁ l₂ Pl k₁ k₂ Pk.
     induction Pl.
-       easy.
+       done.
       now apply permA_skip.
      etransitivity.
       rewrite <-!app_comm_cons. now apply permA_swap.
@@ -113,7 +113,7 @@ Section equivlistA_misc.
 
   Lemma PermutationA_cons_append l x :
     PermutationA (x :: l) (l ++ x :: nil).
-  Proof. induction l. easy. simpl. rewrite <-IHl. intuition. Qed.
+  Proof. induction l. done. simpl. rewrite <-IHl. intuition. Qed.
 
   Lemma PermutationA_app_comm l₁ l₂ :
     PermutationA (l₁ ++ l₂) (l₂ ++ l₁).

implementations/list_finite_set.v

@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders
   MathClasses.theory.lattices MathClasses.orders.lattices.
@@ -48,7 +48,7 @@ Proof. firstorder. Qed.
 Global Instance: Proper ((=) ==> (=) ==> iff) listset_in.
 Proof.
   intros x y E1 l k E2.
-  transitivity (listset_in x k). easy.
+  transitivity (listset_in x k). done.
   unfold listset_in. now rewrite E1.
 Qed.
 
@@ -108,7 +108,7 @@ Lemma listset_to_list_preserves_join l k :
 Proof.
   destruct l as [l Pl], k as [k Pk].
   unfold join, listset_join, listset_join_raw. simpl. clear Pk Pl.
-  induction l; simpl; intros; [easy|].
+  induction l; simpl; intros; [done|].
   now rewrite <-IHl, listset_add_raw_cons.
 Qed.
 
@@ -161,7 +161,7 @@ Section listset_extend.
   Proof.
     induction 1; simpl.
        reflexivity.
-      apply sg_op_proper. now apply sm_proper. easy.
+      apply sg_op_proper. now apply sm_proper. done.
      now rewrite !associativity, (commutativity (f _)).
     etransitivity; eassumption.
   Qed.
@@ -180,7 +180,7 @@ Section listset_extend.
     fset_extend f ({{x}} ⊔ l) = f x ⊔ fset_extend f l.
   Proof.
     destruct l as [l Pl]. unfold fset_extend, list_extend. simpl. clear Pl.
-    induction l; simpl; [easy|].
+    induction l; simpl; [done|].
     case (decide_rel _); intros E.
      now rewrite E, associativity, (idempotency (&) _).
     now rewrite IHl, 2!associativity, (commutativity (f _)).
@@ -215,7 +215,7 @@ Proof.
     solve_proper.
    now rewrite preserves_bottom.
   intros x l E2 E3. rewrite list_extend_add, preserves_join, E3.
-  apply sg_op_proper; [|easy]. symmetry. now apply E1.
+  apply sg_op_proper; [|done]. symmetry. now apply E1.
 Qed.
 
 Instance: FSetContainsSpec A.
@@ -251,7 +251,7 @@ Proof.
     intros E1; inversion E1.
    case (decide_rel); intros ? E1; intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
-  intros [E1 E2]. induction l; simpl; [easy|].
+  intros [E1 E2]. induction l; simpl; [done|].
   case (decide_rel); intros E3.
    inversion_clear E1; intuition.
   inversion_clear E1 as [?? E4|]; intuition.
@@ -292,7 +292,7 @@ Proof.
    case (decide_rel); intros ? E1.
     intuition.
    inversion_clear E1 as [?? E2|]; auto. now rewrite E2.
-  intros [E1 E2]. induction l; simpl; [easy|].
+  intros [E1 E2]. induction l; simpl; [done|].
   case (decide_rel); intros E3.
    inversion_clear E1 as [?? E4|]; intuition.
    destruct E2. now rewrite E4.

implementations/option.v

@@ -1,5 +1,5 @@
-Require Import
-  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads.
+Require Import MathClasses.misc.stdpp_tactics
+  MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads MathClasses.misc.stdpp_tactics.
 
 Inductive option_equiv A `{Equiv A} : Equiv (option A) :=
   | option_equiv_Some : Proper ((=) ==> (=)) Some
@@ -27,7 +27,7 @@ Section contents.
     intros x y z E. revert z. induction E.
      intros z E2. inversion_clear E2.
      apply option_equiv_Some. etransitivity; eassumption.
-    easy.
+    done.
   Qed.
 
   Global Instance: Setoid_Morphism Some.
@@ -59,7 +59,7 @@ Section contents.
        now apply E1.
       symmetry. now apply E1.
      now apply E1.
-    easy.
+    done.
   Qed.
 
   Global Program Instance option_dec `(A_dec : ∀ x y : A, Decision (x = y))
@@ -111,7 +111,7 @@ Instance option_bind_proper `{Setoid A} `{Setoid (option B)}: Proper (=) (option
 Proof.
   intros f₁ f₂ E1 x₁ x₂ [?|].
    unfold option_bind. simpl. now apply E1.
-  easy.
+  done.
 Qed.
 
 #[global]
@@ -122,8 +122,8 @@ Proof.
    now intros ? ? ? [?|].
   intros A ? B ? C ? ? f [???] g [???] [x|] [y|] E; try solve [inversion_clear E].
    setoid_inject. cut (g x = g y); [|now rewrite E].
-   case (g x), (g y); intros E2; inversion_clear E2. now f_equiv. easy.
-  easy.
+   case (g x), (g y); intros E2; inversion_clear E2. now f_equiv. done.
+  done.
 Qed.
 
 #[global]
@@ -140,7 +140,7 @@ Section map.
   Proof.
     pose proof (injective_mor f).
     repeat (split; try apply _).
-    intros [x|] [y|] E; try solve [inversion E | easy].
+    intros [x|] [y|] E; try solve [inversion E | done].
     apply sm_proper. apply (injective f). now apply (injective Some).
   Qed.
 End map.

implementations/polynomials.v

@@ -1,4 +1,5 @@
-Require Import
+Require Import 
+  MathClasses.misc.stdpp_tactics
   Coq.Lists.List
   MathClasses.interfaces.abstract_algebra
   MathClasses.interfaces.vectorspace
@@ -63,7 +64,7 @@ Section contents.
 
   Lemma poly_eq_cons :
     ∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).
-  Proof. easy. Qed.
+  Proof. done. Qed.
 
   Lemma poly_eq_ind (P: poly → poly → Prop)
         (case_0: ∀ p p', poly_eq_zero p → poly_eq_zero p' → P p p')
@@ -134,7 +135,7 @@ Section contents.
   Proof.
     intro eqp; revert q.
     induction eqp as [|x p eqx eqp IH] using poly_eq_zero_ind.
-    { easy. }
+    { done. }
     intros [|y q].
     { cbn -[poly_eq_zero].
       rewrite poly_eq_zero_cons; auto. }
@@ -143,7 +144,7 @@ Section contents.
   Qed.
 
   Instance plus_commutative: Commutative (+).
-  Proof with (try easy); cbn.
+  Proof with (try done); cbn.
     intro.
     induction x as [|x p IH]; intros [|y q]...
     split; auto; ring.
@@ -179,7 +180,7 @@ Section contents.
   Qed.
 
   Instance plus_associative: Associative (+).
-  Proof with try easy.
+  Proof with try done.
     do 2 red; induction x as [|x p IH]...
     intros [|y q]...
     intros [|z r]...
@@ -200,7 +201,7 @@ Section contents.
   Lemma poly_negate_zero p: poly_eq_zero p ↔ poly_eq_zero (-p).
   Proof.
     induction p as [|x p IH].
-    { easy. }
+    { done. }
     cbn.
     rewrite !poly_eq_zero_cons, IH.
     enough (x = 0 ↔ -x = 0) by tauto.
@@ -219,7 +220,7 @@ Section contents.
   Proof.
     intro; rewrite poly_eq_p_zero.
     induction x as [|x p IH]; cbn.
-    { easy. }
+    { done. }
     rewrite poly_eq_zero_cons; split; auto.
     ring.
   Qed.
@@ -239,7 +240,7 @@ Section contents.
   Lemma poly_scalar_mult_0_r q c: poly_eq_zero q → poly_eq_zero (c · q).
   Proof.
     induction q as [|x q IH].
-    { easy. }
+    { done. }
     cbn.
     rewrite !poly_eq_zero_cons.
     intros [-> ?]; split; auto.
@@ -257,36 +258,36 @@ Section contents.
   Qed.
 
   Lemma poly_scalar_mult_1_r x: x · 1 = [x].
-  Proof. cbn; split; [ring|easy]. Qed.
+  Proof. cbn; split; [ring|done]. Qed.
   Instance poly_scalar_mult_1_l: LeftIdentity (·) 1.
   Proof.
-    red; induction y as [|y p IH]; [easy|cbn].
+    red; induction y as [|y p IH]; [done|cbn].
     split; auto; ring.
   Qed.
 
   Instance poly_scalar_mult_dist_l: LeftHeteroDistribute (·) (+) (+).
   Proof.
     intros a p.
-    induction p as [|x p IH]; intros [|y q]; [easy..|cbn].
+    induction p as [|x p IH]; intros [|y q]; [done..|cbn].
     split; auto; ring.
   Qed.
   Instance poly_scalar_mult_dist_r: RightHeteroDistribute (·) (+) (+).
   Proof.
     intros a b x.
-    induction x as [|x p IH]; [easy|cbn].
+    induction x as [|x p IH]; [done|cbn].
     split; auto; ring.
   Qed.
   Instance poly_scalar_mult_assoc: HeteroAssociative (·) (·) (·) (.*.).
   Proof.
     intros a b x.
-    induction x as [|p x IH]; [easy|cbn].
+    induction x as [|p x IH]; [done|cbn].
     split; auto; ring.
   Qed.
 
   Lemma poly_scalar_mult_0_l q c: c = 0 → poly_eq_zero (c · q).
   Proof.
     intros ->.
-    induction q as [|x q IH]; [easy|cbn].
+    induction q as [|x q IH]; [done|cbn].
     rewrite poly_eq_zero_cons; split; auto.
     ring.
   Qed.
@@ -299,15 +300,15 @@ Section contents.
 
   Lemma poly_mult_0_l p q: poly_eq_zero p → poly_eq_zero (p * q).
   Proof.
-    induction 1 using poly_eq_zero_ind; [easy|cbn].
+    induction 1 using poly_eq_zero_ind; [done|cbn].
     apply poly_eq_zero_plus.
     - now apply poly_scalar_mult_0_l.
     - rewrite poly_eq_zero_cons; auto.
   Qed.
 
   Lemma poly_mult_0_r p q: poly_eq_zero q → poly_eq_zero (p * q).
   Proof.
-    induction p as [|x p IH]; [easy|cbn].
+    induction p as [|x p IH]; [done|cbn].
     intro eq0.
     apply poly_eq_zero_plus.
     - now apply poly_scalar_mult_0_r.
@@ -330,20 +331,20 @@ Section contents.
   Instance poly_mult_left_distr: LeftDistribute (.*.) (+).
   Proof.
     intros p q r.
-    induction p as [|x p IH]; [easy|cbn].
+    induction p as [|x p IH]; [done|cbn].
     rewrite (distribute_l x q r ).
-    rewrite <- !associativity; apply poly_plus_proper; [easy|].
+    rewrite <- !associativity; apply poly_plus_proper; [done|].
     rewrite associativity, (commutativity (0::p*q)), <- associativity.
-    apply poly_plus_proper; [easy|].
-    cbn; split; [ring|easy].
+    apply poly_plus_proper; [done|].
+    cbn; split; [ring|done].
   Qed.
 
   Lemma poly_mult_cons_r p q x: p * (x::q) = x · p + (0 :: p * q).
   Proof.
     induction p as [|y p IH]; cbn; auto.
     split; auto.
     rewrite IH, !associativity, (commutativity (y · q)).
-    split; try easy.
+    split; try done.
     ring.
   Qed.
 
@@ -383,7 +384,7 @@ Section contents.
   Qed.
 
   Instance poly_mult_assoc: Associative (.*.).
-  Proof with (try easy); cbn.
+  Proof with (try done); cbn.
     intros x.
     induction x as [|x p IH]...
     intros q r; cbn.

implementations/stdlib_binary_integers.v

@@ -1,6 +1,6 @@
 Require
   MathClasses.interfaces.naturals MathClasses.theory.naturals MathClasses.implementations.peano_naturals MathClasses.theory.integers.
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.ZArith.BinInt Coq.setoid_ring.Ring Coq.Arith.Arith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Numbers.Integer.Binary.ZBinary
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers
   MathClasses.implementations.natpair_integers MathClasses.implementations.stdlib_binary_naturals
@@ -152,7 +152,7 @@ Proof.
   rapply semirings.dec_full_pseudo_srorder.
   split.
    intro. split. now apply Zorder.Zlt_le_weak. now apply Zorder.Zlt_not_eq.
-  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). easy. now destruct E2.
+  intros [E1 E2]. destruct (Zorder.Zle_lt_or_eq _ _ E1). done. now destruct E2.
 Qed.
 
 (* * Embedding of the Peano naturals into [Z] *)