# Zulip Chat Archive

## 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