Working with `Even` and `Odd`

Stream: general

[Matthew Pocock]

I've been struggling to work with the Even and Odd rules. They often seem to behave as if they are opaque to other tactics, and Odd n keeps getting simplified to ¬Even n when I'm not looking, preventing simplification rules defined in terms of Odd n from working.

⊢  ¬Even n → Even (if Even n then n / 2 else 3 * n + 1)

So for example, this target won't simplify out the if/else case. To get simp to start to work on it, I have to do quite a lot of work by hand to unpack the evens, by which time something have gotten themselves messy. It should be obvious that this can be simpified as-is to 3 * n + 1.

But it's worse than that. What I actually wanted to work with was:

⊢ Odd n → Even (if Even n then n / 2 else 3 * n + 1)

I actually need the witness for Odd n to provide the witness to the outer Even _. But the simplifier eagerly flips it, loosing the witness in the process.

Am I doing things wrongly? It feels like I'm fighting the library which is usually a sign that I'm not using it as intended.

[Yaël Dillies]

Nat.odd_iff_not_even. Let me fix that.

[Kevin Buzzard]

In this particular case you probably do want "not even n" because you can then intro h; rw [if_neg h] to simplify the if/then.

[Matthew Pocock]

Kevin Buzzard said:

In this particular case you probably do want "not even n" because you can then intro h; rw [if_neg h] to simplify the if/then.

OK, but I also need the outer Odd, as I need to get its existential -- I need that variable to unify at the other end to prove the rhs Even constraint.

[Kevin Buzzard]

Maybe post a #mwe to better explain your question? This is by far the most efficient way to ask a Lean question.

[Matthew Pocock]

This was the code I ended up with in the end. I'm not particularly happy with it, particularly the step where I do some gymnastics to reduce the if statement.

import Mathlib.Tactic

variable (n : Nat)

def collatz := if Even n then n / 2 else 3 * n + 1

theorem collatz_odd_to_even : Odd n -> Even (collatz n) := by
    intro hon
    rw [collatz]
    simp [Iff.mp Nat.odd_iff_not_even hon] -- reduce the if statement
    obtain ⟨ x, rfl ⟩ := hon
    rw [Even]
    use 3 * x + 2
    simp [←Nat.two_mul, mul_add, ←mul_assoc]

[Kevin Buzzard]

If you abuse definitional equality and use ring you can get your version down to this:

theorem collatz_odd_to_even : Odd n -> Even (collatz n) := by
  intro hon
  simp only [collatz, Iff.mp Nat.odd_iff_not_even hon, ite_false] -- reduce the if statement
  obtain ⟨ x, rfl ⟩ := hon
  use 3 * x + 2
  ring

[Kevin Buzzard]

Here's a version which avoids the Iff.mp thing:

theorem collatz_odd_to_even : Odd n -> Even (collatz n) := by
  intro hon
  have h : ¬ Even n := by simpa using hon
  rw [collatz, if_neg h]
  obtain ⟨ x, rfl ⟩ := hon
  use 3 * x + 2
  ring

[Matthew Pocock]

Thanks! The ring tactic is a godsend here. I wish I'd known about it sooner.

[Eric Rodriguez]

there's a parity_simps simp-set somewhere

[Bhavik Mehta]

Yaël Dillies said:

Nat.odd_iff_not_even. Let me fix that.

Yeah this being simp has annoyed me very often, I don't think it's particularly good as a simp lemma

[Matthew Pocock]

Can I enable parity_simps locally within a file? I tried attribute [local simp] parity_simps but it didn't seem to like that. Also, can I disable Nat.odd_iff_not_even from being considered as a simp within my file? I can put parity_simps within a simp, but I can't see how to just enable it everywhere.

[Alex J. Best]

As far as a I know that's not possible directly at the moment, you could easily define a macro that does simp [parity_simps] though, but making a version of that that's more flexible might be more trouble than it's worth depending how long your file is.

[Kevin Buzzard]

parity_simps is a simp set, not one lemma, so I doubt attribute [local simp] parity_simps will work. For removing simp does attribute [-simp] Nat.odd_iff_not_even work? A more aggressive approach would be to PR the change removing simp from that lemma becasue people have complained before about it being in the simp set.

[Kyle Miller]

I'm not aware of it, but it seems like it'd be a reasonable command to add to mathlib (where you take every lemma in a simp set and give it the simp attribute locally). Feel free to create a mathlib4 issue describing what you want and what problems this solves.

[Kyle Miller]

While on the face of it it doesn't seem that saving the extra keystrokes in simp [parity_simps] is worth it, there's automation that calls simp so this command would enable that automation to use parity_simps lemmas locally.

[Matthew Pocock]

https://github.com/leanprover-community/mathlib4/issues/7082
https://github.com/leanprover-community/mathlib4/issues/7083