The Coq mailing list

[Craig McLaughlin <mr_mcl AT live.co.uk>]

I should have been more clear about my intentions here. The code I presented
is a simplification of a larger code base; the "valid''/"non-valid''
semantics are not important. I require a fixpoint which operates on a subset
of constructors and which may (as in the case of all_choice) recurse on
arguments of the same type (which themselves must satisfy the predicate 
of the
subset type).

I could define a fixpoint like your simplify function but I wish to avoid
doing that since the semantics of the fixpoint do not apply to all
constructors and I do not wish to return dummy values for the impossible
cases. I see the possibility of using a dependent pattern match but it's not
clear how to tell Coq that the structurally decreasing argument is a sig 
type
(which seems to be the problem, given the error message).

Regards,
Craig

On 01/11/14 12:17, Gabriel Scherer wrote:
> I don't have any intuition about your distinction between valid and
> invalid, and the structure of is_valid. The valid_cons function looks
> like it is trying to translate a term in AllCons into a term that does
> not use the constructors you call "valid", but is actually defined
> only on terms that have valid constructors at the top-level (what
> about (all_or all_zero all_zero) for example?).
> You say that valid_cons ought to translate valid constructors into
> "non-valid" ones, but was is a non-valid constructor? If it was only
> the negation of the "valid" predicate, you would not need to call
> valid_cons recursively for this result to hold: (all_or A B) is not
> valid, regardless of what A and B are. It seems there is an underlying
> notion of "not valid" that is somehow "recursively not a valid
> constructor" -- but this would be weird it means some terms that are
> "deeply not valid" in thise sense are not in the "is_valid" relation
> and thus cannot be passed to the valid_cons function.
>
> I wrote the following, using a distinction between "simple" and
> "derived" constructors (the latter which you call "valid"). The
> valid_cons function becomes a function that turns any term into a term
> using only simple constructors.
>
> Fixpoint simplify C := match C with
>    | all_choice A B => all_or (simplify A) (simplify B)
>    | all_zero => all_unit
>    | all_or A B => all_or (simplify A) (simplify B)
>    | all_and A B => all_and (simplify A) (simplify B)
>    | all_unit => all_unit
> end.
>
> Inductive simple : AllCons -> Prop :=
>    | simple_or : forall a b (AS: simple a) (BS: simple b),
>                    simple (all_or a b)
>    | simple_and : forall a b (AS: simple a) (BS: simple b),
>                    simple (all_and a b)
>    | simple_unit : simple all_unit
> .
>
> Lemma simplify_simple : forall C, simple (simplify C).
>    induction C; simpl; constructor; auto.
> Qed.
>
> On Sat, Nov 1, 2014 at 12:34 PM, Craig McLaughlin 
> <mr_mcl AT live.co.uk>
>  wrote:
> > Hi all,
> >
> > I'm trying to define a fixpoint which operates on a subset of an inductive
> > type. I've defined a notion of ``valid'' constructors and created a fixpoint
> > with a subset type argument using this predicate. The fixpoint converts
> > ``valid'' constructors to ``non-valid'' constructors; 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".
> >
> > It should be a matter of somehow including the AV and BV assumptions in the
> > [valid_choice] case of [is_valid], but I'm not aware of any similar
> > examples.
> >
> > Require Import Program.
> > Set Implicit Arguments.
> >
> > Inductive AllCons : Set :=
> > (* valid constructors section *)
> >    | all_choice : AllCons -> AllCons -> AllCons
> >    | all_zero : AllCons
> > (* Other constructors *)
> >    | all_or : AllCons -> AllCons -> AllCons
> >    | all_and : AllCons -> AllCons -> AllCons
> >    | all_unit : AllCons.
> >
> > Inductive is_valid : AllCons -> Prop :=
> >    | valid_choice : forall a b (AV: is_valid a) (BV: is_valid b),
> >                       is_valid (all_choice a b)
> >    | valid_zero : is_valid all_zero.
> >
> > 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.
> >
> > Regards,
> > Craig