The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/01/2014 07:34 AM, Craig McLaughlin 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.

You can define it easily by proving:

Definition valid_cons (C: {x : AllCons | is_valid x}) : AllCons.
destruct C as [x i].
induction x as [x1 IHx1 x2 IHx2| | | | ].
- eapply all_or.
  eapply IHx1.
  inversion i; tauto.
  eapply IHx2.
  inversion i; tauto.
- exact all_unit.
- exfalso.
  inversion i.
- exfalso.
  inversion i.
- exfalso.
  inversion i.
Defined.

Note that:

Extraction valid_cons.

extracts quite nicely to:

let rec valid_cons = function
| All_choice (a0, a1) -> All_or ((valid_cons a0), (valid_cons a1))
| All_zero -> All_unit
| _ -> assert false (* absurd case *)

Just don't look at the proof term (Print valid_cons), else you risk blindness.  It's not clear whether using Program would have given you a cleaner proof term anyway, though.  Probably not by much.

-- Jonathan



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