(I do get your jest, but can't help to expand on it)
No, not of correctness, but only that the corresponding theorem is proven.
Example:
Function a: List -> b: List sorts list a, if b_i <= b_(i+1) for all i.
Then functions
duh _ = []
duh2 xs = [head xs | _ <- xs]
clearly satisfy that theorem.
So one needs to start with the correct theorem involving a proposition that the output list is necessarily a permutation of the input list. How does one prove the "correctness" of the theorem?
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
timeasmymeasure
no subject
Date: 2018-03-10 09:56 am (UTC)No, not of correctness, but only that the corresponding theorem is proven.
Example:
Function a: List -> b: List sorts list a, if b_i <= b_(i+1) for all i.
Then functions
duh _ = []
duh2 xs = [head xs | _ <- xs]
clearly satisfy that theorem.
So one needs to start with the correct theorem involving a proposition that the output list is necessarily a permutation of the input list. How does one prove the "correctness" of the theorem?