Zulip Chat Archive

Stream: new members

Topic: working with ite


view this post on Zulip Michael Hahn (Aug 16 2020 at 00:38):

h: z = v
odd: path.crossed z (p_1.cons e hs hv hsv) = path.crossed z p_1 + ite (z = v  z = p_1.head) 1 0

I'm not super familiar with how to use ite, but I want to use h into odd to reduce the ite that i have

view this post on Zulip Alex J. Best (Aug 16 2020 at 00:53):

As you know the if is true you can use

rw if_pos at odd

which will change the ite to be 1, and give you the goal to prove z = v ∨ z = p_1.head separately.

view this post on Zulip Kenny Lau (Aug 16 2020 at 09:50):

rw if_pos (or.inl h) at odd

view this post on Zulip Jalex Stark (Aug 16 2020 at 21:52):

maybe simp [h] would get you all the way to not have an ite any more. My model here is that first it will change z = v to z = z, then change that to true then change true \or _ to true then change ite true 1 _ to 1.

view this post on Zulip Jalex Stark (Aug 16 2020 at 21:54):

I think if you know about rw if_pos, rw if_neg, and split_ifs, you should always be able to navigate through ite.

view this post on Zulip Jalex Stark (Aug 16 2020 at 21:54):

(and if it's a dite, the lemmas are called dif_pos and dif_neg)


Last updated: May 08 2021 at 18:17 UTC