Transitive relations

Stream: new members

[Kate]

Hey all, I am trying to rewrite proofs from my uni report in Lean. This particular proof is showing how we can disprove a transitive relation by finding a counterexample. I am wondering if this is a good way to do it or if there are better ways to structure the proof in Lean. Any feedback would be appreciated as I am new to Lean and still trying to work out how to do things in it. Thanks!

def R (a b : ℤ) : Prop := Odd (a - b)
example : ¬ Transitive R := by
  unfold Transitive R
  intro h_transitive -- make the assumption that R is transitive
  have h1 : R 1 2 := by
    unfold R Odd -- ∃k, 1 - 3 = 2 * k + 1
    use -1
    ring_nf -- simplifies 1 - 2 to -1
  have h2 : R 2 3 := by
    unfold R Odd
    use -1
    ring_nf
  have h3 : R 1 3 := h_transitive h1 h2
  unfold R Odd at h3
  cases h3 with -- extract the integer k
  | intro k h3_eq -- assume 1 - 3 = 2 * k + 1
  have h_lhs : 1 - 3 = -2 := by ring_nf
  have h_rearrange : 2 * k = -3 := by linarith
  have h_mod1 : (-2) % 2 = 0 := by decide -- take h_lhs and get the remainder when divided by 2
  have h_mod2 : (2 * k) % 2 = 0 := by simp -- 2 * k is even
  rw[h_rearrange] at h_mod2 -- sub in 2 * k = -3
  contradiction -- -3 % 2 = 0 is a contradiction

[Jeremy Tan]

def R (a b : ℤ) : Prop := Odd (a - b)
example : ¬Transitive R := by
  unfold Transitive R; push_neg; use 1, 2, 3, by norm_num, by norm_num, by norm_num

[Kate]

oh wow that is much simpler!! Thank you

[Kate]

I have tried a similar approach with a different question but not quite getting it - hoping you or someone could take a look at it? This is my original attempt.

def R (a b : ℤ) : Prop := ∃ m : ℤ, a = m * b

example : ¬ Symmetric R := by
  unfold Symmetric
  intro h_symmetric
  have h1 : R 2 1:= by
    unfold R
    use 2
    rfl
  have h2 : R 1 2 := h_symmetric h1
  unfold R at h2
  cases h2 with
  | intro m h_eq
  have h_mod : 1 % 2 = 1 := by decide -- 1 is not divisible by 2
  have h_mod2 : (m * 2) % 2 = 0 := by simp -- any multiple of 2 is divisible by 2
  symm at h_eq -- make m * 2 the first term
  rw [h_eq] at h_mod2
  contradiction

[Aaron Liu]

import Mathlib

def R (a b : ℤ) : Prop := ∃ m : ℤ, a = m * b

example : ¬ Symmetric R := by
  intro h
  specialize @h 0 1 ⟨0, by norm_num⟩
  obtain ⟨y, hy⟩ := h
  simp at hy

[Aaron Liu]

It's a lot easier to use 0 and 1 here