The Coq mailing list

[Adriaan Moors <adriaan.moors AT gmail.com>]

Dear Julien,

Thank you for the hint about inlining subst_mems! Is it discussed in a  
FAQ that I should have read?

I implemented your suggestion, and now my fixpoint is accepted, but on  
using Functional Scheme, I get:
"Anomaly: add_args : todo. Please report."

Is this the restriction you mentioned? I guess the only way to use  
functional induction without defining the (huge) induction principles  
by hand (which I've already done for the normal induction principles)  
is to remove nested occurrences of list etc in my datatypes (as  
illustrated in my example below). That'd be quite unfortunate :-(

cheers,
adriaan

ps: here's the relevant fragment from my script:

Fixpoint subst_tm (z : var) (u : tm) (e : tm) {struct e} : tm :=
  match e with
    | bvar i => bvar i
    | fvar x => if x == z then u else (fvar x)
    | sel e1 l => sel (subst_tm z u e1) l
    | new T => new (subst_tp z u T)
  end

with subst_tp (z : var) (u : tm) (e : tp) {struct e} : tp :=
    let subst_mems := fix subst_mems (mems:list mem) {struct mems} :=
       match mems with
         | nil => nil
         | cons m ms => cons (subst_mem z u m) (subst_mems ms)
       end in
  match e with
    | tp_struct None mems => tp_struct None (subst_mems mems)
    | tp_struct (Some self) mems => tp_struct (Some (subst_tp z u  
self))  (subst_mems mems)
  end

with subst_mem (z : var) (u : tm) (e : mem) {struct e} : mem :=
  match e with
    | mtm l T None => mtm l (subst_tp z u T)  None
    | mtm l T (Some rhs) => mtm l (subst_tp z u T)  (Some (subst_tm z  
u rhs))
  end.

Functional Scheme subst_tm_ind := Induction for subst_tm Sort Prop
with subst_tp_ind := Induction for subst_tp Sort Prop
with subst_mem_ind := Induction for subst_mem Sort Prop.


On 09 Apr 2008, at 16:14, Julien Forest wrote:

> 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