Adapt to rocq-prover/rocq#21129. (#140)

Author: ppedrot

implementations/field_of_fractions.v

@@ -116,7 +116,7 @@ Proof.
     rewrite 2!mult_1_r.
     apply (is_ne_0 1).
    unfold dec_recip, Frac_dec_recip.
-   case (decide_rel); simpl; intuition.
+   case (decide_rel); simpl; intuition; auto with *.
   intros [xn xs] Ex.
   unfold dec_recip, Frac_dec_recip.
   simpl. case (decide_rel); simpl.

implementations/list.v

@@ -23,7 +23,7 @@ Section equivlistA_misc.
   Proof.
     split; intros E.
      inversion_clear E; auto. now destruct (proj1 (InA_nil eqA x)).
-    rewrite E. intuition.
+    rewrite E. intuition; auto with *.
   Qed.
 
   Lemma equivlistA_cons_nil x l : ¬equivlistA eqA (x :: l) [].
@@ -81,8 +81,8 @@ Section equivlistA_misc.
   Global Instance: Equivalence PermutationA.
   Proof.
     split.
-      intros l. induction l; intuition.
-     intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition.
+      intros l. induction l; intuition; auto with *.
+     intros l₁ l₂. induction 1; eauto. apply permA_skip; intuition; auto with *.
     intros ???. now apply permA_trans.
   Qed.
 
@@ -92,7 +92,7 @@ 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. easy. apply permA_skip; intuition; auto with *. Qed.
 
   Global Instance PermutationA_app :
     Proper (PermutationA ==> PermutationA ==> PermutationA) (@app A).
@@ -153,8 +153,8 @@ Section equivlistA_misc.
      intros. now rewrite equivlistA_nil_eq by now symmetry.
     intros l₂ Pl₂ E2.
     destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]].
-     rewrite <-E2. intuition.
-    subst. transitivity (y :: l₁); [intuition |].
+     rewrite <-E2. intuition; auto with *.
+    subst. transitivity (y :: l₁); [intuition; auto with * |].
     apply PermutationA_cons_app, IHPl₁.
      now apply NoDupA_split with y.
     apply equivlistA_NoDupA_split with x y; intuition.

implementations/ne_list.v

@@ -95,10 +95,10 @@ Section contents.
   Definition Permutation (x y: L): Prop := ListPermutation x y.
 
   Global Instance: Equivalence Permutation.
-  Proof with intuition.
+  Proof.
    unfold Permutation.
-   split; repeat intro...
-   transitivity y...
+   split; repeat intro; auto with *.
+   transitivity y; auto with *.
   Qed.
 
   Global Instance: Proper (Permutation ==> ListPermutation) to_list.

implementations/polynomials.v

@@ -59,7 +59,7 @@ Section contents.
   Proof. now destruct p. Qed.
 
   Instance: Reflexive poly_eq.
-  Proof with intuition. repeat intro. induction x... split... Qed.
+  Proof with intuition. repeat intro. induction x; auto with *. split; auto with *. Qed.
 
   Lemma poly_eq_cons :
     ∀ (a b : R) (p q : poly), (a = b /\ poly_eq p q) <-> poly_eq (a :: p) (b :: q).

orders/minmax.v

@@ -30,7 +30,7 @@ Section contents.
   Instance: LeftDistribute max min.
   Proof.
     intros x y z. unfold min, max, sort.
-    repeat case (decide_rel _); simpl; try solve [intuition].
+    repeat case (decide_rel _); simpl; try solve [intuition; auto with *].
      intros. apply (antisymmetry (≤)); [|easy]. now transitivity y; apply le_flip.
     intros. now apply (antisymmetry (≤)).
   Qed.

theory/ua_congruence.v

@@ -38,17 +38,17 @@ Section contents.
   Let lifted_normal := @op_type_equiv (sorts σ) v ve.
 
   Instance lifted_e_proper o: Proper ((=) ==> (=) ==> iff) (lifted_e o).
-  Proof with intuition.
+  Proof.
    induction o; simpl. intuition.
    repeat intro.
    unfold respectful.
    split; intros.
