The Coq mailing list

[Rohit Persaud <persaud.rohit AT googlemail.com>]

Thanks Adam, but I did manage to figure out what was wrong.

The purpose of the EqSum function is to recursively apply Pol_eq to the respective projections of functions like A + B -> C, namely A -> C and B -> C. So given two functions of type 
I -> X + Y (given by  PSum1 X Y Ia and PSum1 X Y Ib, with Ia and Ib being the injections
I -> A and I -> B, respectively) we wish to decompose I, applying Pol_eq to its respective components. It only matters if  I is a sum type, say P + Q,  in which case we need to apply Pol_eq to the projections P -> A, Q -> A, P -> B and Q -> B. Otherwise, I needs no decomposition and Pol_eq is applied to the respective injections.

Indeed you are correct in stating that the recursive calls to Pol_eq need the arguments explicitly (Obviously! but i think I've seen some coq code somewhere where something similar was done but, come to think of it, I can't remember checking if the code actually works!). Anyway the following function achieves my objectives: 

 Fixpoint Pol_eq (I J: T) (i : POLY I J) {struct i} :  POLY I J -> bool :=
     match i in POLY _ e return (POLY _ e -> bool)   with
     | PA n => fun _ => true
     | PProdI _ _ Ia Ib =>    fun _ => true
    | Punit   => fun _ => true                       
   | PSum1 X Y
Ib => fun x =>                     
                    match polyys x with
                     | pleft pl => EqSum (fun _ _ => Pol_eq Ib pl) Ib pl
                     |  _       => false
                     end
     | PSum2 X Y Ib => fun _ => true
    end.

Rohit.

On Wed, Feb 18, 2009 at 8:51 PM, Adam Chlipala <adamc AT hcoop.net> wrote:

Rohit Persaud wrote:

Now when i define the function :

  Fixpoint Pol_eq (I J: T) (i : POLY I J) {struct i} :  POLY I J -> bool :=
    match i in POLY _ e return (POLY _ e -> bool)   with
    | PA n => fun _ => true
    | PProdI _ _ Ia Ib =>    fun _ => true
    | Punit   => fun _ => true                       

| PSum1 X Y Ib => fun x =>                     match polyys x with
                    | pleft pl => EqSum (Pol_eq (I := I) (J :=  X)) Ib pl
                    |  _       => false
                    end
    | PSum2 X Y Ib => fun _ => true
   end.
  ( * note  the implementations at the branches are replaced by true for brevity *)
  I get the following error "Recursive call to Pol_eq had not enough arguments " . Shouldn't this function be fine?

No, it shouldn't be fine.  Any call to a recursive function must include the recursive argument explicitly, since this is needed for termination checking.

 Is there any way around this.

I haven't followed the details of what you're trying to do, but it seems plausible that your function might be primitive-recursive in either [I] or [J].  You could try changing the [struct] annotation to reflect that.  This might require more dependent types tricks than you have now.