Take the 2-minute tour ×

I would like to somehow limit what kind of inputs constructors are allowed to take in an inductive definition. Say I want to say define binary numbers as follows:

Inductive bin : Type :=
  | O : bin
  | D : bin -> bin
  | S : bin -> bin.

The idea here is that D doubles up a nonzero number by adding a zero at the end and S takes a number with zero as the last digit and turns the last digit into a one. This means that the following are legal numbers:

S 0
D (S 0)
D (D (S 0))

while the following would not be:

S (S 0)
D 0

Is there a way to enforce such restrictions in an inductive definition in a clean way?

share|improve this question
add comment

2 Answers

up vote 6 down vote accepted

You could define what it means for a bin to be legal with a predicate, and then give a name to the subset of bins that obey that predicate. Then you write functions with Program Definition and Program Fixpoint instead of Definition and Fixpoint. For recursive functions you'll also need a measure to prove the arguments of your functions decrease in size since the functions are not structurally recursive anymore.

Require Import Coq.Program.Program.

Fixpoint Legal (b1 : bin) : Prop :=
  match b1 with
  | O       => True
  | D O     => False
  | D b2    => Legal b2
  | S (S _) => False
  | S b2    => Legal b2

Definition lbin : Type := {b1 : bin | Legal b1}.

Fixpoint to_un (b1 : bin) : nat :=
  match b1 with
  | O    => 0
  | D b2 => to_un b2 + to_un b2
  | S b2 => Coq.Init.Datatypes.S (to_un b2)

Program Definition zer (b1 : lbin) := O.

Program Fixpoint succ (b1 : lbin) {measure (to_un b1)} : lbin :=

But this simply-typed approach would probably be easier.

share|improve this answer
This seems more reasonable than the other answer. I was too lazy to write one. You could take a predicate as additional argument, but then writing numbers is annoying. You could just not care and canonicalize when needed. –  Ptival Dec 24 '12 at 21:13
add comment

This could be done with inductive-recursive definitions - but unfortunately Coq doesn't support those.

From an object-oriented programming perspective, O, D and S are subtypes of bin, and their constructor types are then definable without resorting to logical predicates, but Coq doesn't support object-oriented programming natively either.

However, Coq does have typeclasses. So what I might do is make bin a typeclass, and make each of the constructors a separate inductive type, each of which has an instance of the bin typeclass. I'm not sure what the method(s) of the typeclass would be though.

share|improve this answer
add comment

Your Answer


