The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

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