The Coq mailing list

["Daniel Peng" <dpeng AT eecs.harvard.edu>]

Thanks Frederic.  That's exactly what I was looking for.  Thank you.

Daniel

On 5/22/06, Frederic Blanqui 
<Frederic.Blanqui AT loria.fr>
 wrote:
> 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.