Убывающий аргумент с зависимыми типами
При работе с независимыми типами Coq (обычно) определяет, какой аргумент уменьшается в фиксированной точке. Однако это не относится к зависимым типам.
Например, рассмотрим следующий пример, в котором у меня есть тип A_list, который гарантирует, что свойство P сохраняется для всех элементов (типа A) в списке:
Require Import Coq.Lists.List.
Variable A: Type.
Variable P: A -> Prop.
Definition A_list := {a: list A | Forall P a}.
Теперь предположим, что я хочу, чтобы фиксированная точка работала с таким списком рекурсивно (две леммы здесь не интересны. Dummy_arg предназначен для имитации работы с несколькими аргументами.):
Lemma Forall_tl: forall P (h: A) t, Forall P (h::t) -> Forall P t.
Admitted.
Lemma aux: forall (l1: list A) l2 P, l1 = l2 -> Forall P l1 -> Forall P l2.
Admitted.
Fixpoint my_fixpoint (l: A_list) (dummy_arg: A) :=
match (proj1_sig l) as x return proj1_sig l = x -> bool with
| nil => fun _ => true
| hd::tl =>
fun h =>
my_fixpoint (exist (Forall P) tl (Forall_tl P hd tl (aux _ _ _ h (proj2_sig l)))) dummy_arg
end eq_refl.
Что, как и ожидалось, возвращает ошибку «Невозможно угадать убывающий аргумент исправления». поскольку, строго говоря, мы не уменьшаем аргументацию. Тем не менее, на proj1_sig l (список встроен в sig) мы явно падаем.
Вероятно, это можно решить с помощью Program Fixpoint, но, поскольку это должно быть очень распространенная схема уменьшения проекции зависимого типа, мне интересно, каков «правильный» способ управлять такими случаями.
Ответы 1
Вы можете решить эту проблему, используя один из методов, упомянутых в этот ответ, включая Program.
Если вы разделите список и доказательство, то это можно будет сделать с помощью обычной рекурсии:
Fixpoint my_fixpoint (l: list A) (pf : Forall P l) (dummy_arg: A) : bool :=
match l as x return Forall P x -> bool with
| nil => fun _ => true
| hd::tl => fun h => my_fixpoint tl (Forall_tl P hd tl h) dummy_arg
end pf.
Отлично, спасибо. Я не получил упомянутого вами ответа (вероятно, потому, что искал не те теги).