improved auto goal selection (see coq/#16293)

coq-community · Jul 11, 2022 · 711119c · 711119c
1 parent e13df50
commit 711119c
Show file tree

Hide file tree

Showing 11 changed files with 15 additions and 14 deletions.
diff --git a/complex/AbsCC.v b/complex/AbsCC.v
@@ -267,7 +267,7 @@ Qed.
 Lemma AbsCC_square_ap_zero : forall z : CC, z [#] [0] -> AbsCC z[^]2 [#] [0].
 Proof.
  intros z H.
- astepl (Re z[^]2[+]Im z[^]2).
+ stepl (Re z[^]2[+]Im z[^]2).
   apply (cc_inv_aid (Re z) (Im z) H).
  apply AbsCC_square_Re_Im with (x := Re z) (y := Im z).
 Qed.

diff --git a/complex/NRootCC.v b/complex/NRootCC.v
@@ -943,7 +943,7 @@ Proof.
   pattern n at 1 in |- *; replace n with (1 * n).
    apply degree_nexp.
    apply degree_x_.
-  replace (1 * n) with n; auto.
+  replace (1 * n) with n; [auto|..].
   unfold mult in |- *.
   auto with arith.
  assumption.

diff --git a/fta/KeyLemma.v b/fta/KeyLemma.v
@@ -164,7 +164,7 @@ Proof.
        apply less_leEq; auto.
       apply a_nonneg.
      apply H12.
-      replace (n - j) with (S (n - S j)); auto with arith.
+      replace (n - j) with (S (n - S j)); [auto with arith|].
       rewrite minus_Sn_m; auto with arith.
      auto.
     rewrite <- H22.
@@ -192,7 +192,7 @@ Proof.
   intros i H15 H16.
  elim (le_lt_eq_dec _ _ H15); intro H18.
   apply H12.
-   replace (n - j) with (S (n - S j)); auto with arith.
+   replace (n - j) with (S (n - S j)); [auto with arith|].
    rewrite minus_Sn_m; auto with arith.
   auto.
  rewrite <- H18.

diff --git a/metric2/FinEnum.v b/metric2/FinEnum.v
@@ -373,7 +373,7 @@ Proof.
   apply (msp_stable (msp X) (Zpos p # Pos.of_succ_nat (Init.Nat.pred (Pos.to_nat d)))). auto.
   apply ball_weak_le with (1 # P_of_succ_nat z); auto.
   simpl.
-  apply Zmult_le_compat; auto with *.
+  apply Zmult_le_compat; [..|auto with *].
   apply Pos.le_1_l. simpl.
   assert (forall i j:nat, le i j -> Pos.of_succ_nat i <= Pos.of_succ_nat j)%positive.
   { intros.

diff --git a/metrics/CPMSTheory.v b/metrics/CPMSTheory.v
@@ -682,7 +682,7 @@ Proof.
  astepl (OneR[*]one_div_succ (n + (n + (n + 0)) + 2)[+]
    (Two:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
  astepl ((OneR[+]Two)[*]one_div_succ (n + (n + (n + 0)) + 2)).
- astepl ((Three:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
+ stepl ((Three:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)).
   2: apply mult_wdl.
   2: rational.
  astepr ((Three:IR)[*]([1][/] Three[//]three_ap_zero IR)[*]one_div_succ n).

diff --git a/metrics/ContFunctions.v b/metrics/ContFunctions.v
@@ -146,7 +146,7 @@ Proof.
    apply shift_less_plus.
    apply minusOne_less.
   astepl (OneR[+]nexp IR p Two).
-  astepr (OneR[+]nring (power p 2)).
+  stepr (OneR[+]nring (power p 2)).
    apply plus_resp_eq.
    apply nexp_power.
   simpl in |- *.

diff --git a/metrics/LipExt.v b/metrics/LipExt.v
@@ -121,7 +121,7 @@ nexp IR n ([1][/] (Two:IR)[//]H).
 Proof.
  intros.
  astepl ((zexp Two H k)[*](nexp IR (n + k) ([1][/] Two[//]H) )).
- astepl ((zexp Two H k)[*](zexp Two H (- (n + k)%nat))).
+ stepl ((zexp Two H k)[*](zexp Two H (- (n + k)%nat))).
   astepr (zexp Two H (k + (- (n + k)%nat))).
    apply eq_symmetric.
    apply zexp_plus.

diff --git a/ode/SimpleIntegration.v b/ode/SimpleIntegration.v
@@ -567,17 +567,17 @@ Section implements_abstract_interface.
        apply Qpos_nonzero.
        rewrite E. simpl.
        setoid_replace (wbints true #1) with (/ (1#wbints true)) by reflexivity.
-       field... split. discriminate. apply Qpos_nonzero.
+       field. split. discriminate. apply Qpos_nonzero.
        assert (Zpos j == (proj1_sig (ww false) / wbints false / proj1_sig x)) as jE.
        { apply (Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero.
        rewrite F. simpl.
        setoid_replace (wbints false #1) with (/ (1#wbints false)) by reflexivity.
-       field... split. discriminate. apply Qpos_nonzero. }
+       field. split. discriminate. apply Qpos_nonzero. }
        assert (Zpos k == (proj1_sig totalw / w01ints / proj1_sig x)) as kE.
        { apply (Qmult_injective_l (proj1_sig x)). apply Qpos_nonzero.
          rewrite G. simpl.
          setoid_replace (w01ints #1) with (/ (1#w01ints)) by reflexivity.
-         field... split. discriminate. apply Qpos_nonzero. }
+         field. split. discriminate. apply Qpos_nonzero. }
        apply Qball_plus.
         (* left case: *)
         apply Σ_Qball_pos_bounds.

diff --git a/reals/fast/Interval.v b/reals/fast/Interval.v
@@ -582,7 +582,7 @@ Proof.
   rewrite -> Hlr.
   split; simpl.
    clear - H.
-   apply Qle_trans with 0%Q; auto with *.
+   apply Qle_trans with 0%Q.
    apply (Qopp_le_compat 0), Qpos_nonneg.
    rewrite -> Qle_minus_iff in *.
    rewrite Qplus_0_r.

diff --git a/transc/Exponential.v b/transc/Exponential.v
@@ -1324,7 +1324,8 @@ Proof.
  pose (G:=(([--][1][/]_[//]nringS_ap_zero IR n){**}([-C-][1]{-}FId){^}(S n))).
  assert (X0:Derivative (olor [0] Two) (pos_two IR) G (([-C-][1]{-}FId){^}n)).
   unfold G.
-  Derivative_Help; [|apply Derivative_scal;refine (Derivative_nth _ _ _ _ _ _);Deriv].
+  eapply Derivative_wdr; simpl in |- *;
+   [|apply Derivative_scal;refine (Derivative_nth _ _ _ _ _ _);Deriv].
   FEQ.
   repeat constructor.
  assert (X1:Continuous (olor [0] Two) (([-C-][1]{-}FId){^}n)).

diff --git a/transc/MoreArcTan.v b/transc/MoreArcTan.v
@@ -624,7 +624,7 @@ Proof.
  intros n.
  rewrite plus_comm.
  simpl.
- Derivative_Help; [|apply Derivative_scal;apply Derivative_nth;Deriv].
+ Derivative_Help; [|apply Derivative_scal;apply Derivative_nth;Deriv..].
  FEQ.
 Qed.