The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

I'm trying to define a fixpoint which operates on a subset of an inductive
type.[…] I have attempted to do
this using PROGRAM. However, I'm not sure what annotation I should be placing
on my matching construct to get the typechecker to accept it. From the code
below (Coq v8.4pl4), I get the following error:

Recursive call to valid_cons has principal argument equal to
"exist (fun x : AllCons => is_valid x) A ?8" instead of
a subterm of "C". […]

Program Fixpoint valid_cons (C: {x : AllCons | is_valid x}) {struct C} :=
  match C with
  | all_choice A B => all_or (valid_cons A) (valid_cons B)
  | all_zero => all_unit
  | _ => False_rec _ _
  end.

Actually, the issue is not Program. Nor is it annotation of your pattern-matching (you most likely won't need any). It's just that fixpoints, in Coq, must be structural on an argument, and "subtypes" are non-recursive inductive types. So Coq cannot define a (non-trivial) fixpoint on them.

What you are actually trying to do, is to define a structural fixpoint on an [AllCons]. So you will need to do it in two steps:

Program Fixpoint valid_cons_aux (C:AllCons) (h:is_valid C) {struct C} := …

Program Definition valid_cons_aux (C: {x : AllCons | is_valid x}) := valid_cons_aux C _.

Or take any other route that suits you. What matters is that the subtype is destructed before the fixpoint is introduced. Jonathan solution does that too.