Убывающий аргумент с зависимыми типами

При работе с независимыми типами 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 Fixpoints, но поскольку это должен быть очень распространенный шаблон для уменьшения проекции зависимого типа, мне интересно, каков «правильный» способ управлять такими случаями.


dependent-type termination coq
person Bromind    schedule 22.08.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете решить эту проблему, используя один из методов, упомянутых в этом ответе, включая 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.
person Anton Trunov    schedule 22.08.2018
comment
Отлично, спасибо. Я не получил упомянутого вами ответа (вероятно, потому, что искал не те теги). - person Bromind; 22.08.2018