Shorten if-else statements

Stream: new members

[Vivek Rajesh Joshi]

How do I use ∧ and ∨ to shorten this if-else part of a definition?

if h2 : (isRowReduced_row a).1 then
        (isRowReduced_col (cl.get ⟨(((isRowReduced_row a).2).getD 0),((h ⟨0,Nat.zero_lt_succ as.length⟩) ▸ indLastOne_lt_rowLength a h2 h1)⟩)) ∨
          isRowReducedAux as cl (by intro i; have := h (i.castSucc); rw [← (h0' i)] at this; exact this)
      else false

(isRowReduced_row a).1 is of type Bool

[Kyle Miller]

If you have a #mwe you might get an answer, but I'm not sure what the goal is — why do you want it shorter?

[Vivek Rajesh Joshi]

No particular reason, I'm just seeing if I can get rid of the else false
Here's an mwe:

import Mathlib.Data.Matrix.Notation
import Mathlib.Data.Matrix.Basis

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

abbrev rowListofMat := List.map List.ofFn (List.ofFn M)

lemma rowListLength_eq_numRow : (rowListofMat M).length = m := by simp

lemma rowListofMat_elt_length_eq_numCol : ∀ i, ((rowListofMat M).get i).length = n := by simp

lemma rowLengthEq : ∀ i j, (List.ofFn (M i)).length = (List.ofFn (M j)).length := by simp

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

lemma colListLength_eq_numCol : (colListofMat M).length = n := by simp

def row_allZerosBeforeFirstOne (row : List Rat) : Bool :=
  List.isPrefixOf (List.replicate (row.indexOf 1) 0) row

def isRowReduced_row (ri : List Rat) : Bool×(Option Nat) :=
  if ri.all (fun x => x==0) then (true,none)
  else
    if ri.indexOf 1 = ri.length then (false,none)
    else
      if row_allZerosBeforeFirstOne ri then (true,ri.indexOf 1)
      else (false,none)

def isRowReduced_col (cj : List Rat) : Bool := List.all (List.erase cj 1) (fun x => x==0)

lemma indFirstOne_lt_rowLength (rl : List Rat) (h : (isRowReduced_row rl).1 = true) (h' : ¬(rl.all (fun x => x==0))) :
  (((isRowReduced_row rl).2).getD 0) < rl.length := by
  unfold isRowReduced_row
  split_ifs with h1 h2
  · have : (isRowReduced_row rl).1 == false := by unfold isRowReduced_row; rw [if_neg h', if_pos h1]; rfl
    simp at h this; rw [h] at this; contradiction
  · show rl.indexOf 1 < rl.length
    apply List.indexOf_lt_length.mpr
    rcases lt_or_gt_of_ne h1 with indlt|indgt
    exact List.indexOf_lt_length.mp indlt
    have l1 := rl.indexOf_le_length (a:=1)
    have nl1 := not_le_of_gt indgt
    contradiction
  · have : (isRowReduced_row rl).1 == false := by
      unfold isRowReduced_row; rw [if_neg h', if_neg h1, if_neg h2]; rfl
    simp at h this; rw [h] at this; contradiction

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

def isRowReducedAux (rl : List (List Rat)) (cl : List (List Rat)) (h : ∀ i, (rl.get i).length = cl.length) : Bool :=
  match rl with
  | [] => true
  | a::as =>
    have h0 : ∀ i, as.get i ∈ as := by intro i; rw [as.mem_iff_get]; use i
    have h0' : ∀ i, (as.get i).length = ((a::as).get i.castSucc).length := by
      intro i
      obtain ⟨n,hn⟩ := ((a::as).mem_iff_get).mp ((List.subset_cons a as) (h0 i))
      have l1 := h (Fin.castSucc i); have l2 := h n; rw [←l1, hn] at l2; exact l2
    if h1 : list_allZero a then isRowReducedAux as cl (by intro i; have := h (i.castSucc); rw [← (h0' i)] at this; exact this)
    else
      if h2 : (isRowReduced_row a).1 then
       (isRowReduced_col (cl.get ⟨(((isRowReduced_row a).2).getD 0),((h ⟨0,Nat.zero_lt_succ as.length⟩) ▸ indFirstOne_lt_rowLength a h2 h1)⟩)) ∨
          isRowReducedAux as cl (by intro i; have := h (i.castSucc); rw [← (h0' i)] at this; exact this)
      else false

[Kevin Buzzard]

If you're asking "is if...then without else valid syntax" then the answer is "no". If not, then what are you asking?

[Vivek Rajesh Joshi]

For example, if P then True else if ¬Q then False else R can be shortened to P ∨ (Q ∧ R) . Can something like that be done here?

[Yaël Dillies]

Yes, you can do ∃ h2 : (isRowReduced_row a).1, (isRowReduced_col (cl.get ⟨(((isRowReduced_row a).2).getD 0),((h ⟨0,Nat.zero_lt_succ as.length⟩) ▸ indFirstOne_lt_rowLength a h2 h1)⟩)) ∨ isRowReducedAux as cl (by intro i; have := h (i.castSucc); rw [← (h0' i)] at this; exact this)

[Yaël Dillies]

More clearly, if h : P then Q h else False is equivalent to ∃ h : P, Q h

[Vivek Rajesh Joshi]

Ohh okay, that's what I wanted. Thanks a lot!