function-def theorem idioms

Stream: new members

[Somo S.]

I have often found myself defining a function (for example, by well-founded recursion), and then needing to prove a chain of theorems about the its outputs; yet not being sure about what the best way to state the theorems is. Given the following kind of example, I would like some opinions about what is idiomatically the best way to state such theorems..

def BarFactory : Type → Type := sorry

def foo (arr : Array α) (left : Nat) (right : Nat)
    (h : right ≤ (arr.size - 1)) (bar : BarFactory α)
    : Array α :=
  sorry

variable {arr : Array α} {left right : Nat}
  {h : right ≤ arr.size - 1} {bar : BarFactory α}

-- The following are equivalent:
theorem foo_monotonic1 {f : Array α} (h : f = foo arr left right h bar := by rfl) :
    ∀ (i j : Nat) (_ : i < f.size) (_ : j < f.size),
    (left ≤ i) → (i < j) → (j ≤ right) → (f[i] ≤ f[j]) :=
  sorry

theorem foo_monotonic2 :
    let f := foo arr left right h bar;
    ∀ (i j : Nat) (_ : i < f.size) (_ : j < f.size),
    (left ≤ i) → (i < j) → (j ≤ right) → (f[i] ≤ f[j]) :=
  sorry

theorem foo_monotonic3 :
    ∀ (i j : Nat)
    (_ : i < (foo arr left right h bar).size)
    (_ : j < (foo arr left right h bar).size),
    (left ≤ i) → (i < j) → (j ≤ right) →
    ((foo arr left right h bar)[i] ≤ (foo arr left right h bar)[j]) :=
  sorry

things that may be of concern:

1. Readability: Should a statement try to minimize "noise", should one be able to easily understand what the statement means/says. For me, foo_monotonic2 is the easiest to read.
2. Usability: For the UI (func signature) for such a statement, does it matter that it has "nicer" ergonomics, from the standpoint of users of such a theorem statement. What's considered nicer in this regard? For me, foo_monotonic1 has been a bit easier to use.
3. Maintainability: if there are reptitive elements such as an application of the function several times with the same arguments, it useful to be DRY and abstract them away <see foo_monotonic2 and foo_monotonic2 >
4. Performance: are there typically elaboration performance costs/implications but stating it one way versus another.
5. perhaps there is an even better way to do these things than those exemplified above?

[Somo S.]

Here is another example that came up:

