Поиск по списку рекурсивно в Coq

Question

Я пытаюсь найти объект в списке, а затем, возможно, вернуть true, если он найден; ложь в противном случае.

Однако то, что я пытался придумать, неверно. Я был бы очень признателен за некоторые рекомендации. Мне нужна функция для поиска по списку элементов, сравнивая заголовок списка с соответствующим элементом, если не совпадает, то рекурсивно пропускаю оставшуюся часть списка через функцию и повторяю, сопоставляя заголовок списка.

Fixpoint find (li:list Interface){struct li}: list Interface :=
match li with
| nil => nil
| y::rest => find rest 
end.

Ваше руководство и помощь очень ценятся.

Заранее спасибо

Answer 1

Существует очень похожая функция в теории List в стандартной библиотеке.Эта функция принимает предикат в качестве аргумента, то есть функцию f из типа элемента в bool, и возвращает Some x, если найден соответствующий элемент x, или None, если ни один не найден.

Variable A : Type.
Fixpoint find (f:A->bool) (l:list A) : option A :=
  match l with
    | nil => None
    | x :: tl => if f x then Some x else find tl
  end.

Вы ищете элемент, который соответствует определенному объекту a.Это означает, что ваш предикат равен eq_Interface a, где eq_Interface - это равенство, которое вы хотите получить над Interface.

Вы должны определить функцию равенства для вашего типа, потому что может быть много определенийравенство.Coq определяет =, то есть равенство Лейбница : два значения равны, если нет никакого различия между ними.= является предложением, а не логическим, потому что это свойство вообще не разрешимо.Это также не всегда желаемое равенство для типа, иногда требуется более грубое отношение эквивалентности, чтобы два объекта можно было считать равными, если они были построены по-разному, но тем не менее имеют одинаковое значение.

Если Interface это простой тип данных - интуитивно, структура данных без встроенного предложения - есть встроенная тактика для построения функции структурного равенства из определения типа.Посмотрите decide equality в справочном руководстве.

Definition Interface_dec : forall x y : Interface, {x=y} + {x <> y}.
Proof. decide equality. Defined.
Definition Interface_eq x y := if Interface_dec x y then true else false.

Interface_dec не только говорит вам, равны ли его аргументы, но также поставляется с доказательством того, что аргументы равны или что они разные.

Если у вас есть эта функция равенства, вы можете определить свою функцию find в терминах стандартной библиотечной функции:

Definition Interface_is_in x := if List.find (Interface_eq x) then true else false.

Answer 2

Хммм, я не испорчу удовольствие, дав рабочий код :).Вы явно что-то упускаете.Ваша проблема в том, как закодировать это в Coq или это более общий вопрос?Как бы вы написали это в псевдокоде?Или на каком-нибудь другом языке, с которым вы знакомы?