How do you define piecewise functions

Stream: new members

[Sabbir Rahman]

I am kinda new to lean. How do you define linear functions? I understand if then can be done for two condition cases. but what about function with multiple pieces like. f(x) = 1 if x < 10, 2 if 10 <= x < 20, 3 if 20 <= x < 30, 4 if 30 <= x

[Damiano Testa]

Do you mean something like this?

example (x : Nat) : Nat :=
  if x < 10 then 1 else
  if x < 20 then 2 else
  if x < 30 then 3 else
  4

[Sabbir Rahman]

This does work, but one thing I dislike is that now proofs can't treat each case in the same "level" instead it's first work with first case then rest case are recursively broken up. is that the only way to go

[Aaron Liu]

Are you aware of the tactic split_ifs?

[Damiano Testa]

Can you give an example of something concrete? Does this

import Mathlib.Tactic

def F (x : Nat) : Nat :=
  if x < 10 then 1 else
  if x < 20 then 2 else
  if x < 30 then 3 else
  4

def G (x : Nat) : Nat :=
  min 4 (x / 10 + 1)

example : F = G := by
  funext
  unfold F G
  split_ifs <;>
  omega

count as different levels?

[Sabbir Rahman]

I was not aware of split_ifs this does seem better. I was afraid that I would have to first break goals to x < 10 and not x < 10, then break not x < 10 to x < 20 and not x < 20 and so on