Zulip Chat Archive

Stream: Is there code for X?

Topic: assume h and then prove cases for h and not h


view this post on Zulip Ariel Fridman (Feb 18 2021 at 10:26):

I am currently proving some (elementary) results about groups, and I got to a lemma where it would be easier to split into cases where g is equal to the identity element, and g is surely not the identity element.

Is there some kind of cases variant for such a thing? I am not a constructivist so if such a tactic only works in classical mode that's ok with me too.

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 10:26):

by_cases h : g = 1

view this post on Zulip Ariel Fridman (Feb 18 2021 at 10:27):

@Yakov Pechersky oops, now I feel bad that I haven't found it by myself, with such a simple naming ^^'. Thank you!

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 10:31):

Sometimes when I was learning I would just read through all of https://leanprover-community.github.io/mathlib_docs/tactics.html , but honestly it's easier to ask here :-)

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 10:32):

I actually find by_cases annoying sometimes, because the second case will be \not g = 1 rather than g \ne 1. I often do cases eq_or_ne g 1 in this situation (or whatever it's called)

view this post on Zulip Ariel Fridman (Feb 18 2021 at 10:33):

I first try searching the docs, of course. but sometimes you just miss stuff, or stuff is not documented in an easy-to-find way. This is probably not the case for by_cases though, that's just me ^^'.

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 10:34):

rcases eq_or_ne g 1 with rfl|h -- if eq_or_ne existed

to even skip the rw [h] step, and have g automatically be substituted with 1 everywhere.

view this post on Zulip Ariel Fridman (Feb 18 2021 at 10:34):

Kevin Buzzard said:

I actually find by_cases annoying sometimes, because the second case will be \not g = 1 rather than g \ne 1. I often do cases eq_or_ne g 1 in this situation (or whatever it's called)

hmm, I did a rename and change, but if this works then it sound better in this situation. Thanks for the tip!

view this post on Zulip Kevin Buzzard (Feb 18 2021 at 10:35):

I've said that, but now I think about it I'm usually in a situation where I want to split on <= or >, and I use le_or_gt because I don't want the second case to be "not le". I've just looked around a bit and I can't even find eq_or_ne and am now wondering if it even exists!

view this post on Zulip Ariel Fridman (Feb 18 2021 at 10:37):

I also tried to search through the docs, and couldn't see something like that, but it looks useful for these kind of situations. Is this something one can just PR into the language, or is there some RFC process for such a thing?

view this post on Zulip Yakov Pechersky (Feb 18 2021 at 10:37):

Kevin, are you working with solely with the naturals, and are doing cases k.zero_le.eq_or_lt and relying on the fact that 0 < k \iff 0 \ne k :upside_down:


Last updated: May 17 2021 at 15:13 UTC