How to write cases and split on them in proofs

Stream: new members

[Jakub Nowak]

Here's a code I wrote:

import Mathlib

def sorted (a b c d : ℚ) : Prop := a < b ∧ a < c ∧ a < d ∧ b < c ∧ b < d ∧ c < d

def R' (a b c d : ℚ) : Prop :=
  a < b ∧ c < d → sorted a c d b ∨ sorted c a b d ∨ sorted a b c d ∨ sorted c d a b
def R (a b c d : ℚ) : Prop :=
  a ≠ b ∧ c ≠ d ∧ R' a b c d ∧ R' b a c d ∧ R' a b d c ∧ R' b a d c

example : R a b c d → R a⁻¹ b⁻¹ c⁻¹ d⁻¹ := by
  intro r
  unfold R R' at r
  obtain ⟨h_ab_ne, h_cd_ne, ri⟩ := r

  obtain p | p | p | p : a < b ∧ c < d ∨ b < a ∧ c < d ∨ a < b ∧ d < c ∨ b < a ∧ d < c := by
    rcases lt_or_gt_of_ne h_ab_ne with _ | _
    <;> rcases lt_or_gt_of_ne h_cd_ne with _ | _
    <;> simp [*]
  focus obtain ⟨ri, -, -, -⟩ := ri
  rotate_left
  focus obtain ⟨-, ri, -, -⟩ := ri
  rotate_left
  focus obtain ⟨-, -, ri, -⟩ := ri
  rotate_left
  focus obtain ⟨-, -, -, ri⟩ := ri
  rotate_left
  all_goals have ri := ri p
  all_goals rename_i r'
  all_goals clear r'

Relation R says that two intervals are either one fully contained in the other or don't intersect.
The definition of R I wrote distinguishes four cases namely
a < b ∧ c < d ∨ b < a ∧ c < d ∨ a < b ∧ d < c ∨ b < a ∧ d < c.
In the proof I wanted to split the goal into those four cases, but that required me to write the kind of code as seen above:

  focus obtain ⟨ri, -, -, -⟩ := ri
  rotate_left
  focus obtain ⟨-, ri, -, -⟩ := ri
  rotate_left
  focus obtain ⟨-, -, ri, -⟩ := ri
  rotate_left
  focus obtain ⟨-, -, -, ri⟩ := ri
  rotate_left

Is it possible to make this simpler, possibly by modifying the definition of R?

[Eric Paul]

This may not be helpful for the part you're asking about, but at least for stating the definition of R, it might be easier if you talk about the intervals themselves

import Mathlib

def R' (A B : Set ℚ) := Disjoint A B ∨ A ⊆ B ∨ B ⊆ A
def R (a b c d : ℚ) := R' (Set.uIcc a b) (Set.uIcc c d)

[Jakub Nowak]

That kinda works:

import Mathlib

lemma cases4 {a b c d : ℚ} (h_ab_ne : a ≠ b) (h_cd_ne : c ≠ d) : a < b ∧ c < d ∨ b < a ∧ c < d ∨ a < b ∧ d < c ∨ b < a ∧ d < c := by
    rcases lt_or_gt_of_ne h_ab_ne with _ | _
    <;> rcases lt_or_gt_of_ne h_cd_ne with _ | _
    <;> simp [*]

opaque R' (a b c d : ℚ) : Prop
def R (a b c d : ℚ) : Prop := ∃ (h_ab_ne : a ≠ b) (h_cd_ne : c ≠ d),
  if _ : a < b ∧ c < d then
    R' a b c d
  else if _ : b < a ∧ c < d then
    R' b a c d
  else if _ : a < b ∧ d < c then
    R' a b d c
  else
    have : b < a ∧ d < c := by
      have h := cases4 h_ab_ne h_cd_ne
      simp [*] at h
      exact h
    R' b a d c

example : R a b c d → R a⁻¹ b⁻¹ c⁻¹ d⁻¹ := by
  intro r
  unfold R at r
  obtain ⟨h_ab_ne, h_cd_ne, r⟩ := r

  split_ifs at r <;> try extract_lets at r

[Jz Pan]

I think you need to revise your definitions.

[Jz Pan]

The very first definition sorted already seems not good to me. Isn't a < b ∧ b < c ∧ c < d enough? The remaining 3 conditions are superfluous.

[Jakub Nowak]

Jz Pan said:

The very first definition sorted already seems not good to me. Isn't a < b ∧ b < c ∧ c < d enough? The remaining 3 conditions are superfluous.

Listing all inequalities helps simp tactic to automatically prove goals, as it cannot derive these automatically. I also have this theorem to make it easier to prove sorted ..:

@[simp]
theorem sorted_easier {a b c d : ℚ} (_ : a < b) (_ : b < c) (_ : c < d) : sorted a b c d := by
  split_ands <;> linarith

Although, I think what would also work essentially the same, I could use the simpler definition of sorted and add six theorems for deriving inequalities from sorted ... Actually, that could be slightly more elegant, as with this approach I wouldn't have to unfold sorted.

[Kenny Lau]

This already highlights a very important distinction between "use" and "prove". In mathlib we want to have basically two versions of everything, the one with the most information that you can "use" from, and the one with the least information that you can "prove" easily.

[Kenny Lau]

This is the core of the dot notation and custom projections and custom constructors

[Kenny Lau]

this is also known as the "API"