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.