Zulip Chat Archive

Stream: new members

Topic: best way to split into cases


Jack J Garzella (Jul 10 2020 at 02:54):

I am trying to prove a theorem which splits into cases based on the degree of a polynomial. In particular, if f is my polynomial, I have seperate cases for if degree f is , 0, 1, or 2, and n+3, the final case requiring an induction. I have tried a few different approaches and haven't figured out a good way:

  • the cases tactic replaces the instances of degree f in my goal, instead of giving me a term of type degree f = ⊥ or degree f = 0, etc. I really need the term of type degree f = ..., so I tried hacking it in there with a variable (e.g. let n = degree f, have n = degree f, by simp [f], cases ...) but I still wasn't able to figure out how to finish the proof this way
  • the by_cases tactic gives me the proposition I want, but at the end I am left with a bunch of ¬degree f = ... assumptions, making for a messy proof by induction
  • if I try to switch into term mode and using a match statement like exact match ... end then Lean can't figure out any of the placeholders

Overall, it just feels clunky to not be able to match in tactic mode, instead having to eliminate on the option type and then three times in the match--is there a better way to do this?

Jalex Stark (Jul 10 2020 at 03:05):

Jack J Garzella said:

  • the by_cases tactic gives me the proposition I want, but at the end I am left with a bunch of ¬degree f = ... assumptions, making for a messy proof by induction

you can probably prove 3 \le degree f by omega

Jalex Stark (Jul 10 2020 at 03:05):

posting your code would help a lot here

Scott Morrison (Jul 10 2020 at 03:28):

perhaps by_cases h : degree f \le 2, and then interval_cases h?

Scott Morrison (Jul 10 2020 at 03:29):

You might also find it helpful to introduce a new n:nat, with h : n = degree f, and then do induction on n.

Kevin Buzzard (Jul 10 2020 at 14:07):

Possibly with some unfreezingI magic


Last updated: Dec 20 2023 at 11:08 UTC