Added changes from 'easy' to 'done'

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,4 +1,4 @@
-Require Import
+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) :=

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] *)

orders/dec_fields.v

@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields.
 Require Export
@@ -22,7 +22,7 @@ Proof.
   destruct (decide (x = 0)) as [E2 | E2].
    now rewrite E2, dec_recip_0.
   apply lt_le. apply pos_dec_recip_compat.
-  apply lt_iff_le_ne. split. easy. now apply not_symmetry.
+  apply lt_iff_le_ne. split. done. now apply not_symmetry.
 Qed.
 
 Lemma neg_dec_recip_compat x : x < 0 → /x < 0.

orders/lattices.v

@@ -1,4 +1,4 @@
-Require Import
+Require Import MathClasses.misc.stdpp_tactics
   MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.orders.maps MathClasses.theory.lattices.
 
 (*
@@ -49,7 +49,7 @@ Section join_semilattice_order.
   Qed.
 
   Lemma join_le_compat_r x y z : z ≤ x → z ≤ x ⊔ y.
-  Proof. intros E. transitivity x. easy. apply join_ub_l. Qed.
+  Proof. intros E. transitivity x. done. apply join_ub_l. Qed.
   Lemma join_le_compat_l x y z : z ≤ y → z ≤ x ⊔ y.
   Proof. intros E. rewrite commutativity. now apply join_le_compat_r. Qed.
 
@@ -133,7 +133,7 @@ Section meet_semilattice_order.
   Qed.
 
   Lemma meet_le_compat_r x y z : x ≤ z → x ⊓ y ≤ z.
-  Proof. intros E. transitivity x. apply meet_lb_l. easy. Qed.
+  Proof. intros E. transitivity x. apply meet_lb_l. done. Qed.
   Lemma meet_le_compat_l x y z : y ≤ z → x ⊓ y ≤ z.
   Proof. intros E. rewrite commutativity. now apply meet_le_compat_r. Qed.
 
@@ -174,13 +174,13 @@ Section lattice_order.
   Proof.
     intros x y. apply (antisymmetry (≤)).
      now apply meet_lb_l.
-    apply meet_le. easy. now apply join_ub_l.
+    apply meet_le. done. now apply join_ub_l.
   Qed.
 
   Instance: Absorption (⊔) (⊓).
   Proof.
     intros x y. apply (antisymmetry (≤)).
-     apply join_le. easy. now apply meet_lb_l.
+     apply join_le. done. now apply meet_lb_l.
     now apply join_ub_l.
   Qed.
 
@@ -293,8 +293,8 @@ Section order_preserving_join_sl_mor.
   Proof.
     repeat (split; try apply _).
     intros x y. case (total (≤) x y); intros E.
-     rewrite 2!join_r; try easy. now apply (order_preserving _).
-    rewrite 2!join_l; try easy. now apply (order_preserving _).
+     rewrite 2!join_r; try done. now apply (order_preserving _).
+    rewrite 2!join_l; try done. now apply (order_preserving _).
   Qed.
 End order_preserving_join_sl_mor.
 
@@ -309,7 +309,7 @@ Section order_preserving_meet_sl_mor.
   Proof.
     repeat (split; try apply _).
     intros x y. case (total (≤) x y); intros E.
-     rewrite 2!meet_l; try easy. now apply (order_preserving _).
-    rewrite 2!meet_r; try easy. now apply (order_preserving _).
+     rewrite 2!meet_l; try done. now apply (order_preserving _).
+    rewrite 2!meet_r; try done. now apply (order_preserving _).
   Qed.
 End order_preserving_meet_sl_mor.