Simplifying match and projection

Stream: lean4

[pandaman]

Hi. I have the following function:

def f {α : Type} (arr : Array α) (i j : Nat) : { m : Nat // i ≤ m ∧ m ≤ j } × Array α := sorry

When proving a theorem involving the function, I wanted to simplify a term with match and the projection like this, but simp couldn't process it.

theorem motive {α : Type} (arr : Array α) (i j : Nat) :
  (match f arr i (j - 1) with
  | (⟨mid, ⟨hmid₁, hmid₂⟩⟩, arr) => (⟨mid, ⟨hmid₁, Nat.le_trans hmid₂ (Nat.sub_le ..)⟩⟩, arr)
  : { mid : Nat // i ≤ mid ∧ mid ≤ j } × Array α).snd = (f arr i (j - 1)).snd := by
  -- simp made no progress
  sorry

It seems that the ⟨hmid₁, hmid₂⟩ part is the culprit, so this version worked:

theorem motive' {α : Type} (arr : Array α) (i j : Nat) :
  (match f arr i (j - 1) with
  | (⟨mid, hm⟩, arr) => (⟨mid, ⟨hm.left, Nat.le_trans hm.right (Nat.sub_le ..)⟩⟩, arr)
  : { mid : Nat // i ≤ mid ∧ mid ≤ j } × Array α).snd = (f arr i (j - 1)).snd := by
  simp

Out of curiosity, I would like to know

1. Why the first version didn't work?
2. If we don't want to change the definition, how we can make the first version work?

Thanks!

[pandaman]

A similar instance of the issue (sorry, couldn't minimize this). Consider the following definition of quickSortImpl.

abbrev Vec (α : Type) (n : Nat) := { arr : Array α // arr.size = n }

def partition {α : Type} [Ord α]
  {n : Nat} (arr : Vec α n) (first last : Nat)
  (fl : first ≤ last) (ln : last < n) :
  { mid : Nat // first ≤ mid ∧ mid ≤ last } × Vec α n := sorry

def quickSortImpl {α : Type} [Ord α]
  {n : Nat} (arr : Vec α n) (first last : Nat) (ln : last < n) :
  Vec α n :=
  if lt : first < last then
    match partition arr first last (Nat.le_of_lt lt) ln with
    | (⟨mid, ⟨hmid₁, hmid₂⟩⟩, arr) =>
      -- Lemmas
      have : mid - 1 - first < last - first :=  sorry
      have : last - (mid + 1) < last - first := sorry
      have : mid - 1 < n := sorry

      -- Recursion
      let arr := quickSortImpl arr first (mid - 1) (by assumption)
      quickSortImpl arr (mid + 1) last ln
  else
    arr
termination_by _ => last - first

When proving a theorem about the function, I got a term like this, which simp cannot proceed with destructuring the match:

-- def P (arr : Vec α n) : Prop := sorry

-- I want to show this
P (match partition arr first last (_ : first ≤ last) ln with
  | ({ val := mid, property := (_ : first ≤ mid ∧ mid ≤ last) }, arr) =>
    quickSortImpl (quickSortImpl arr first (mid - 1) (_ : mid - 1 < n)) (mid + 1) last ln)

However, when I removed the use of match in quickSortImpl, somehow I could get a nicer term:

-- Given this definition
def quickSortImpl {α : Type} [Ord α]
  {n : Nat} (arr : Vec α n) (first last : Nat) (ln : last < n) :
  Vec α n :=
  if lt : first < last then
    -- Do not use match
    let parted := partition arr first last (Nat.le_of_lt lt) ln
    let mid := parted.1.val
    let hm := parted.1.property
    let arr := parted.2

    -- Lemmas
    have : mid - 1 - first < last - first := termination_lemma lt hm.1 hm.2
    have : last - (mid + 1) < last - first := Nat.sub_lt_sub_left lt (Nat.lt_of_le_of_lt hm.1 (Nat.lt_succ_self ..))
    have : mid - 1 < n := Nat.lt_of_le_of_lt (Nat.sub_le ..) (Nat.lt_of_le_of_lt hm.2 ln)

    -- Recursion
    let arr := quickSortImpl arr first (mid - 1) (by assumption)
    quickSortImpl arr (mid + 1) last ln
  else
    arr

-- I got this, which I could prove by recursion on P.
P (quickSortImpl
    (quickSortImpl (partition arr first last (_ : first ≤ last) ln).snd first
      ((partition arr first last (_ : first ≤ last) ln).fst.val - 1)
      (_ : (partition arr first last (_ : first ≤ last) ln).fst.val - 1 < n))
    ((partition arr first last (_ : first ≤ last) ln).fst.val + 1) last ln)

[pandaman]

Is this kind of use of match to deconstruct nested data structures not recommended?