fix: rw argument elaboration

[leodemoura]

• rw [id] is now elaborated as rw [@id]
• Add Rewrite.Config.newGoals field for specifying how new rw goals are ordered. We use the same approach used in the apply tactic.
• Add support for optParam to rw and apply tactics.

fixes #2736

[leanprover-community-mathlib4-bot]

• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2023-10-31 12:49:43) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2023-11-01 04:24:55) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2023-11-01 04:40:49) View Log
• ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-04' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-04 14:01:46)
• 🟡 Mathlib branch lean-pr-testing-2793 build this PR didn't complete normally. (2023-11-05 23:56:30) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2023-11-06 00:44:34) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2023-11-06 14:44:32) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3e05b0641bf882d5142327b1013fb8bf38e4b9ab --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39. (2024-06-19 23:21:44)
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2024-06-23 04:31:24) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2024-06-23 05:01:38) View Log
• 🟡 Mathlib branch lean-pr-testing-2793 build against this PR was cancelled. (2024-06-23 06:14:16) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2024-06-23 06:33:22) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2024-06-23 07:46:59) View Log
• ❌ Mathlib branch lean-pr-testing-2793 built against this PR, but testing failed. (2024-06-23 09:07:15) View Log
• 🟡 Mathlib branch lean-pr-testing-2793 build this PR didn't complete normally. (2024-07-02 04:38:40) View Log
• 💥 Mathlib branch lean-pr-testing-2793 build failed against this PR. (2024-07-02 05:17:39) View Log

[kim-em]

The downstream failure is due to a regression from this PR that we should fix:

axiom P : Prop
axiom p : P
axiom f : P → Nat
axiom Q : Nat → Prop
axiom q : ∀ n, Q n
theorem r (p : P := p) : 0 = f p := sorry
example : Q 0 := by
  rw [r]
  apply q
  -- Used to work, but now: `unsolved goals: ⊢ optParam P p`

This is a pretty common pattern in Mathlib, where a side condition for a rewrite rule is specified with an optional value.

[leodemoura]

This is a pretty common pattern in Mathlib, where a side condition for a rewrite rule is specified with an optional value.

We have conflicting requests. In some situations, users want the implicit arguments consumed (e.g., example above). In other situations, they don't want because the implicit parameter causes a failure (e.g., associated issue).

@semorrison Any suggestions?

BTW, we can keep things as-is, and just tell users to use @ in the original issue.

[digama0]

I don't immediately see what #2736 has to do with optParam insertion, as there are no optParams in the example and it is instead failing with a typeclass inference failure. (Not saying there is no connection, I just don't see why these two cases are entangled.)

[leodemoura]

I don't immediately see what #2736 has to do with optParam insertion, as there are no optParams in the example and it is instead failing with a typeclass inference failure. (Not saying there is no connection, I just don't see why these two cases are entangled.)

Common theme: implicit arguments.

Given a constant foo, this commit makes rw [foo] to behave like simp [foo]. That is, both treat it as rw [@foo] and simp [@foo]. With the new behavior, implicit arguments are not processed when elaborating the tactic arguments. We have been doing that in simp, but not for rw.

[leodemoura]

@semorrison Failure above seems to be a CI issue.

[kim-em]

No, genuine failures due to this PR. I'll start minimizing, they don't look too hard.

[kim-em]

Many of the Mathlib failures are because the side conditions coming from rw have changed order.

e.g.

def Set (ι : Type) := ι → Prop

namespace Set

def univ : Set ι := fun _ => True
def empty : Set ι := fun _ => False

def pi {ι : Type} {α : ι → Type} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i) := sorry

theorem univ_pi_eq_empty (ht : t i = empty) : Set.pi univ t = empty := sorry

example (i : ι) (h : t i = empty) : Set.pi univ t = empty := by
  rw [univ_pi_eq_empty]
  · exact h

used to work, but on this toolchain it requires

  rw [univ_pi_eq_empty]
  · exact i
  · exact h

