Dismiss absurd case in if-else definition

Stream: new members

[Vivek Rajesh Joshi]

I have a function defined in terms of cases, where one of the cases is an absurdity. How do I dismiss the case, i.e. tell the function "Don't worry, you won't have to evaluate that case"?

[Ruben Van de Velde]

Can you show some code? (read #mwe for best results)

[Vivek Rajesh Joshi]

I'm a bit hesitant to show the code because of how messy it is, but here ya go:

import Mathlib.Data.Matrix.Notation

variable (M : Matrix (Fin m) (Fin n) Rat) (hm : m>0) (hn : n>0)

abbrev colListofMat := List.map List.ofFn (List.ofFn M.transpose)

def list_allZero (l : List Rat) : Bool := l.all (fun x => (x==0))

def findNonzCol : ℕ := (colListofMat M).findIdx (fun col => ¬ list_allZero col)

lemma findIdx_eq_length_of_notExists (l : List α) (p : α → Bool) (hl : ∀ x∈l, p x = false) : l.findIdx p = l.length := by
  contrapose hl
  push_neg at *; simp

lemma findIdx_le_length (l : List α) (p : α → Bool) : l.findIdx p ≤ l.length := by
  by_cases h : (∃ x∈l, p x)
  exact le_of_lt (List.findIdx_lt_length_of_exists h)
  push_neg at h; simp at h
  exact le_of_eq (findIdx_eq_length_of_notExists l p h)

lemma findNonzCol_le_numCol : (findNonzCol M) ≤ (colListofMat M).length := by
  unfold findNonzCol
  apply findIdx_le_length (colListofMat M) (fun col => ¬list_allZero col)

lemma nonzListHasNonz (h : ¬list_allZero l) : ∃ x∈l, x≠0 := by
  unfold list_allZero at h
  rw [List.all_eq_true] at h
  push_neg at h
  convert h; simp

lemma findNonzCol_get_HasNonz (h : findNonzCol M < (colListofMat M).length) :
  ∃ x ∈ (colListofMat M).get ⟨findNonzCol M,h⟩, x≠0 := by
  unfold findNonzCol at h
  have := List.findIdx_get (w:=h)
  simp only [Bool.not_eq_true, Bool.decide_eq_false] at this
  rw [Bool.not_iff_not] at this
  obtain ⟨x,hx,xn0⟩ := nonzListHasNonz this
  use x
  constructor
  unfold findNonzCol
  convert hx; simp
  assumption

def findPivot : Rat :=
    if h1 : findNonzCol M = (colListofMat M).length then 1
    else
      if h2 : findNonzCol M < (colListofMat M).length then
        let pcol := (colListofMat M).get ⟨findNonzCol M,indlt⟩
        have h3 : pcol.findIdx (fun x => x≠0) < pcol.length := by
          have h4 := findNonzCol_get_HasNonz M h2
          apply List.findIdx_lt_length_of_exists h4
        pcol.get ⟨pcol.findIdx (fun x => x≠0),h3⟩
      else
        have h4 := findNonzCol_le_numCol M
        Or.elim (eq_or_lt_of_not_lt h2) (fun h => absurd h h1) (fun h => absurd h4 (not_le_of_gt h))

Ignore the h2 block. The problem lies in the else of the h2 block

[Luigi Massacci]

Or.elim can only eliminate into Prop. Using absurd was the right idea though: eg you could replace your last line with something like

have nh4 := not_le.mpr (lt_of_le_of_ne (not_lt.mp h2) (Ne.symm h1))
absurd h4 nh4

[Vivek Rajesh Joshi]

That works, thanks a lot!

[Vivek Rajesh Joshi]

Another sub-doubt, if you don't mind - how do I unfold the pcol definition in the goal for the have h3: block?

[Kevin Buzzard]

unfold pcol?

[Vivek Rajesh Joshi]

unknown constant 'pcol'

[Matthew Ballard]

unfold_let?

[Vivek Rajesh Joshi]

Yes, that works. Thank you!