The Coq mailing list

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

Hi There,


I am having trouble defining the following function in Coq, and would greatly appreciate any advice.

Given the family of types :

 Inductive T : Set :=
   | T1 : T 
   | TN : T 
   | TP : T -> T -> T
   | TS : T -> T -> T.

 (* here is the interpretation of T, just for guidance : 
 
   Inductive Tint : T -> Set :=
   | Tunit : Tint T1
   | Tnat  : nat ->  Tint TN
   | Tinl  : forall t1, Tint t1 -> forall t2, Tint (TS t1 t2) 
   | Tinr  : forall t2, Tint t2 -> forall t1, Tint (TS t1 t2)
   | Tprod : forall t1, Tint t1 -> forall t2, Tint t2 -> Tint (TP t1 t2). 

 *)

and the types of functions over this family (these actually are of a special form, such that functions from nat -> nat are  decidable) :

  Inductive POLY (I : T) : T -> Set :=
  | Punit   : POLY I T1
  | PA      :  nat -> POLY I TN
  | PProdI  : forall X B, POLY I X -> POLY I B -> POLY I (TP X B)
  | PSum1   : forall X B, POLY I X -> POLY I (TS X B) 
  | PSum2   : forall X B, POLY I B -> POLY I (TS X B).
 Infix "  ===> " := POLY (at level 15).

we wish to decide equality on these functions:   Pol_eq (I J: T) :  POLY I J -> POLY I J -> bool.

It is clear how to define equality into the unit and product types, and we assume we know how to decide functions of type POLY TN TN. Two
functions from a sum type are equal iff their respective projections are equal. 

Given the following definitions :
 
 (* views  *)
  Inductive POLYS (I  A B: T) :   I ===> (TS A B)  -> Set :=  
   | pleft  : forall (i: POLY I A), POLYS (PSum1 B i )
   | pright : forall (i: POLY I B), POLYS (PSum2 A i). 

   Definition polyys (I A B : T) (i :  I ===>  (TS A  B)) : POLYS i :=
    match i in POLY _ e return match e return (POLY I e) -> Set with
                            | TS _ _ => @POLYS I _ _
                            | _ => fun _ => unit
                            end i  with
    | PSum1 _ b X => pleft  _ X
    | PSum2 a _ X => pright  _ X 
    | _ => tt
    end. 
 ( * ....... *)
 
  Fixpoint Pin1 (A B C : T) (i : (TS A  B) ===> C) {struct i} : A ===> C := 
   match i in (_  ===> e) return (A ===> e) with 
   | Punit => Punit A
   | PA n => PA A n
   | PProdI _ _ Ia Ib => PProdI (Pin1 Ia ) (Pin1 Ib)
   | PSum1  _ X Ia => PSum1 X (Pin1 Ia)
   | PSum2  X _ Ib => PSum2 X (Pin1 Ib)
   end.

  Fixpoint Pin2 (A B C : T) (i : (TS A  B) ===> C) {struct i} : B ===> C := 
   match i in (_ ===> e) return (B ===> e) with
   | Punit => Punit B
   | PA n => PA B n
   | PProdI _ _ Ia Ib => PProdI (Pin2 Ia ) (Pin2 Ib)
   | PSum1  _ X Ia => PSum1 X (Pin2 Ia)
   | PSum2  X _ Ib => PSum2 X (Pin2 Ib)
   end.

  Fixpoint Pout1 (A B C : T) (i : A  ===> C) {struct i} : TS B A ===> C := 
   match i in (_  ===> e) return (TS B A ===> e) with 
   | Punit => Punit (TS B A)
   | PA n => PA (TS B A) n
   | PProdI _ _ Ia Ib => PProdI (Pout1 B Ia ) (Pout1 B Ib)
   | PSum1  _ X Ia => PSum1 X (Pout1 B Ia)
   | PSum2  X _ Ib => PSum2 X (Pout1 B Ib)
   end.


  Fixpoint Pout2 (A B C : T) (i :  A ===> C) {struct i} : TS A B ===> C := 
   match i in (_ ===> e) return (TS A B ===> e) with
   | Punit => Punit (TS A B)
   | PA n => PA (TS A B) n
   | PProdI _ _ Ia Ib => PProdI (Pout2  B Ia ) (Pout2 B Ib)
   | PSum1  _ X Ia => PSum1 X (Pout2 B Ia)
   | PSum2  X _ Ib => PSum2 X (Pout2 B Ib)
   end.
 
   Fixpoint EqSum (A B : T) {struct A} : (POLY A B  -> POLY A B -> bool)
            -> POLY A B ->  POLY A B ->  bool :=
     match A as e return ((POLY e B  -> POLY e B -> bool) ->  POLY e B -> POLY e B -> bool) with
     | TS X Y => fun H f g =>
            EqSum (fun i j => H (Pout1 Y i) (Pout1 Y j)) (Pin1 f) (Pin1 g)
            &&
            EqSum (fun i j => H (Pout2 X i) (Pout2 X j)) (Pin2 f) (Pin2 g)
     | _ => fun H i j => H i j
     end.
 
 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? 
 Is there any way around this. 


Many Thanks,

Rohit.