Научить coq проверять терминацию

Coq, в отличие от многих других, принимает необязательный явный параметр, который можно использовать для указания убывающей структуры определения фиксированной точки.

Из спецификации Gallina, 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 и убеждаете его принять определение фиксированной точки?


termination coq totality
person Jason Hu    schedule 09.01.2018    source источник
comment
Вы спрашиваете об инструментах, которые вы можете использовать, чтобы убедить Coq, что ваша функция завершается? Или что-то другое? Например, как это сделать с помощью примитива Fixpoint или fix?   -  person Anton Trunov    schedule 09.01.2018
comment
@AntonTrunov Я спрашиваю, могу ли я доказать, что функция завершается, как я могу научить ее coq, если это возможно. ради примера, как я могу позволить coq принять это определение чередования без изменения основной идеи алгоритма?   -  person Jason Hu    schedule 09.01.2018
comment
Не могли бы вы использовать Program Fixpoint / Function / Fix комбинатор / Equations плагин в качестве решения? Использование этих инструментов добавляет к вашей функции дополнительный параметр, цель которого — убедить Coq, что ваша функция завершается.   -  person Anton Trunov    schedule 09.01.2018
comment
@AntonTrunov Я не знаю об этом. Посмотрю.   -  person Jason Hu    schedule 09.01.2018

Ответы (2)


arrow_upward
10
arrow_downward

У вас есть несколько вариантов, и все они в конце концов сводятся к структурной рекурсии.

Преамбула

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.

Плагин Equations

Это внешний плагин, который решает многие проблемы с определением функций в 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?

person Anton Trunov    schedule 10.01.2018
comment
слава богу, это такой хороший и краткий учебный текст. - person Jason Hu; 10.01.2018

arrow_upward
1
arrow_downward

Вы можете использовать что-то под названием 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

person Ptival    schedule 09.01.2018