Почему определение «половины» в Fixpoint для списка не работает?
Я пытаюсь определить функцию Fixpoint для list X, чтобы получить первую половину подсписка, если это нечетное количество элементов, то средний элемент не учитывается.
Вот что я пробовал:
Fixpoint half {X : Type} (l : list X) : list X :=
match l with
| [] => []
| h :: t => match (rev t) with
| [] => []
| p :: b => [h] ++ (half (rev b))
end
end.
Но выдает ошибку:Cannot guess decreasing argument of fix.
Что мне здесь не хватает?
Что вы подразумеваете под structurally smaller? rev b является частью t, поэтому я не могу понять, почему он не меньше l... Ссылка кажется гораздо сложнее, попробую переварить, спасибо! @НаимФавиер
Вам придется сообщить Coq и использовать тот факт, что rev b является подсписком l и строго меньше l, о чем Coq не может просто догадаться. А способы «сообщить Coq об этом» — это то, что вы можете увидеть в теме, на которую ссылается @NaïmFavier. OTOH, я бы не хотел давать решение по этому вопросу, если вы прямо не спросите, учитывая, что ваш код крайне неэффективен, его не просто сложно писать и использовать, хотя я могу придумать хотя бы один способ реализации half, который чрезвычайно проще и, возможно, даже наиболее эффективно (для простого связанного списка): использование length и firstn...
Я согласен, что это неудобно и неэффективно. На самом деле я пытался написать это для целей доказательства. Мне просто интересно узнать причину. Спасибо за подсказки :-) @JulioDiEgidio
(На самом деле, для n длины списка существует решение за O(n), но ценой необходимости использования вспомогательной функции: в любом случае, я не буду на этом останавливаться.)
Ответы 2
Вы можете выполнить рекурсивный вызов только в том случае, если один из ваших аргументов является «обоснованным» индуктивным типом данных. Coq должен иметь возможность это проверить, и один из способов — увидеть, что рекурсивный аргумент является небольшой частью исходного аргумента. Вы не можете просто применить к нему функцию, так как это может сделать аргумент «больше», и тогда невозможно будет так же легко доказать, что рекурсия завершится. В вашем случае coq не видит, что rev b, например, не возвращает более длинный список. В этом случае мы можем выбрать что-то еще, что, как мы знаем, монотонно уменьшается, и использовать это, чтобы показать, что рекурсия завершается. Например, длина входного аргумента. Но тогда нам придется проделать кое-какую работу, чтобы показать это Коку.
Если вы хотите использовать более гибкий способ указания рекурсии,
импортируйте модуль Program и используйте Program Fixpoint вместо Fixpoint, чтобы определить свою функцию. И добавьте аргумент в {}, указывающий монотонно убывающую меру.
Например, мы можем использовать {measure (length l)}, чтобы указать, что длина аргумента l уменьшается при рекурсивных вызовах.
Затем определите функцию и используйте Next Obligation., чтобы получить оставшиеся обязательства по доказательству.
Require Import List. Import ListNotations.
Require Import Program.
(* add Program and {measure ...} *)
Program Fixpoint half {X : Type} (l : list X) {measure (length l)} : list X :=
match l with
| [] => []
| h :: t => match (rev t) with
| [] => []
| p :: b => [h] ++ (half (rev b))
end
end
.
Next Obligation.
(* Here we need to prove that the length of
the argument to the recursive call is smaller than
that of the calling function's argument:
Heq_anonymous : p :: b = rev t
--------
length (rev b) < length (h :: t)
*)
(* We need to find some lemma that shows that length (rev x) = length x
Search (length (rev _)). (* found rev_length *)
rewrite (rev_length b).
simpl.
rewrite <- (rev_length t).
rewrite <- Heq_anonymous.
simpl.
auto.
Qed.
Прошел эти этапы и узнал что-то новое. Довольно информативно! Большое спасибо!
Для справки, мое другое решение последовало предложению ХулиоДиЭгидио в комментарии к вопросу:
Fixpoint half_len {X : Type} (l : list X) : nat :=
match l with
| [] => 0
| _ :: t => match t with
| [] => 0
| _ :: t' => S (half_len t')
end
end.
Fixpoint firstn {X : Type} (l : list X) (n : nat) : list X
:= match l, n with
| [], _ => nil
| _, 0 => nil
| h :: t, S n' => h :: (firstn t n')
end.
Definition half {X : Type} (l : list X) : list X :=
firstn l (half_len l).
На самом деле использовал двух помощников, возможно, это не очень хороший алгоритм.
Приветствуем любые улучшения, спасибо!
rev bструктурно не меньшеl. См. также: stackoverflow.com/questions/46348606/…