coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 inductiveActually, the issue is not Program. Nor is it annotation of your
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.
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
- [Coq-Club] Annotation for Dependent Pattern Matching, Craig McLaughlin, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Gabriel Scherer, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Craig McLaughlin, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Jonathan, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Craig McLaughlin, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Jonathan, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, John Wiegley, 11/02/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Arnaud Spiwack, 11/03/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Craig McLaughlin, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Arnaud Spiwack, 11/01/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Jonathan, 11/02/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Arnaud Spiwack, 11/03/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Jonathan, 11/02/2014
- Re: [Coq-Club] Annotation for Dependent Pattern Matching, Gabriel Scherer, 11/01/2014
Archive powered by MHonArc 2.6.18.