temporary unamed variable before induction

Stream: lean4

[Alexandre Rademaker]

Given the definitions below (almost identical to the ones provided by Lean):

def foldr {a b : Type} (f : a → b → b) (e : b) : List a → b
| []      => e
| x :: xs => f x (foldr f e xs)

def foldl {a b : Type} (f : b → a → b) (e : b) : List a → b
| []      => e
| x :: xs => foldl f (f e x) xs

def foldl₁ {a b : Type} (f : b → a → b) (e : b) (xs : List a) : b :=
  foldr (flip f) e xs.reverse

I was able to prove that an alternative definition of foldl is equivalent to the original definition:

example {a b : Type} (f : b → a → b) (e : b) (xs : List a)
 : foldl f e xs = foldl₁ f e xs := by
 unfold foldl₁
 induction xs generalizing e with
 | nil =>
   rw [List.reverse, foldl]; simp
   rw [foldr]
 | cons r rs ih₁ =>
   rw [List.reverse]
   simp
   rw [foldl]
   rw [ih₁ (f e r)]
   induction rs.reverse with
   | nil =>
     simp [foldr, flip]
   | cons z zs ih₂ =>
     simp [foldr, flip]
     rw [ih₂]

But if you put your cursor at the beginning of the line induction rs.reverse with (before its execution), you notice the introduction of an unnamed variable x✝ : List a. Why is that happening?

[Kyle Miller]

The induction target needs to be a local variable, so induction will use generalize rs.reverse = x first and then do induction x.

[Alexandre Rademaker]

Can I control the name of the result term rs.reverse? Moreover, why is this appearing before the induction being executed (the cursor was at the beginning of the line).

[Kyle Miller]

The induction tactic is saving the goal states after it does this generalization. Likely it should save it before generalization. (That's to say, even though your cursor is at the beginning of induction, you are seeing the goal state partway through induction being executed.)

No, you can't control the name of this term using induction. If you want control, you can manually use generalize.

There's also induction h : rs.reverse syntax for creating an equality, like with generalize h : rs.reverse = x.