Decreasing argument with dependent types

Question

When dealing with non-dependent types, Coq (usually) infers which argument is decreasing in a fixpoint. However, it is not the case with dependent types.

For instance, consider the following example in which I have a type A_list which ensures that a property P holds for all elements (of type A) in the list:

Require Import Coq.Lists.List.

Variable A: Type.
Variable P: A -> Prop.

Definition A_list := {a: list A | Forall P a}.

Now, say I want to have a fixpoint working with such a list recursively (the 2 lemmas are not interesting here. The dummy_arg is to simulate working with multiple arguments.) :

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.

Which, as expected, returns an error "Cannot guess decreasing argument of fix." since, strictly speaking, we are not decreasing on the argument. Nonetheless, we are obviously decreasing on proj1_sig l (the list embedded in the sig).

This is probably solvable using Program Fixpoints, but since it must be a very common pattern to decrease on a projection of a dependent type, I wonder what is the "right" way to manage such cases.

Anton Trunov Anton Trunov · Accepted Answer · 2018-08-22T12:10:42

You can solve this problem using one of the methods I mentioned in this answer, including Program. If you decouple the list and the proof, then it can be done using ordinary recursion :

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.

Decreasing argument with dependent types

1 Answers