История изменений
Исправление AndreyKl, (текущая версия) :
Я привёл пример функции f
Ты привёл пример функции для которой никто ничего доказать не сможет кроме как перебором, кроме некоторых частных случаев. (ну или вот я приводил, может верное доказательство, но тогда мужик один из первых и немногих кто вообще для этой функции что то более-менее доказал)
И попросил меня доказать для неё что-то. Смотри: доказательства на Коке почти не отличаются от доказательств в обычной математике. Есть некоторая специфика, конечно. Может быть, пожалуй, наиболее заментая - это большая подробность - там где в математике ты просто скажешь «ну понятно», в коке придётся всё таки дать доказательство.
Теперь мне кажется ты можешь согласится что наивно ожидать что кто-то в принципе даст тебе доказательство того, доказательство чего не дали лучшие математики. Я думаю теперь должно быть понятно почему пример неудачный. Просто для этой функции не докажет никто и нечего. Такая функция.
Почему реализовывать перебор на Коке странно я тоже уже постарался вроде объяснить. Перебирать лучше на чём то что более подходит для перебора.
Фактически, доказывается только для аналога цикла for (в диапазоне или в коллекции).
Отнюдь. Но это довольно простой случай. И наверное наиболее частый (в некоторых вариациях).
Вот такое (Integrate), я так понимаю, тоже доказать нельзя будет:
Всё сводится к «обычной» математике. Если можешь доказать сходимость этого интрегрирования (формально, на математическом языке), на Коке тоже скорее всего всё получится. Правда доказательств для численных методов я лично никогда не касался.
После вышесказанного. При попытке доказать функциональную корректность у меня почему то получается что f в нуле виснет. Это я что то напутал или так и задумано?
Require Import Arith.
Require Import Bool.Bool.
Open Scope nat_scope.
Variable onehmlr : nat.
Axiom onehmrl_eq : onehmlr = 100000000000.
#[bypass_check(guard=yes)]
Fixpoint f(k : nat) : nat :=
if k =? 1 then 1
else
if negb (k <=? onehmlr) then 0
else
if k mod 2 =? 0 then f (k/2)
else f (3*k+1).
Fixpoint model_f (k fuel : nat) {struct fuel} : option nat :=
match fuel with
| O => None
| S fuel =>
if k =? 1 then Some 1
else if negb (k <=? onehmlr) then Some 0
else if k mod 2 =? 0 then model_f (k/2) fuel
else model_f (3*k+1) fuel
end.
Locate unint.
Opaque onehmlr.
Lemma leb0true n : 0 <=? n = true.
Proof.
destruct n; reflexivity.
Qed.
Lemma eq_f_model_f k fuel : k < onehmlr -> fuel < onehmlr -> fuel > 0 -> model_f k fuel = Some (f k).
Proof.
induction fuel.
intros. inversion H1.
intros. destruct k.
unfold model_f. cbv fix. cbv beta. cbv iota.
fold (model_f (3 * 0 + 1) fuel).
fold (model_f (0 / 2) fuel).
remember (0 =? 1) as eq.
cbv in Heqeq. rewrite Heqeq.
rewrite leb0true. simpl negb.
cbv iota. remember (0 mod 2) as Emod.
cbv in HeqEmod.
rewrite HeqEmod.
cbv [Nat.eqb].
Admitted.
Исходная версия AndreyKl, :
Я привёл пример функции f
Ты привёл пример функции для которой никто ничего доказать не сможет кроме как перебором, кроме некоторых частных случаев. (ну или вот я приводил, может верное доказательство, но тогда мужик один из первых и немногих кто вообще для этой функции что то более-менее доказал)
И попросил меня доказать для неё что-то. Смотри: доказательства на Коке почти не отличаются от доказательств в обычной математике. Есть некоторая специфика, конечно. Может быть, пожалуй, наиболее заментая - это большая подробность - там где в математике ты просто скажешь «ну понятно», в коке придётся всё таки дать доказательство.
Теперь мне кажется ты можешь согласится что наивно ожидать что кто-то впринципе даст тебе доказательство того, доказательство чего не дали лучшие математики. Я думаю теперь должно быть понятно почему пример неудачный. Просто для этой функции не докажет никто и нечего. Такая функция.
Почему реализовывать перебор на Коке странно я тоже уже постарался вроде объяснить. Переберать лучше на чём то что более подходит для перебора.
Фактически, доказывается только для аналога цикла for (в диапазоне или в коллекции).
Отнюдь. Но это довольно простой случай. И наверное наиболее частый (в некоторых вариациях).
Вот такое (Integrate), я так понимаю, тоже доказать нельзя будет:
Всё сводится к «обычной» математике. Если можешь доказать сходимость этого интрегрирования (формально, на математическом языке), на Коке тоже скорее всего всё получится. Правда доказательств для численных методов я лично никогда не касался.
После вышесказанного. При попытке доказать функциональную корректность у меня почему то получается что f в нуле виснет. Это я что то напутал или так и задумано?
Require Import Arith.
Require Import Bool.Bool.
Open Scope nat_scope.
Variable onehmlr : nat.
Axiom onehmrl_eq : onehmlr = 100000000000.
#[bypass_check(guard=yes)]
Fixpoint f(k : nat) : nat :=
if k =? 1 then 1
else
if negb (k <=? onehmlr) then 0
else
if k mod 2 =? 0 then f (k/2)
else f (3*k+1).
Fixpoint model_f (k fuel : nat) {struct fuel} : option nat :=
match fuel with
| O => None
| S fuel =>
if k =? 1 then Some 1
else if negb (k <=? onehmlr) then Some 0
else if k mod 2 =? 0 then model_f (k/2) fuel
else model_f (3*k+1) fuel
end.
Locate unint.
Opaque onehmlr.
Lemma leb0true n : 0 <=? n = true.
Proof.
destruct n; reflexivity.
Qed.
Lemma eq_f_model_f k fuel : k < onehmlr -> fuel < onehmlr -> fuel > 0 -> model_f k fuel = Some (f k).
Proof.
induction fuel.
intros. inversion H1.
intros. destruct k.
unfold model_f. cbv fix. cbv beta. cbv iota.
fold (model_f (3 * 0 + 1) fuel).
fold (model_f (0 / 2) fuel).
remember (0 =? 1) as eq.
cbv in Heqeq. rewrite Heqeq.
rewrite leb0true. simpl negb.
cbv iota. remember (0 mod 2) as Emod.
cbv in HeqEmod.
rewrite HeqEmod.
cbv [Nat.eqb].
Admitted.