lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

fix: `rw` argument elaboration

Open leodemoura opened this issue 1 year ago • 21 comments

  • 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

leodemoura avatar Oct 31 '23 11:10 leodemoura

leanprover-community-mathlib4-bot avatar Oct 31 '23 12:10 leanprover-community-mathlib4-bot

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.

kim-em avatar Nov 01 '23 04:11 kim-em

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.

leodemoura avatar Nov 01 '23 17:11 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.)

digama0 avatar Nov 01 '23 20:11 digama0

I don't immediately see what https://github.com/leanprover/lean4/issues/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 avatar Nov 03 '23 12:11 leodemoura

@semorrison Failure above seems to be a CI issue.

leodemoura avatar Nov 06 '23 00:11 leodemoura

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

kim-em avatar Nov 06 '23 01:11 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 avatar Nov 06 '23 01:11 kim-em

The Mathlib testing PI is https://github.com/leanprover-community/mathlib4/pull/8076

kim-em avatar Nov 06 '23 01:11 kim-em

@semorrison Any action items for me?

leodemoura avatar Nov 06 '23 04:11 leodemoura

@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.

kim-em avatar Nov 06 '23 05:11 kim-em

@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.

leodemoura avatar Nov 06 '23 19:11 leodemoura

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.

digama0 avatar Nov 06 '23 21:11 digama0

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.

kim-em avatar Nov 07 '23 10:11 kim-em

@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 https://github.com/leanprover-community/mathlib4/pull/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.

leodemoura avatar Nov 07 '23 14:11 leodemoura

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?

kim-em avatar Nov 08 '23 08:11 kim-em

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.

leodemoura avatar Nov 08 '23 12:11 leodemoura

@leodemoura, are you still planning on implementing nonDependentFirst here? If not we need a new plan here. (Either change the behaviour in this PR so the order of side conditions is preserved, or start the Mathlib adaptation.)

kim-em avatar Nov 22 '23 04:11 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 https://github.com/leanprover-community/mathlib4/pull/8076 for the Mathlib diff.

kim-em avatar Jun 23 '24 06:06 kim-em

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)?

fpvandoorn avatar Jun 23 '24 09:06 fpvandoorn

@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

kim-em avatar Jul 02 '24 05:07 kim-em

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

leodemoura avatar Jul 03 '24 21:07 leodemoura