Zulip Chat Archive

Stream: new members

Topic: using ite functions in a proof


Vivek Rajesh Joshi (May 13 2024 at 17:47):

I want to expand the cases of a function defined in terms of a few nested if-then-else's. Is there a better way to do it than introducing a by_cases hypothesis for every if_else?

Adam Topaz (May 13 2024 at 17:51):

Here are some examples to get you started:

import Mathlib.Tactic

example (n : ) (hn : n = 3) : (if n = 3 then 2 else 0) = 2 := by
  split <;> rfl

example (n : ) (hn : n = 1) : (if n = 3 then 2 else 0) = 0 := by
  split <;> first | rfl | linarith

example (n : ) (hn : n = 3) : (if n = 3 then 2 else 0) = 2 := by
  rw [if_pos hn]

example (n : ) (hn : n = 1) : (if n = 3 then 2 else 0) = 0 := by
  rw [if_neg]
  linarith

Vivek Rajesh Joshi (May 13 2024 at 17:58):

Is there a way to name the hypothesis that comes out of a split?

Yury G. Kudryashov (May 13 2024 at 17:58):

split_ifs with h

Vivek Rajesh Joshi (May 13 2024 at 17:58):

Got it, thanks!

Joachim Breitner (May 13 2024 at 18:00):

I also use

split
next h =>  
next h =>  

especially if you are constrained to Lean core tactics.


Last updated: May 02 2025 at 03:31 UTC