checking cases in `zmod 4`

Stream: maths

[Kevin Buzzard]

import tactic
import data.zmod.algebra

example (x y : zmod 4) (h: y ^ 2 = x ^ 3 - 1) : x = 1 :=
begin
  -- check all the cases
  fin_cases x; fin_cases y,
  /-
    16 goals, but -- disaster -- many are not in a good form.
    Example goal:

    h : bit1 ⟨1, _⟩ ^ 2 = ⟨1, _⟩ ^ 3 - 1
    ⊢ ⟨1, _⟩ = 1

  -/
end

I don't know how to break into cases whilst making the goals sensible. cases h makes progress but it takes a long time, and can time out when you try it 15 times. Is this a bug in fin_cases? Or is it something to do with the term of type fintype (zmod 4)?

[Adam Topaz]

if you dsimp at * it should clear those up

[Kevin Buzzard]

Oh I just found a hack:

example (x y : zmod 4) (h: y ^ 2 = x ^ 3 - 1) : x = 1 :=
begin
  -- check all the cases
  change fin 4 at x,
  change fin 4 at y,
  fin_cases x; fin_cases y,

[Michael Stoll]

dec_trivial! does this in one go.
Do you need all the cases specifically for some reason?

[Kevin Buzzard]

Thanks!

[Michael Stoll]

I've learnt this some while ago (through some of the community members on Zulip); I was also first trying fin_cases...

[Heather Macbeth]

@Kevin Buzzard I actually wrote a tactic for this a while ago, and then @Mario Carneiro wrote a better one! It's not PR'd, but by popular request it could be.

[Heather Macbeth]

https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/Code.20review.20for.20small.20tactic

[Kevin Buzzard]

Yeah I knew this had come up before but I didn't remember that! Thanks for letting me know!