Научите coq проверять завершение
Coq, в отличие от многих других, принимает необязательный явный параметр, который может использоваться для указания убывающей структуры определения точки фиксации.
Из спецификации Галлина, 1.3.4,
Fixpoint ident params {struct ident0 } : type0 := term0
определяет синтаксис. но из этого мы узнали, что это должен быть идентификатор, а не общая мера.
Тем не менее, в общем, существуют рекурсивные функции, которые завершение не совсем очевидно, или это на самом деле, но просто проверяющий завершение трудно найти убывающую структуру. Например, следующая программа чередует два списка,
Fixpoint interleave (A : Set) (l1 l2 : list A) : list A :=
match l1 with
| [] => []
| h :: t => h :: interleave l2 t
end
Эта функция явно завершается, в то время как Coq просто не мог понять это. Причина не l1 ни l2 уменьшаются каждый цикл. Но что, если мы рассмотрим меру, определенную как length l1 + length l2? Тогда эта мера явно уменьшает каждую рекурсию.
Поэтому мой вопрос в том, что в случае сложной ситуации, когда код нелегко организовать организованным способом проверки завершения, как вы обучаете coq и убеждаете его принять определение точки фиксации?
2 ответа
У вас есть несколько вариантов, и все они в конечном итоге сводятся к структурной рекурсии.
преамбула
From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.
Структурная рекурсия
Иногда вы можете переформулировать свой алгоритм структурно рекурсивным способом:
Fixpoint interleave1 {A} (l1 l2 : list A) {struct l1} : list A :=
match l1, l2 with
| [], _ => l2
| _, [] => l1
| h1 :: t1, h2 :: t2 => h1 :: h2 :: interleave1 t1 t2
end.
Кстати, в некоторых случаях вы можете использовать трюк с вложенным fixes - посмотрите это определение функции Аккермана (она не будет работать только с Fixpoint).
Program Fixpoint
Ты можешь использовать Program Fixpoint механизм, который позволяет вам написать вашу программу естественным образом, а затем доказать, что она всегда заканчивается.
From Coq Require Import Program Arith.
Program Fixpoint interleave2 {A} (l1 l2 : list A)
{measure (length l1 + length l2)} : list A :=
match l1 with
| [] => l2
| h :: t => h :: interleave2 l2 t
end.
Next Obligation. simpl; rewrite Nat.add_comm; trivial with arith. Qed.
Function
Другой вариант заключается в использовании Function команда, которая может быть несколько ограничена по сравнению с Program Fixpoint, Вы можете узнать больше об их различиях здесь.
From Coq Require Recdef.
Definition sum_len {A} (ls : (list A * list A)) : nat :=
length (fst ls) + length (snd ls).
Function interleave3 {A} (ls : (list A * list A))
{measure sum_len ls} : list A :=
match ls with
| ([], _) => []
| (h :: t, l2) => h :: interleave3 (l2, t)
end.
Proof.
intros A ls l1 l2 h t -> ->; unfold sum_len; simpl; rewrite Nat.add_comm; trivial with arith.
Defined.
Плагин уравнений
Это внешний плагин, который решает многие проблемы с определением функций в Coq, включая зависимые типы и завершение.
From Equations Require Import Equations.
Equations interleave4 {A} (l1 l2 : list A) : list A :=
interleave4 l1 l2 by rec (length l1 + length l2) lt :=
interleave4 nil l2 := l2;
interleave4 (cons h t) l2 := cons h (interleave4 l2 t).
Next Obligation. rewrite Nat.add_comm; trivial with arith. Qed.
Приведенный выше код работает, если вы примените это исправление.
Fix / Fix_F_2 комбинаторы
Вы можете узнать больше об этом (ручном) подходе, если перейдете по ссылкам из этого вопроса о mergeSort функция. Кстати, mergeSort функция может быть определена без использования Fix если вы примените вложенный fix трюк, о котором я упоминал ранее. Вот решение, которое использует Fix_F_2 комбинатор, так как у нас есть два аргумента, а не один, как mergeSort:
Definition ordering {A} (l1 l2 : list A * list A) : Prop :=
length (fst l1) + length (snd l1) < length (fst l2) + length (snd l2).
Lemma ordering_wf' {A} : forall (m : nat) (p : list A * list A),
length (fst p) + length (snd p) <= m -> Acc (@ordering A) p.
Proof.
unfold ordering; induction m; intros p H; constructor; intros p'.
- apply Nat.le_0_r, Nat.eq_add_0 in H as [-> ->].
intros contra%Nat.nlt_0_r; contradiction.
- intros H'; eapply IHm, Nat.lt_succ_r, Nat.lt_le_trans; eauto.
Defined.
Lemma ordering_wf {A} : well_founded (@ordering A).
Proof. now red; intro ; eapply ordering_wf'. Defined.
(* it's in the stdlib but unfortunately opaque -- this blocks evaluation *)
Lemma destruct_list {A} (l : list A) :
{ x:A & {tl:list A | l = x::tl} } + { l = [] }.
Proof.
induction l as [|h tl]; [right | left]; trivial.
exists h, tl; reflexivity.
Defined.
Definition interleave5 {A} (xs ys : list A) : list A.
refine (Fix_F_2 (fun _ _ => list A)
(fun (l1 l2 : list A)
(interleave : (forall l1' l2', ordering (l1', l2') (l1, l2) -> list A)) =>
match destruct_list l1 with
| inright _ => l2
| inleft pf => let '(existT _ h (exist _ tl eq)) := pf in
h :: interleave l2 tl _
end) (ordering_wf (xs,ys))).
Proof. unfold ordering; rewrite eq, Nat.add_comm; auto.
Defined.
Оценочные тесты
Check eq_refl : interleave1 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave2 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Check eq_refl : interleave3 ([1;2;3], [4;5;6]) = [1;4;2;5;3;6].
Fail Check eq_refl : interleave4 [1;2;3] [4;5;6] = [1;4;2;5;3;6]. (* Equations plugin *)
Check eq_refl : interleave5 [1;2;3] [4;5;6] = [1;4;2;5;3;6].
Упражнение: что произойдет с этой последней проверкой, если вы закомментируете destruct_list Лемма?
Вы можете использовать то, что называется measure вместо структурного аргумента для прекращения. Для этого я считаю, что вы должны использовать Program Fixpoint механизм, который немного задействован и сделает ваши доказательства более уродливыми (потому что он генерирует структурную рекурсию из предоставленного вами доказательства, так что функция, которую вы фактически будете использовать, не совсем та, которую вы написали).
Подробности здесь: https://coq.inria.fr/refman/program.html
Это также похоже на то, что называется Equations можно разобраться с мерами? ср http://mattam82.github.io/Coq-Equations/examples/RoseTree.html https://www.irif.fr/~sozeau/research/coq/equations.en.html