i was thinking about this post by @fullmoon and pointfree adjacent stuff at the same time,¹ and it got me thinking about the almost moral difference between these two haskell functions:^2,3

composeList :: [a -> a] -> a -> a
composeList []     = id
composeList (f:fs) = composeList fs . f

composeList' :: [a -> a] -> a -> a
composeList' []     x = x
composeList' (f:fs) x = composeList' fs $ f x

for some reason, the first one is what i gravitated towards, yet i felt that the second one was somehow closer to the final result? i also underestimated the power of symbolic reasoning (which, and i'm really being serious, is extremely unlike me¹⁰), thinking that dhall could prove the second implementation was correct but not the first. i'm fairly certain it can; it has no problem reasoning about the identity function.

when i realized that, i felt pretty silly. why did i bother doing this with lean4 if dhall can do it easier? what's being gained from using a drastically more complex system (consistency is hard, even math kind of gives up most of the time)?

@[simp]
def composeList : List (α → α) → α → α
| [] => id
| (f::fs) => composeList fs ∘ f

@[simp]
def composeList' : List (α → α) → α → α
| [],      x => x
| (f::fs), x => composeList' fs (f x)

example : ∀(f g h : α → α), composeList [f,g,h] = (λx ↦ h (g (f x))) := by
  simp [Function.comp]

theorem property0
: ∀(f g h : α → α),
  composeList [f,g,h] = composeList' [f,g,h]
  ∧ composeList' [f,g,h] = (λx ↦ h (g (f x))) := by
  simp [Function.comp]

theorem property0.succ 
: ∀(fs : List (α → α)) x, 
  composeList fs x = composeList' fs x := by
  intro fs
  induction fs <;> simp [*]

^{^5}

here's why:⁹

theorem property0.succ 
: ∀(fs : List (α → α)) x, 
  composeList fs x = composeList' fs x := by
  intro fs
  induction fs <;> simp [*]

neat, right? no? don't see the point? that's understandable, nothing is really being gained by proving these two functions are equivalent. a far more compelling example is found in mathlib:

List of all permutations of l. This version of permutations is less efficient but has simpler definitional equations.

this makes me so happy! we can have faster functions and prove things about them using functions that are more canonical and easy to reason about it!¹¹

we can have our cake and eat it too, and all it takes is infinite universes!¹²