The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Dear Adriaan,



On Wed, 9 Apr 2008 10:12:03 +0000 (UTC)
Adriaan Moors 
<adriaan AT cs.kuleuven.be>
 wrote:

> 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.
> 

This is not a Function limitation but a Fixpoint one. 
Coq only allows the user to define a mutual recursive functions over
mutually recursively defined inductives. So that you can not defined
subst_mems in the same block as the three other functions. 

In order not to inline the definition of lists, you can use a well-know trick 
constiting in inlining 
the definition of subst_mems itself as follows:

Fixpoint 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 => 
      let subst_mems := 
        fix subst_mems (mems:list member) {struct mems} := 
        match mems with 
          | nil => nil
          | cons m ms => cons (subst_mem m) (subst_mems ms)
        end
        in
      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
.

But this time you will lose the possibility of using Function since this 
feature does not support (and will not support for probably a long time) 
so called local recursive definition. 


Best regards, 
Julien Forest