The Coq mailing list

[Adriaan Moors <adriaan AT cs.kuleuven.be>]

Dear Club,

I'm trying to do functional induction on my substitution function. My current
definition uses List.map to define substitution on a list of members in terms
of substitution on a single member. This breaks the generation of the
induction principle, which I can live with. Thus, to be able to generate the
induction principle automatically, I simplified my definition to the
following, which still does not work:

Require Import List.

Inductive trm : Set :=
  | new : typ -> trm
with typ : Set :=
  | strct : list member -> typ
with member : Set :=
  | membr : typ -> trm -> member.

Function subst_trm (e : trm) {struct e} : trm :=
  match e with
    | new T => new (subst_typ T)
  end

with subst_typ (e : typ) {struct e} : typ :=
  match e with
    | strct mems => strct (subst_mems mems)
  end

with subst_mem  (e : member) {struct e} : member :=
  match e with
    | membr T rhs => membr (subst_typ T) (subst_trm rhs)
  end

with subst_mems (e : list member) {struct e} : list member :=
  match e with
    | nil => nil
    | cons m ms => cons (subst_mem m) (subst_mems ms)  
(* Error:
Recursive call to subst_mem has principal argument equal to 
"m"
instead of ms
*)
  end.


Now, if I further "inline" the definition of list, as below, the error goes
away. One of the things I like about Coq is the rich standard library, so I
would prefer not to do this. Is there a way to have my cake and eat it too?
Can I keep my nested list's and use Function to get my functional induction
principle?

Inductive trm : Set :=
  | new : typ -> trm
with typ : Set :=
  | strct : members -> typ
with member : Set :=
  | membr : typ -> trm -> member
with members : Set :=
  | mnil : members
  | mcons : member -> members -> members.

Function subst_trm (e : trm) {struct e} : trm :=
  match e with
    | new T => new (subst_typ T)
  end

with subst_typ (e : typ) {struct e} : typ :=
  match e with
    | strct mems => strct (subst_mems mems)
  end

with subst_mem  (e : member) {struct e} : member :=
  match e with
    | membr T rhs => membr (subst_typ T) (subst_trm rhs)
  end

with subst_mems (e : members) {struct e} : members :=
  match e with
    | mnil => mnil
    | mcons m ms => mcons (subst_mem m) (subst_mems ms)
  end.

cheers,
adriaan