(x + 1 = y) → (x % 2 == 0) ≠ (y % 2 == 0)

Stream: Is there code for X?

[Iván Renison]

Does there is a prof of this or something similar to this?

theorem aux (x y : ℕ) (h : x + 1 = y) : (x % 2 == 0) ≠ (y % 2 == 0) := by
  sorry

I was able to prob it, but with a 30 lines prof

[Riccardo Brasca]

Can you please write a #mwe, with imports?

[Iván Renison]

Here is where I want to use it and how I is my prof:

import Mathlib.Combinatorics.SimpleGraph.Coloring
import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Data.ZMod.Basic


theorem aux {α : Type u} [BEq α] (x y : α) : (x != y) = !(x == y) := by
  exact rfl

theorem aux2 {α : Type u} [BEq α] (x y : α) : (x == y) = false ↔ (x != y) = true := by
  simp [aux]

theorem aux3 (n m : ℕ) : (n % 2 == 0) = (m % 2 == 0) ↔ n % 2 = m % 2 := by
  apply Iff.intro
  . intro (h : (n % 2 == 0) = (m % 2 == 0))
    cases h2: n % 2 == 0 with
    | true =>
      have h3 : n % 2 = 0 := by exact Nat.eq_of_beq_eq_true h2
      have h4 : (m % 2 == 0) = true := by simp_all only [beq_self_eq_true]
      have h5 : m % 2 = 0 := by simp_all only [beq_self_eq_true, beq_iff_eq]
      simp [h3, h5]
    | false =>
      have h3 : (n % 2 != 0) = true := by
        exact (aux2 (n % 2) 0).mp h2
      have h4 : n % 2 = 1 := by
        simp_all only [bne_iff_ne, ne_eq, Nat.mod_two_ne_zero]
      have h5 : m % 2 = 1 := by
        simp_all only [beq_eq_false_iff_ne, ne_eq, Nat.mod_two_ne_zero, bne_iff_ne]
      simp [h4, h5]
  . intro (h : n % 2 = m % 2)
    simp_all only

theorem aux4 (x : ℕ) : (x % 2 == 0) ≠ ((x + 1) % 2 == 0) := by
  simp [aux3]
  refine (ZMod.eq_iff_modEq_nat 2).not.mp ?_
  simp [*]

theorem aux5 (x y : ℕ) (h : x + 1 = y) : (x % 2 == 0) ≠ (y % 2 == 0) := by
  simp [h.symm]
  exact aux4 (x)

def SimpleGraph.pathGraph.bicoloring (n : ℕ)
    : SimpleGraph.Coloring (pathGraph n) Bool :=
  Coloring.mk (fun u => u.val % 2 == 0)
    (by
      intro u v h
      simp
      have h2 : u ⋖ v ∨ v ⋖ u := by simp_all [pathGraph]
      have h3 : u.val ⋖ v.val ∨ v.val ⋖ u.val := by simp_all [Fin.coe_covby_iff]
      have h4 : u.val + 1 = v.val ∨ v.val + 1 = u.val := by simp_all [Nat.covby_iff_succ_eq]
      match h4 with
        | Or.inl h' => exact aux5 u v h'
        | Or.inr h' => exact (aux5 v u h').symm
    )

[Mauricio Collares]

Would it help colouring with ZMod 2 instead of Bool?

[Riccardo Brasca]

Let me have a look.

[Riccardo Brasca]

This

import Mathlib.Combinatorics.SimpleGraph.Coloring
import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Data.ZMod.Basic

lemma foo (n : ℕ) : Even (n + 1) ↔ Odd n := by
  refine ⟨fun h ↦ ?_, fun h ↦ h.add_odd odd_one⟩
  by_contra' even
  rw [← Nat.even_iff_not_odd] at even
  exact Nat.odd_iff_not_even.1 (even.add_odd odd_one) h

theorem aux (x y : ℕ) (h : x + 1 = y) : (x % 2 == 0) ≠ (y % 2 == 0) := by
  intro H
  rw [Bool.eq_iff_eq_true_iff, beq_iff_eq] at H
  simp only [beq_iff_eq, ← h, ← Nat.even_iff, foo, Nat.odd_iff_not_even] at H
  by_cases even : Even x
  · refine H.1 even even
  · refine even (H.2 even)

works, but it can surely be golfed a little

[Riccardo Brasca]

foo is maybe somewhere

[Riccardo Brasca]

Ah, we have docs#Nat.even_add_one

[Riccardo Brasca]

import Mathlib.Combinatorics.SimpleGraph.Coloring
import Mathlib.Combinatorics.SimpleGraph.Hasse
import Mathlib.Data.ZMod.Basic

theorem aux (x y : ℕ) (h : x + 1 = y) : (x % 2 == 0) ≠ (y % 2 == 0) := by
  intro H
  rw [Bool.eq_iff_eq_true_iff, beq_iff_eq] at H
  simp only [beq_iff_eq, ← h, ← Nat.even_iff, Nat.even_add_one] at H
  exact not_iff_self H.symm

better

[Iván Renison]

Thank you