(At least we'll get some obviously missing tests for rw out of this!)

[kim-em]

The Mathlib testing PI is leanprover-community/mathlib4#8076

[leodemoura]

@semorrison Any action items for me?

[kim-em]

@semorrison Any action items for me?

@leodemoura yes, see my comment immediately above, with a MWE showing a regression due to this PR. The order of side conditions generated by rw has changed.

[leodemoura]

@leodemoura yes, see my comment immediately above, with a MWE showing a regression due to this PR. The order of side conditions generated by rw has changed.

@semorrison I saw it, but you did not make it clear whether the new order is the wrong one or not. We have regressions all the time. Note that we currently don't have newGoals := ApplyNewGoals.nonDependentFirst in the config object for the rw tactic like we do for apply. Of course, we can add it and make nonDependentFirst the default.

Update Even if we make ApplyNewGoals.nonDependentFirst the default for rw, we may still have regressions.

[digama0]

I'm not sure (I haven't thought carefully about it) which ordering is the best in an absolute sense, but I know that any change to the order of generated subgoals of rw in its default mode will result in massive breakage in mathlib (estimated >4000 use sites) and will be a major task to adapt without some ad hoc migration tooling.

[kim-em]

Ah, I see. I had thought it was clear that nonDependentFirst would be the preferred default for users and/or tactics.

That said, I don't think this is as impactful as Mario says above. Note in particular that it manages to compile about 80% of Mathlib without encountering this change, so I suspect it could be done by hand if desired.

The change that has occurred is not changing the relative order of the main goal and the introduced side goals, it is only changing the order of the side goals amongst themselves.

My preference would be that we change the behaviour to restore the ordering as before. But unless I hear otherwise I will patch Mathlib for the new behaviour, on leanprover-community/mathlib4#8076, hopefully tomorrow.

[leodemoura]

@semorrison

My preference would be that we change the behaviour to restore the ordering as before. But unless I hear otherwise I will patch Mathlib for the new behaviour, on leanprover-community/mathlib4#8076, hopefully tomorrow.

Note that the previous order was not nonDependentFirst. It just turns out that implicit arguments are often dependent ones.

Just to clarify, given a function foo where x is the first explicit argument, rw [foo] was using the following order: all for arguments starting at x, followed by all for implicit arguments occurring before x. In the example, you see the illusion of nonDependentFirst because the dependent argument is implicit.

I agree it makes sense to use nonDependentFirst, but it may cause breakage. Happy to hear you are willing to fix any breakages this change may produce.

[kim-em]

Ah, okay, that description of the goal ordering makes sense, and I agree it's not something worth preserving as is.

Shall I fix Mathlib to work with this PR as is, and we can think about moving to nonDependendFirst later, or did you want to do that in this PR?

[leodemoura]

Shall I fix Mathlib to work with this PR as is, and we can think about moving to nonDependendFirst later, or did you want to do that in this PR?

I will take a look next weekend. I think it is better to try to integrate nonDependentFirst now, to avoid more breakage in the future.

[kim-em]

I have mathlib working again. It is not too bad, except for a very large number of rws by lemmas (mostly in the linear algebra library), where we now get errors of the form "can't synthesize Ring ?R", and which can by solved either by rw [my_lemma (R := R)] or rw [my_lemma ..].

This is because of the change so rw [my_lemma] means rw [@my_lemma]. I'm not certain yet how painful people will find this change.

See leanprover-community/mathlib4#8076 for the Mathlib diff.

[fpvandoorn]

The regressions in Mathlib seem very similar to the issue reported in #2736. Is this change in Lean actually an improvement?
Do you know what causes the current rw to fail to find instances, and in what situations the new rw will fail to find instances? Can we find a way to get the best of both worlds (i.e. an algorithm for rw [foo] that will succeed when either rw [@foo] or rw [foo ..] succeeds)?

[kim-em]

@leodemoura, here is the promised minimization:

/-!
This is a minimization of an issue widely seen in Mathlib after
https://github.com/leanprover/lean4/pull/2793.
We find that we need to either specify a named argument or use `..` in certain rewrites.
-/

section Mathlib.Init.ZeroOne

set_option autoImplicit true

class Zero.{u} (α : Type u) where
  zero : α

instance (priority := 300) Zero.toOfNat0 {α} [Zero α] : OfNat α (nat_lit 0) where
  ofNat := ‹Zero α›.1

end Mathlib.Init.ZeroOne

section Mathlib.Algebra.Group.Defs

universe u v w

class HSMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
  hSMul : α → β → γ

