The Coq mailing list

["Daniel Peng" <coq AT peng.dyndns.org>]

Hello,

I'm trying to formalize Typed Assembly Language in Coq, and the types
look like this:

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.

I thought I could leverage the standard library by using Map, but
perhaps this is the wrong approach.  Do I need to give up on Map and
somehow make the mutual induction explicit (e.g., below)?  Is there a
better way to do this?  I just started learning Coq a week ago, so I'd
appreciate any suggestions and advice.

Inductive T : Set :=
 | TInt
 | TCode: (register -> opt) -> T
 | TVar : typevariable -> T (* deBruijn indices *)
 | TForall : T -> T
with opt : Set :=
| SOME : T -> opt
| NONE.

Scheme T_ind2 :=
 Induction for T Sort Set
with TCode_ind2 :=
 Induction for option Sort Set.


Thank you,
Daniel Peng