structure Part (α: Type u) where (arr' : Array α) (i' : Nat) (j' : Nat)
variable [LE α]

def part (arr: Array α) (i : Nat) (hi : i < arr.size)  (j : Nat) (hj : j < arr.size) (piv : α)
    (hxi : ∃ (i_ : Nat) (_ : i_ < arr.size), i ≤ i_ ∧ piv ≤ arr[i_])
    (hxj : ∃ (j_ : Nat) (_ : j_ < arr.size), j_ ≤ j ∧ arr[j_] ≤ piv) : Part α :=
  sorry

-- The following are equivalent:
theorem part_correctness_mid1
    {arr: Array α} {i : Nat} {hi : i < arr.size}  {j : Nat} {hj : j < arr.size} {piv : α}
    (hxi' : ∃ (i_ : Nat) (_ : i_ < arr.size), i ≤ i_ ∧ i_ ≤ j ∧ piv ≤ arr[i_])
    (hxj' : ∃ (j_ : Nat) (_ : j_ < arr.size), i ≤ j_ ∧ j_ ≤ j ∧ arr[j_] ≤ piv)
    (hlt : i < j)  (h : x = part arr i hi j hj piv sorry sorry := by rfl) :
    ∀ (p_ : Nat) (_ : p_ < x.arr'.size), x.j' < p_ → (p_  < x.i') → x.arr'[p_] = piv :=
  sorry

theorem part_correctness_mid2
    {arr: Array α} {i : Nat} {hi : i < arr.size}  {j : Nat} {hj : j < arr.size} {piv : α}
    (hxi' : ∃ (i_ : Nat) (_ : i_ < arr.size), i ≤ i_ ∧ i_ ≤ j ∧ piv ≤ arr[i_])
    (_ : ∃ (j_ : Nat) (_ : j_ < arr.size), i ≤ j_ ∧ j_ ≤ j ∧ arr[j_] ≤ piv)
    (hlt : i < j) : let x := part arr i hi j hj piv sorry sorry;
    ∀ (p_ : Nat) (_ : p_ < x.arr'.size), x.j' < p_ → p_  < x.i' → x.arr'[p_] = piv :=
  sorry

theorem part_correctness_mid3
    {arr: Array α} {i : Nat} {hi : i < arr.size}  {j : Nat} {hj : j < arr.size} {piv : α}
    (hxi' : ∃ (i_ : Nat) (_ : i_ < arr.size), i ≤ i_ ∧ i_ ≤ j ∧ piv ≤ arr[i_])
    (hxj' : ∃ (j_ : Nat) (_ : j_ < arr.size), i ≤ j_ ∧ j_ ≤ j ∧ arr[j_] ≤ piv)
    (hlt : i < j) : ∀ (p_ : Nat)
    (_ : p_ < (part arr i hi j hj piv sorry sorry).arr'.size),
    (part arr i hi j hj piv sorry sorry).j' < p_ →
    p_  < (part arr i hi j hj piv sorry sorry).i' →
    (part arr i hi j hj piv sorry sorry).arr'[p_] = piv :=
  sorry

In the case of part_correctness_mid3, couldn't elaborating the proofs for all the repeated sorry's be unnecessarily expensive as opposed to doing so in one place?

[Somo S.]

@Kim Morrison, I asked this yesterday at office hours. This is a follow up because I don't think I properly illustrated what my issues are and to make sure I understand what you suggested. To that end, were you suggesting that the best is for me just use style3 (foo_monotonic3/part_correctness_mid3) in each case?

[Kim Morrison]

I suggested that that you define a predicate that that statement can just apply to art arr i hi j hj piv sorry sorry.

[Hugh]

How can I prove behavior about a function that returns each choice from successive applications of an exists lemma? As a simpler example, I tried to prove this, but without luck:

def splitByN : List ℕ → List (List ℕ)
  | [] => []
  | x::xs =>
    let split := xs.splitAt x
    (x :: split.fst) :: splitByN split.snd
  termination_by x => x.length
  decreasing_by
    simp
    omega


theorem splitByNFlattenRfl : ∀ list : List ℕ,
  list = (splitByN list).flatten := by
  intro list
  induction' list using List.recOn with x xs ih
  · unfold splitByN
    rfl
  · sorry

[Edward van de Meent]

not sure what you mean with "exists lemma" in this case, but here's a solution to your MWE:

import Mathlib

def splitByN : List ℕ → List (List ℕ)
  | [] => []
  | x::xs =>
    let split := xs.splitAt x
    (x :: split.fst) :: splitByN split.snd
  termination_by x => x.length
  decreasing_by
    simp
    omega

theorem splitByNFlattenRfl : ∀ list : List ℕ,
  list = (splitByN list).flatten := by
  intro list
  fun_induction splitByN list with
  | case1 =>
    unfold splitByN
    rfl
  | case2 a b split ih2 =>
    rw [splitByN,List.flatten_cons]
    unfold split at *
    rw [← ih2, List.splitAt_eq]
    simp

[Hugh]

Much appreciated! Yeah I guess I was missing the idea of function induction. Here is the original problem for reference, I'm trying to prove a contradiction by showing that the mean of each splitList is greater than the original, and therefore the mean of their join is greater than the original. If there is a better way to approach this, please let me know! Otherwise I'll try to prove it using fun_induction.

noncomputable def splitList
  (original : List ℝ)
  (h₁ : ∀ k ≤ original.length,
  ∃ j ∈ Finset.range k, original.sum / original.length <
    (List.drop j (List.take k original)).sum / (k - j)
  )
   :=
  let rec splitListHelper := λ (m : ℕ) (m_le_len : m ≤ original.length) => by
    choose j j_le j_mean using h₁ m m_le_len
    let part := List.drop j (List.take m original)
    exact if j = 0
    then [part]
    else part :: splitListHelper j (by
      apply Nat.le_of_succ_le
      exact Nat.le_trans (List.mem_range.mp j_le) m_le_len
    )
    termination_by l => l
    decreasing_by
      simp_all [Finset.range]


  splitListHelper original.length (Nat.le_refl original.length)

theorem algebra_123 :
  ∀ list : List ℝ,
  ∃ k ≤ list.length,
  ∀ j ∈ Finset.range k,
  ((list.take k).drop j).sum / (k - j) ≤ list.sum / list.length
    := by
  intro original
  by_contra! h₁
  have splitListRfl : (splitList original h₁).flatten = original := by
    induction' original using splitList with x xs ih
    · simp at h₁