## Stream: new members

### Topic: dite proofs

#### Bjørn Kjos-Hanssen (Dec 02 2020 at 21:44):

How do I complete the proof below? I think it must involve dif_pos somehow?

def f (x:ℕ) := if h:x=0 then 0 else 1

theorem my_thm (x:ℕ) : if h:x=0 then f x = 0 else f x = 1 :=
sorry


#### Yakov Pechersky (Dec 02 2020 at 21:46):

Still only if_pos, because you aren't using the h hypothesis.

#### Yakov Pechersky (Dec 02 2020 at 21:47):

I guess it does get turned into a dite even though you're not using the h.

#### Bjørn Kjos-Hanssen (Dec 02 2020 at 21:49):

I threw the h in because in my actual use case it seems it will be handy...

#### Yakov Pechersky (Dec 02 2020 at 21:50):

import tactic.basic

def f (x:ℕ) := if h:x=0 then 0 else 1

theorem my_thm (x:ℕ) : if h:x=0 then f x = 0 else f x = 1 :=
begin
rw f,
by_cases h : (x = 0),
{ simp [h] },
{ simp [h] },
end


#### Yakov Pechersky (Dec 02 2020 at 21:51):

Or

import tactic.basic

def f (x:ℕ) := if h:x=0 then 0 else 1

theorem my_thm (x:ℕ) : if h:x=0 then f x = 0 else f x = 1 :=
begin
split_ifs with h,
{ simp [h, f] },
{ simp [h, f] },
end


#### Yakov Pechersky (Dec 02 2020 at 21:51):

Not sure why split_ifs gets upset if you do rw f before it.

#### Bjørn Kjos-Hanssen (Dec 02 2020 at 21:54):

Thanks @Yakov Pechersky ! Would it be much harder to not use tactics?

#### Kevin Buzzard (Dec 02 2020 at 21:55):

Then you could do or.elim on some theorem saying that any natural number was 0 or not, and then use dif_pos and dif_neg. Why would you want to avoid tactics though? I mean, you could just use tactics, then #print the proof term, and then use that instead.

#### Reid Barton (Dec 02 2020 at 21:56):

it seems like you will have to do some rw equivalent, which is usually not pleasant in term mode

#### Bjørn Kjos-Hanssen (Dec 02 2020 at 21:59):

Ooh, now I did #print the proof term, and it looks :sweat_smile: rather complicated! I guess I was hoping such a simple result would have a short proof term.

Last updated: May 08 2021 at 03:17 UTC