-    assert (x x1 = y x1). apply H0...
-    assert (x0 y1 = y0 y1). apply H1...
-    apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5)...
-   assert (x x1 = y x1). apply H0...
-   assert (x0 y1 = y0 y1). apply H1...
-   apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5)...
+    assert (x x1 = y x1). apply H0; auto with *.
+    assert (x0 y1 = y0 y1). apply H1; auto with *.
+    apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5); auto with *.
+   assert (x x1 = y x1). apply H0; auto with *.
+   assert (x0 y1 = y0 y1). apply H1; auto with *.
+   apply (IHo (x x1) (y x1) H4 (x0 y1) (y0 y1) H5); auto with *.
   Qed. (* todo: clean up *)
 
   (* With that out of the way, we show that there are two equivalent ways of stating compatibility with the
@@ -85,8 +85,8 @@ Section contents.
    clearbody f.
    induction (σ o)...
    simpl in *...
-   apply IHo0...
-   apply H1...
+   apply IHo0; intuition; auto with *.
+   apply H1; auto with *.
   Qed. (* todo: clean up *)
 
   Lemma eSub_eAlgebra: eSub → eAlgebra.
@@ -110,7 +110,7 @@ Section contents.
    simpl in *.
    repeat intro.
    unfold respectful in H0.
-   apply (IHo0 (λ b, f b (if b then x else y)))...
+   apply (IHo0 (λ b, f b (if b then x else y))); auto with *.
   Qed. (* todo: clean up *)
 
   Lemma back_and_forth: iffT eSub eAlgebra.
@@ -231,7 +231,7 @@ Section first_iso.
     exists o1...
    destruct X.
    apply (@op_closed_proper σ B _ _ _ image image_proper _ (o1 z) (o1 (f _ x))).
-    apply H3...
+    apply H3; auto with *.
    apply IHo0 with (o2 x)...
    apply _.
   Qed.

theory/ua_products.v

@@ -198,18 +198,18 @@ Section categorical.
 
   Global Program Instance: IntroProduct c (product c) := λ H h a X i, h i a X.
 
-  Next Obligation. Proof with intuition.
+  Next Obligation. Proof.
    repeat constructor; try apply _.
-     intros ?? E ?. destruct h. simpl. rewrite E...
+     intros ?? E ?. destruct h. simpl. rewrite E; auto with *.
     intro o.
     pose proof (λ i, @preserves _ _ _ _ _ _ _ _ (proj2_sig (h i)) o) as H0.
     unfold product_ops, algebra_op.
     set (o0 := λ i, varieties.variety_ops et (c i) o).
     set (o1 := varieties.variety_ops et H o) in *.
     change (∀i : I, Preservation et H (c i) (` (h i)) o1 (o0 i)) in H0.
     clearbody o0 o1. revert o0 o1 H0.
-    induction (et o); simpl...
-   apply (@product_algebra et I c)...
+    induction (et o); simpl; auto with *.
+   apply (@product_algebra et I c); auto with *.
   Qed.
 
   Global Instance: Product c (product c).

theory/ua_subalgebra.v

@@ -16,12 +16,12 @@ Section subalgebras.
     end.
 
   Global Instance op_closed_proper: ∀ `{∀ s, Proper ((=) ==> iff) (P s)} o, Proper ((=) ==> iff) (@op_closed o).
-  Proof with intuition.
+  Proof.
    induction o; simpl; intros x y E.
-    rewrite E...
+    rewrite E; auto with *.
    split; intros.
-    apply (IHo (x z))... apply E...
-   apply (IHo _ (y z))... apply E...
+    apply (IHo (x z)); auto with *. apply E; auto with *.
+   apply (IHo _ (y z)); auto with *. apply E; auto with *.
   Qed.
 
   Class ClosedSubset: Prop :=

theory/ua_subalgebraT.v

@@ -28,10 +28,10 @@ Section subalgebras.
     intuition.
    split; intros...
     apply (IHo (x z))...
-    apply E...
-   apply (IHo (y z))...
+    apply E; auto with *.
+   apply (IHo (y z)); auto with *.
    symmetry.
-   apply E...
+   apply E; auto with *.
   Qed.
 
   Class ClosedSubset: Type :=

theory/ua_subvariety.v

@@ -33,23 +33,23 @@ Section contents.
      transitivity x0...
     transitivity x1...
     transitivity y0...
-   assert (∀ u, x u = y u). intros. apply U...
+   assert (∀ u, x u = y u). intros. apply U; auto with *.
    split; repeat intro.
     apply -> (IHo (x u) (y u) (H1 u) (x0 (proj1_sig u)))...
-    apply K...
+    apply K; auto with *.
    apply <- (IHo (x u) (y u) (H1 u) (x0 (proj1_sig u)))...
-   apply K...
+   apply K; auto with *.
   Qed.
 
   Lemma heq_eval vars {o} (t: T et o): heq (eval et vars t) (eval et (Pvars vars) t).
   Proof with intuition.
    induction t; simpl...
-     unfold Pvars...
+     unfold Pvars; auto with *.
     simpl in IHt1.
     generalize (IHt1 (eval et vars t3)). clear IHt1.
     apply heq_proper.
      pose proof (@eval_proper et (carrier P) _ _ _ nat (ne_list.cons y t1)).
-     apply H1; try intro...
+     apply H1; try intro; auto with *.
     pose proof (@eval_proper et A _ _ _ nat (ne_list.cons y t1)).
     apply H1...
     unfold heq in IHt2. (* todo: this wasn't needed in a previous Coq version *)