Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Annotation for Dependent Pattern Matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Annotation for Dependent Pattern Matching


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Annotation for Dependent Pattern Matching
  • Date: Sat, 01 Nov 2014 19:35:55 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page