Zulip Chat Archive

Stream: new members

Topic: dite proofs


view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 21:46):

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Dec 02 2020 at 21:51):

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

view this post on Zulip Bjørn Kjos-Hanssen (Dec 02 2020 at 21:54):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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