История изменений

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

То это проблема не статических систем типов, а программирования в целом (и даже значительно шире, если честно). В программировании запросто может оказаться что ты пишешь вообще не то что нужно. И у меня так несколько раз было (на пхп/яваскрипте ещё).

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте? При этом логические спецификации читаются по-моему гораздо лучше. Т.е. ошибку с точки зрения корректности требований (т.е. с точки зрения «потребителя» или «клиента», т.е. того кому функция нужна в итоге для использования) найти по-моему проще в типе argmax_correct выше, чем в контракте.

Если брать данный конкретный случай, то сначала я ошибся в написании inner, а потом на спецификации inner_correct, и не мог доказать. И не доказал до тех пор пока не разобрался что именно не так и не поправил. Т.е. в некотором смысле это критерий - если не получается доказать (а вообще то должно доказываться), то вероятнее всего что то не так либо с функцией либо со спекой. Конечно, можно неудачно сформулировать и зависнуть, но это больше уже дело опыта, кмк.

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

То это проблема не статических систем типов, а программирования в целом (и даже значительно шире, если честно). В программировании запросто может оказаться что ты пишешь вообще не то что нужно. И у меня так несколько раз было (на пхп/яваскрипте ещё).

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте? При этом логические спецификации читаются по-моему гораздо лучше. Т.е. ошибку с точки зрения корректности требований (т.е. с точки зрения «потребителя» или «клиента», т.е. того кому функция нужна в итоге для использования) найти по-моему проще в типе argmax_correct выше, чем в контракте.

Если брать данный конкретный случай, то я затупил на спецификации inner_correct, и не мог доказать. И не доказал до тех пор пока не разобрался что именно не так и не поправил спецификацию. Т.е. в некотором смысле это критерий - если не получается доказать (а вообще то должно доказываться), то вероятнее всего что то не так либо с функцией либо со спекой. Конечно, можно неудачно сформулировать и зависнуть, но это больше уже дело опыта, кмк.

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

То это проблема не статических систем типов, а программирования в целом (и даже значительно шире, если честно). В программировании запросто может оказаться что ты пишешь вообще не то что нужно. И у меня так несколько раз было (на пхп/яваскрипте ещё).

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте? При этом логические спецификации читаются по-моему гораздо лучше. Т.е. ошибку с точки зрения корректности требований найти по-моему проще в типе argmax_correct выше, чем в контракте.

Если брать данный конкретный случай, то я затупил на спецификации inner_correct, и не мог доказать. И не доказал до тех пор пока не разобрался что именно не так и не поправил спецификацию. Т.е. в некотором смысле это критерий - если не получается доказать (а вообще то должно доказываться), то вероятнее всего что то не так либо с функцией либо со спекой. Конечно, можно неудачно сформулировать и зависнуть, но это больше уже дело опыта, кмк.

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

То это проблема не статических систем типов, а программирования в целом (и даже значительно шире, если честно). В программировании запросто может оказаться что ты пишешь вообще не то что нужно. И у меня так несколько раз было (на пхп).

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте? При этом логические спецификации читаются по-моему гораздо лучше. Т.е. ошибку с точки зрения корректности требований найти по-моему проще в типе argmax_correct выше, чем в контракте.

Если брать данный конкретный случай, то я затупил на спецификации inner_correct, и не мог доказать. И не доказал до тех пор пока не разобрался что именно не так и не поправил спецификацию. Т.е. в некотором смысле это критерий - если не получается доказать (а вообще то должно доказываться), то вероятнее всего что то не так либо с функцией либо со спекой. Конечно, можно неудачно сформулировать и зависнуть, но это больше уже дело опыта, кмк.

В общем-то всё доказалось, там не очень сложно. Запутался скорее от недостатка опыта (плюс ошибку сделал при определении inner, в коде выше правда кажется уже поправлено). Попробую сделать орд вместо нат.

Спецификация осталась та же по моему (только я более общий тип добавил для списка).

Fixpoint argmax (A : Type) (default : A) (f : A -> nat) (xs : list A) : A :=
  match xs with
  | [] => default
  | [x] => x
  | x::xs => inner (f x) x f xs
  end
with inner (A : Type) (s : nat) (r : A) (f : A -> nat) (xs : list A) : A :=
       match xs with
       | [] => r
       | x::xs' => let fx := f x in
                 if s <? fx
                 then inner fx x f xs'
                 else inner s r f xs'
       end.

Theorem argmax_correct (A : Type) (d x : A) (f : A -> nat) (xs : list A) :
    argmax d f xs = x ->
    ((xs = [] /\ x = d) \/
     exists ix, nth_error xs ix = Some x /\
           (forall y iy, nth_error xs iy = Some y -> f y < f x \/ ix <= iy)).
Proof. Admitted.

Вот это настоящая проблема достаточно мощных статических систем типов. Что-то чуть более нетривиальное, чем сортировку доказать крайне сложно. Можно написать assume, но в контракты времени выполнения условие не сконвертируется и вполне может оказаться ложным.

То это проблема не статических систем типов, а программирования в целом. Запросто может оказаться что ты пишешь вообще не то что нужно. И у меня так много раз было.

Если брать контракты, то те же яйца вид сбоку: что мешает сделать ошибку в контракте? При этом логические спецификации читаются по-моему гораздо лучше. Т.е. ошибку с точки зрения корректности требований найти по-моему проще в типе argmax_correct выше, чем в контракте.

Если брать данный конкретный случай, то я затупил на спецификации inner_correct, и не мог доказать. И не доказал до тех пор пока не разобрался что именно не так и не поправил спецификацию. Т.е. в некотором смысле это критерий - если не получается доказать (а вообще то должно доказываться), то вероятнее всего что то не так либо с функцией либо со спекой. Конечно, можно неудачно сформулировать и зависнуть, но это больше уже дело опыта, кмк.