dite proofs

Stream: new members

[Bjørn Kjos-Hanssen]

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]

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

[Yakov Pechersky]

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

[Bjørn Kjos-Hanssen]

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

[Yakov Pechersky]

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]

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]

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

[Bjørn Kjos-Hanssen]

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

[Kevin Buzzard]

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]

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

[Bjørn Kjos-Hanssen]

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.