class SMul (M : Type u) (α : Type v) where
  smul : M → α → α

@[inherit_doc] infixr:73 " • " => HSMul.hSMul

instance instHSMul {α β} [SMul α β] : HSMul α β β where
  hSMul := SMul.smul

end Mathlib.Algebra.Group.Defs

section Mathlib.Data.FunLike.Basic

class DFunLike (F : Sort _) (α : outParam (Sort _)) (β : outParam <| α → Sort _) where
  coe : F → ∀ a : α, β a

abbrev FunLike F α β := DFunLike F α fun _ => β

instance (priority := 100) hasCoeToFun {F α β} [i : DFunLike F α β] :
    CoeFun F (fun _ ↦ ∀ a : α, β a) where
  coe := @DFunLike.coe _ _ β _

end Mathlib.Data.FunLike.Basic

section Mathlib.Algebra.Group.Hom.Defs

variable {M N : Type _}
variable {F : Type _}

class ZeroHomClass (F : Type _) (M N : outParam (Type _)) [Zero M] [Zero N] [FunLike F M N] :
    Prop where
  map_zero : ∀ f : F, f 0 = 0

variable [Zero M] [Zero N] [FunLike F M N]

theorem map_zero [ZeroHomClass F M N] (f : F) : f 0 = 0 :=
  ZeroHomClass.map_zero f

end Mathlib.Algebra.Group.Hom.Defs

section Mathlib.GroupTheory.GroupAction.Defs

variable {M A : Type _}

class SMulZeroClass (M A : Type _) [Zero A] extends SMul M A where
  smul_zero : ∀ a : M, a • (0 : A) = 0

@[simp]
theorem smul_zero [Zero A] [SMulZeroClass M A] (a : M) : a • (0 : A) = 0 :=
  SMulZeroClass.smul_zero _

end Mathlib.GroupTheory.GroupAction.Defs

section Mathlib.Algebra.SMulWithZero

variable (R M)

class SMulWithZero [Zero R] [Zero M] extends SMulZeroClass R M where

@[simp]
theorem zero_smul {M} [Zero R] [Zero M] [SMulWithZero R M] (m : M) : (0 : R) • m = 0 := sorry

end Mathlib.Algebra.SMulWithZero

section Mathlib.GroupTheory.GroupAction.Hom

class MulActionSemiHomClass (F : Type _)
    {M N : outParam (Type _)} (φ : outParam (M → N))
    (X Y : outParam (Type _)) [SMul M X] [SMul N Y] [FunLike F X Y] : Prop where
  map_smulₛₗ : ∀ (f : F) (c : M) (x : X), f (c • x) = (φ c) • (f x)

export MulActionSemiHomClass (map_smulₛₗ)

end Mathlib.GroupTheory.GroupAction.Hom

section Mathlib.Algebra.Module.LinearMap.Defs

variable {R S S₃ T M M₃ : Type _}

class LinearMapClass (F : Type _) (R : outParam (Type _))
  (M M₂ : outParam (Type _)) [Add M] [Add M₂]
    [SMul R M] [SMul R M₂] [FunLike F M M₂]
    extends MulActionSemiHomClass F (id : R → R) M M₂ : Prop

variable (F : Type _)
variable [Zero R]
variable [Zero M] [Add M] [Zero M₃] [Add M₃]
variable [SMulWithZero R M] [SMulWithZero R M₃]

/--
error: failed to synthesize
  SMul ?N M₃
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
instance inst1 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
  { map_zero := fun f ↦
      show f 0 = 0 by
        rw [← zero_smul R (0 : M), map_smulₛₗ] }

instance inst2 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
  { map_zero := fun f ↦
      show f 0 = 0 by
        rw [← zero_smul R (0 : M), map_smulₛₗ (N := R)]
        simp only [map_zero, smul_zero] }

instance inst3 [FunLike F M M₃] [LinearMapClass F R M M₃] : ZeroHomClass F M M₃ :=
  { map_zero := fun f ↦
      show f 0 = 0 by
        rw [← zero_smul R (0 : M), map_smulₛₗ ..]
        simp only [map_zero, smul_zero] }

end Mathlib.Algebra.Module.LinearMap.Defs

[leodemoura]

Subsumed by #4596.
Issue in the mwe above has been fixed by #4646