Zulip Chat Archive

Stream: Is there code for X?

Topic: by_cases foo, {finish}


view this post on Zulip Adam Topaz (Feb 18 2021 at 18:35):

When writing proofs on paper it is very common to write something like this: We may assume that x0x \neq 0 since the x=0x = 0 follows easily, etc.

I can simulate this using

by_cases h : x = 0, { finish },
etc

This isn't bad, but I wonder whether we have a nicer way to do this that more closely resembles what I might write on paper.

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 21:37):

You could probably write a can_assume tactic which just throws the kitchen sink at the negation of what you assumed (perhaps after simplifying \not (x != 0) to x = 0 etc)

view this post on Zulip Mario Carneiro (Feb 18 2021 at 21:41):

I would do have : x = 0 := by by_contra; kitchen_sink

view this post on Zulip Ruben Van de Velde (Feb 18 2021 at 21:43):

Followed by "hold on, this isn't actually that trivial"?

view this post on Zulip Mario Carneiro (Feb 18 2021 at 21:43):

actually, I guess the pattern here is that you want to assume !A in goal P assuming A -> P

view this post on Zulip Mario Carneiro (Feb 18 2021 at 21:44):

It might not be the case that !A is provable

view this post on Zulip Mario Carneiro (Feb 18 2021 at 21:44):

That said, given all the spaces where you have to say things I don't think you can improve on the structure provided by by_cases

view this post on Zulip Eric Wieser (Feb 18 2021 at 22:30):

tactic#nontriviality is a special case of what you're asking for I think

view this post on Zulip Adam Topaz (Feb 18 2021 at 22:31):

Yeah, that's the "We may assume our ring is nontrivial, because the result is trivially true for the trivial ring" tactic.


Last updated: May 17 2021 at 15:13 UTC