How to dismiss impossible case in proof

Stream: new members

[Jakub Nowak]

When using if then else or match some of the cases I write are sometimes impossible. How can I write these cases, so that Lean is able to quickly find contradiction in those cases when splitting in proofs?

For the impossible cases I can use False.elim to dismiss the case as impossible. But then I have to copy-paste the False.elim in proof again.

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 if _ : b < a ∧ d < c then
    R' b a d c
  else False.elim (by
      have h := cases4 h_ab_ne h_cd_ne
      simp [*] at h
    )

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
  rotate_right
  exact False.elim (by
      have h := cases4 h_ab_ne h_cd_ne
      simp [*] at h
    )

[Aaron Liu]

You can use if_pos and if_neg (or dif_pos and dif_neg) instead of split

[Aaron Liu]

For this particular case you can also use contradiction and it will find the False.elim in your tactic state and extract the proof of False.

[Aaron Liu]

or at least that's what I thought it would do but it seems to not be working

[Jakub Nowak]

Yes, contradiction doesn't work here.

[Aaron Liu]

oh it works if you revert r first

[Robin Arnez]

Or, if you want to be fancy:

set_option linter.dupNamespace false in
def False.elim.elim {h : False} (_ : (False.elim h : Sort u)) : α := h.elim

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; rotate_right; exact r.elim

[Jz Pan]

I think the following is the same as your R:

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

and it looks better.

[Jz Pan]

Or even

def R (a b c d : ℚ) : Prop := a ≠ b ∧ c ≠ d ∧ R' (min a b) (max a b) (min c d) (max c d)

[Jakub Nowak]

Jz Pan said:

I think the following is the same as your R:

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

and it looks better.

That's how I wrote it at first, but it was even worse to use in proof. See #new members > How to write cases and split on them in proofs