The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

On Sat, 20 May 2006, Daniel Peng wrote:

> Inductive T : Set :=
> | TInt
> | TCode: Map T -> T (* the type of a code pointer is a partial map
> from registers to types *)
> | TVar : nat -> T (* deBruijn indices *)
> | TForall : T -> T.
>
> I'm having trouble with the induction principle in the TCode case.
> When I induct over T, the TCode case doesn't provide any induction
> hypotheses. Essentially, I want Map T and T to be mutually inductive;
> however, I haven't declared them that way, and I can't seem to get a
> mutual induction principle over them.

coq doesn't recognize (Map T) in the type of TCode as a recursive argument and 
doesn't generate the correct induction principle. you have to define it 
yourself. see Term/Varyadic/VTerm.v in the CoLoR library 
http://color.loria.fr/ for an example with list instead of Map:

[...]

Inductive term : Set :=
  | Var : variable -> term
  | Fun : forall f : Sig, list term -> term.

Reset term_rect.

Section term_rect.

Variables
  (P : term -> Type)
  (Q : terms -> Type).

Hypotheses
  (H1 : forall x, P (Var x))
  (H2 : forall f v, Q v -> P (Fun f v))
  (H3 : Q nil)
  (H4 : forall t v, P t -> Q v -> Q (t :: v)).

Fixpoint term_rect t : P t :=
  match t as t return P t with
    | Var x => H1 x
    | Fun f v => H2 f
      ((fix vt_rect (v : terms) : Q v :=
        match v as v return Q v with
          | nil => H3
          | cons t' v' => H4 (term_rect t') (vt_rect v')
        end) v)
  end.

End term_rect.

Definition term_ind (P : term -> Prop) (Q : terms -> Prop) := term_rect P Q.

Definition term_rec (P : term -> Set) (Q : terms -> Set) := term_rect P Q.