Using if-then-else definitions

Stream: new members

[Mark Dickinson]

I'm missing something fundamental. If I've defined a function ℕ → ℕ by making use of the if-then-else construct, how do I go about proving anything about that function? For example, given:

definition nat_max (m n : ℕ) := if m < n then n else m

How do I prove something like

lemma max_right (m n : ℕ) : m < n → nat_max m n = n := sorry

? This seems as though it should be trivial, but I'm struggling. unfold nat_max, by_cases (m < n)gives me two cases, one of which is an easy contradiction. The other then looks like:

m n : ℕ,
h : m < n
⊢ m < n → @ite (m < n) (nat.decidable_lt m n) ℕ n m = n

and at that point I'm stuck.

[Chris Hughes]

rw if_pos h

[Mark Dickinson]

Ah, and if_pos was the fundamental thing I was missing. Thank you!

[Mark Dickinson]

Meta-question: what's the right way for a newcomer to find out about things like if_pos? Is it reasonable to say that any attempt to learn Lean has to include reading through the source of the standard library at some point?

[Mark Dickinson]

Though looking at the definition of if_pos, I really _should_ have been able to construct it from first principles ...

[Bryan Gin-ge Chen]

Speaking as another relatively new member, the naming convention + the VS code extension's "Intellisense" window and then tactic.find are usually what I go to first. Then I ask here.

[Chris Hughes]

Ask on Zulip probably. Usually Ctrl-clicking on ite will take you to the file where it was defined, and there'll usually be all the obvious lemmas about it there, but that seems to not be the case this time.

[Mark Dickinson]

Thanks, both.

[Kevin Buzzard]

This time last year I remember Kenny and I fretting over exactly this question -- a constructor for ite -- and I found if_pos by grepping through the source code :-)