proof tactics suggestion

Stream: maths

[Mason McBride]

I'm trying to practice my theorem proving in lean, but I'm relatively new. Do any experts have lean-ic (read: pythonic) suggestions for ways to tackle this proof. I'd also like it to be readable.

theorem imo_1977_p6
  (f : ℕ+ → ℕ+)
  (h₀ : ∀ n, f (f n) < f (n + 1)) :
  ∀ n, f n = n :=
begin
  sorry
end

[Thomas Browning]

The first thing is to figure out the math-proof. What's the strategy you want to take?

[Mason McBride]

I'm unsure of the direct path, by my strategy is to use induction and also prove f n > n and f n <= n to imply f n = n

[Thomas Browning]

It's almost always easier to find the math-proof first, and then code it up in lean. But if you want to prove a subgoal by induction, the following format might be helpful:

begin
   have first_goal : ∀ n, f n ≤ n,
  { intro n,
    apply pnat.strong_induction_on n,
    intros h hk,
    sorry },
  sorry,
end

[Scott Morrison]

(Certainly don't try any IMO level problems without writing out an informal proof on paper first! Indeed, the lean-ic way to proceed would ideally be to write the module-doc first, containing the human readable informal proof. :-)

[Mason McBride]

thanks! I like this format. is there any reason it's intros h hk and not intros k hk?

[Mario Carneiro]

those are just the names of the local variables, you can name them as you wish (and k probably makes more sense than h here)

[Mason McBride]

does anyone know if I can get f(n) < n + 1 from f(f(n)) < f(n+1)?

[Mario Carneiro]

only if f is weakly increasing

[Patrick Johnson]

https://github.com/leanprover-community/mathlib/blob/master/archive/imo/imo1977_q6.lean