Induction sends me in a loop

Stream: general

[Billy Woods]

Hi all,

Hope I'm posting in the right place!

Here's an example of a theorem I'm having a surprising amount of difficulty proving. No matter whether I do induction on L or n, it always just seems to send me in a circle, and my inductive hypotheses end up wrong. I wonder if any Lean experts could tell me where I'm going wrong?

namespace List

  def swap : List Nat → Nat → List Nat
  | nil,                _   => nil
  | cons a nil,         _   => cons a nil
  | cons a (cons a' b), 0   => cons a' (cons a b)
  | cons a b,           n+1 => cons a (swap b n)

  theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : L.contains 5) : (swap L n).contains 5 := by
    sorry

end List

I honestly don't think it's worth sharing my exact attempts - it's always just hundreds and hundreds of lines of spiralling tactic proofs - but it's normally some mixture of dozens of unfold swap and split, most of which cases are trivial, but one of which always leads me right back to the thing I wanted to prove. Thanks!

[Kenny Lau]

this might not be very helpful, but you shouldn't have proofs that are a hundred lines long :upside_down:

[Billy Woods]

Kenny Lau said:

this might not be very helpful, but you shouldn't have proofs that are a hundred lines long :upside_down:

I wasn't happy about it either! So what's the short, snappy proof that I'm missing?

[Kenny Lau]

namespace List

def swap : List Nat → Nat → List Nat
| nil,                _   => nil
| cons a nil,         _   => cons a nil
| cons a (cons a' b), 0   => cons a' (cons a b)
| cons a b,           n+1 => cons a (swap b n)

#eval swap [1,2,3,4] 3

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  induction L generalizing n with
  | nil => simp at hl
  | cons h t =>
      obtain rfl | hl : 5 = h ∨ 5 ∈ t := by simpa using hl
      · sorry
      · sorry

end List

[Kenny Lau]

@Billy Woods this should be a good start

[Billy Woods]

That seems to have worked immediately - how strange. It's basically exactly like the many attempts I had yesterday except for that generalizing keyword, so I suppose that's my next thing to learn. Thanks!

[Kenny Lau]

namespace List

def swap : List Nat → Nat → List Nat
| nil,                _   => nil
| cons a nil,         _   => cons a nil
| cons a (cons a' b), 0   => cons a' (cons a b)
| cons a b,           n+1 => cons a (swap b n)

#eval swap [1,2,3,4] 3

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  induction L generalizing n with
  | nil => simp at hl
  | cons h t ih =>
      obtain _ | n := n
      · obtain _ | ⟨h', t⟩ := t
        · rw [swap]; exact hl
        rw [swap]; simp_all [or_left_comm]
      obtain _ | ⟨h', t⟩ := t
      · rw [swap]; exact hl
      rw [swap]
      obtain rfl | hl : 5 = h ∨ 5 ∈ h' :: t := by simpa using hl
      · simp
      specialize ih n hl
      simp [ih]
      simp

end List

[pandaman]

Another option is to use fun_induction.

namespace List

def swap : List Nat → Nat → List Nat
| nil,                _   => nil
| cons a nil,         _   => cons a nil
| cons a (cons a' b), 0   => cons a' (cons a b)
| cons a b,           n+1 => cons a (swap b n)

#eval swap [1,2,3,4] 3

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  fun_induction swap L n
  next => simp at hl
  next => exact hl
  next a a' b => grind
  next a L b h ih =>
    -- grind can solve this, but we can also manually prove it
    simp at hl
    cases hl with
    | inl eq => simp [eq]
    | inr hl' => simp [ih hl']

end List

[Kenny Lau]

something for me to learn!

[Damiano Testa]

pandaman, well done! You can also golf it like this:

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  fun_induction swap L n <;> grind

[Billy Woods]

pandaman said:

Another option is to use fun_induction.

namespace List

def swap : List Nat → Nat → List Nat
| nil,                _   => nil
| cons a nil,         _   => cons a nil
| cons a (cons a' b), 0   => cons a' (cons a b)
| cons a b,           n+1 => cons a (swap b n)

#eval swap [1,2,3,4] 3

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  fun_induction swap L n
  next => simp at hl
  next => exact hl -- (***)
  next a a' b => grind -- (***)
  next a L b h ih =>
    -- grind can solve this, but we can also manually prove it
    simp at hl
    cases hl with
    | inl eq => simp [eq] -- (***)
    | inr hl' => simp [ih hl'] -- (***)

end List

Lean is telling me four of these goals (at the places I've marked above) aren't closed yet, and grind failed at the second. I can resolve them, so thanks for pointing me towards an interesting new tactic - but what's happening here?

[Billy Woods]

Damiano Testa said:

pandaman, well done! You can also golf it like this:

theorem contains_5_imp_swap_contains_5 (L : List Nat) (n : Nat) (hl : 5 ∈ L) : 5 ∈ swap L n := by
  fun_induction swap L n <;> grind

Same here - I'm getting grind failed. I think I'm using the most recent stable version of Lean (v4.22.0-rc2)...

[Aaron Liu]

It works on the web server

[Aaron Liu]

the web server is using leanprover/lean4:v4.22.0-rc3

[Billy Woods]

You're right. After a bit of prodding there, even though VS Code is telling me that I'm running v4.22.0-rc2, #eval Lean.versionString is telling me I'm running v4.19.0. So I guess this is a VS Code problem. Thanks!

[Aaron Liu]

try updating your lean-toolchain?

[pandaman]

The fun_inductiom tactic uses the functional induction principle, which performs case splitting and induction following the structure of the function. It's very useful when the structure of the function differs from that of the arguments, like in this case.
https://lean-lang.org/blog/2024-5-17-functional-induction/