unification problem in rw

Stream: general

[Dušan Gvozdenović]

Why do I have to manually specify these implicit arguments to foldl_descend when using rw tactic?

If I try to use ... := by rw [fold_descend] in foldl_eq_foldr I get two goals, exactly of types f_comm and f_assoc which I can then regularly close with assumption.

What am I missing here?

theorem foldl_descend {f : α → α → α}
    {f_comm : ∀ a b : α, f a b = f b a}
    {f_assoc : ∀ a b c : α, f (f a b) c = f a (f b c)} :
    List.foldl f init (head :: tail) = f init (List.foldl f head tail) := by
  induction tail generalizing init with
  | nil => rfl
  | cons h₂ tail ih =>
    calc
      List.foldl f init (head :: h₂ :: tail)
        = List.foldl f (f (f init head) h₂) tail  := by repeat rw [List.foldl]
      _ = List.foldl f (f init (f head h₂)) tail  := by rw [f_assoc]
      _ = List.foldl f (f init (f h₂ head)) tail  := by conv in f h₂ head => rw [f_comm]
      _ = List.foldl f (f (f init h₂) head) tail  := by rw [←f_assoc]
      _ = List.foldl f (f init h₂) (head :: tail) := by rw [←List.foldl]
      _ = f (f init h₂) (List.foldl f head tail)  := by rw [@ih (f init h₂)]
      _ = f init (f h₂ (List.foldl f head tail))  := by rw [f_assoc]
      _ = f init (List.foldl f h₂ (head :: tail)) := by rw [@ih h₂]
      _ = f init (List.foldl f (f h₂ head) tail)  := by rw [List.foldl]
      _ = f init (List.foldl f (f head h₂) tail)  := by conv in f head h₂ => rw [f_comm]
      _ = f init (List.foldl f head (h₂ :: tail)) := by rw [←List.foldl]

theorem foldl_eq_foldr
    {f : α → α → α}
    {f_comm : ∀ a b : α, f a b = f b a}
    {f_assoc : ∀ a b c : α, f (f a b) c = f a (f b c)} :
    List.foldl f init l = List.foldr f init l := by
  induction l with
  | nil => rfl
  | cons ha l ih =>
    conv => rhs; unfold List.foldr; rw [f_comm, ←ih]
    conv => lhs; unfold List.foldl
    cases l with
    | nil => rfl
    | cons hb tail =>
      calc
        List.foldl f (f init ha) (hb :: tail)
          = f (f init ha) (List.foldl f hb tail)  := by rw [@foldl_descend _ _ _ _ _ f_comm f_assoc]
        _ = f init (f ha (List.foldl f hb tail))  := by rw [f_assoc]
        _ = f init (f (List.foldl f hb tail) ha)  := by simp only [f_comm]
        _ = f (f init (List.foldl f hb tail)) ha  := by rw [←f_assoc]
        _ = f (List.foldl f init (hb :: tail)) ha := by rw [@foldl_descend _ _ _ _ _ f_comm f_assoc]

[Lucas Allen]

Lean will automatically fill in implicit arguments, but sometimes it fills in implicit arguments differently from how the user may have intended. This means that sometimes you need to specify implicit arguments in order to get the expression you actually want rewrite with.

[Dušan Gvozdenović]

Thanks, but I’m struggling to understand what sometimes means in this case. When? How does the algorithm work?

Given that we have unique variables in the context that exactly match the type of those of implicit parameters (could there be any other?) why do we have to be explicit about them?

Another observation is that I get the same result (need to manually close the goal(s)) when trying to do any of these:

rw [@foldl_descend α init hb tail f _ _]
rw [@foldl_descend α init hb tail f f_comm _]
rw [@foldl_descend α init hb tail f _ f_assoc]

[Yaël Dillies]

Is this not related to https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/.2312902.2C.20adaptations.20for.20nightly-2024-05-14/near/438566016 ?

[Kim Morrison]

I don't think so; what's referred to there is relevant for problems that have to switch back and forth between unification and synthesis, but it's not clear to me that's happening here.

You could always try this code out of nightly-testing, now that the sandbox supports that!

[Damiano Testa]

Maybe I am confused, but why should rw close those side-goals? rw does not look at the local context to fill in missing hypotheses, right? So, it is not aware of an assumption that would close its side-goals.

[Dušan Gvozdenović]

@Damiano Testa Oh ok, what you are saying makes sense. I was under impression that it does look at the local context too (still learning). Thanks!

[Damiano Testa]

To expand a little on my comment, my understanding of rw is that it looks at the expression that you point it to, scans it searching for places where your equality/iff could be used and does the substitution. What it can match just from this information, it tries to match, what it cannot, it leaves as side-goal.

At least roughly, this is what it does.

The matching is up to syntactic equality, which means (almost) that it will only happen on expression that are identically-printed (and even then, not always!). However, nothing in the mechanism that rw uses looks at anything other than the target location and the given equality with which you want to rewrite.

There are lots of surrounding subtleties, but this should be the gist of it.

[Damiano Testa]

In your examples, you can see that it did not leave f as a side-goal, since there was enough surrounding information in the target expression to deduce what f must have been, but the target has no memory/information about f_comm, f_assoc, so rw leaves that to you to fill in.