The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/01/2014 05:51 PM, Arnaud Spiwack wrote:
> > 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 _.

But, doesn't the need to split up C short-change the subtyping 
capabilities of Program?

-- Jonathan