Zulip Chat Archive

Stream: new members

Topic: simplification of ite


view this post on Zulip Ken Roe (Aug 11 2018 at 20:09):

How do I complete the following theorem:

theorem th :  (a:) (b:), a  b  (if a=b then 5 else 3)=3 :=
begin
    intros, ...
end

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:12):

simp *

view this post on Zulip Chris Hughes (Aug 11 2018 at 20:16):

Also rw if_neg h if h is your proof of a \ne b

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:17):

For @Chris Hughes 's solution, you might make it clearer as introv h, rw if_neg h. As a habit, you should avoid referring to auto generated variable names.

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:19):

why introv instead of intro or intros?

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:20):

I would have done intros a b h

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:21):

Because the two natural numbers already have a name and we can just keep them. The assumption however is anonymous in the statement and you should rely on the name given under the hood. Additionally, we don't refer to a and b in the proof so renaming them is not very useful.

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:22):

I didn't know that tactic!

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:22):

Pretty neat eh? :)

view this post on Zulip Patrick Massot (Aug 11 2018 at 20:23):

what does the v stand for?

view this post on Zulip Simon Hudon (Aug 11 2018 at 20:23):

Btw @Ken Roe, feel free to migrate your questioning to the general stream of Zulip. new members is more for introductions I believe.


Last updated: May 14 2021 at 11:10 UTC