Extracting a value from an if-then-else given the condition

Stream: lean4

[James Browning]

Suppose we use an if-then-else to define some function, how can we prove that if the condition is met we get the associated result.

As a minimal example of what I mean, how could I prove the following?

def f (n : Nat) : String :=
  if n < 10 then "small" else "big"

example (n : Nat) : n < 10 → (f n) = "small" :=
  λ (n_lt_10) => sorry

It's obvious that the result is true, however it's unclear to me how to even begin proving it.

If the condition had've been n = 10 or such, it would be easy to do with n_eq_10 ▸ Eq.refl (f n). However we have n < 10, though we essentially want to perform the same sort've substitution so that if ... then ... else further reduces away to just the desired case (just like ▸ manages to do).

[Eric Wieser]

Are you aware of the lemma docs4#if_pos ?

[James Browning]

No, I've mostly been following the book : https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html

I would say the book does a pretty good job of explaing the core of dependent type theory and at least the syntax of Lean, but it really lacks examples of things in the standard library and generally how one would even create things in the standard library

There is also a fair bit of lack of searchability of especially the builtin library, like I've looked around mathlib a bit and for the most part things have textual descriptions that show up when searching, however a lot of the builtin (i.e.Init/Prelude/etc) just flat out have no descriptions let alone examples of usage so it becomes quite difficult to search for things

[Reid Barton]

I agree the discoverability is not great at the moment, which is partly due to a lack of polish (after all Lean 4 is not officially released yet).
In particular a lot of stuff in the core library is defined (maybe by necessity) in Init.Prelude, while all the functions and lemmas for working with it are elsewhere.
My best survival tip for now is to rely on autocompletion a lot.

[Reid Barton]

For example even if you know or figure out that if then else is syntax for docs4#ite, that function is defined in Init.Prelude while docs4#if_pos is in Init.Core.

[James Browning]

My best survival tip for now is to rely on autocompletion a lot.

Autocompletion has been generally useful, although it would probably be easier to find things like if_pos if they were in some namespace, like I did actually check if Decidable.* had anything like that but I couldn't find anything

In this regard Nat is pretty good, to the extent that Lean provides theorems for Nat I've generally been able to find them just by auto-complete by typing Nat. and a related word

[Kyle Miller]

I'd probably do a tactic proof. Here, I'm telling simp to unfold f and also make use of the n < 10 hypothesis. Presumably it uses if_pos but I didn't check.

example (n : Nat) : n < 10 → (f n) = "small" := by
  intro h
  simp [f, h]

[Kyle Miller]

Here's another proof that makes use of the split tactic, which can turn an if into cases.

example (n : Nat) : n < 10 → (f n) = "small" := by
  intro h
  unfold f
  split <;> rfl

Amusingly, it seems split knows how to make use of assumptions and both cases end up being the same case (with f n being replaced by "small"). I'm guessing this is a small bug in split that it creates a redundant case?

[Yaël Dillies]

Kyle Miller said:

I'd probably do a tactic proof. Here, I'm telling simp to unfold f and also make use of the n < 10 hypothesis. Presumably it uses if_pos but I didn't check.

example (n : Nat) : n < 10 → (f n) = "small" := by
  intro h
  simp [f, h]

It will simplify the expression to true (or True, not sure), and then use if_true.

[Jeremy Salwen]

(@Yaël Dillies wrong thread?)

[Yaël Dillies]

No, why?

[Yaël Dillies]

Oh I guess it got moved