The Coq mailing list

[Zhong Shao <shao AT cs.yale.edu>]

My question is apparently ill-phrased:

Given the way I define R in the last message:

   Definition F (A B : Set) (x : A) (y : R(A->B)) : R(B) := 
      match y with 
        Rep y0 => Rep B (y0 x)
      end.

apparently works fine. 

But if I define R differently as RR: 
 
   Inductive RR : Set -> Type := 
         RRep : forall A : Set, A -> RR(A).

Then my above definition "F" will be hard to write, since RRep
needs to take the explicit type argument (which is hard to
specify)

   Definition F (A B : Set) (x : A) (y : RR(A->B)) : RR(B) := 
      match y with 
        RRep _ y0 => RRep B (y0 x)
      end.


So there is a subtle difference between these two definitions R 
and RR.

-Zhong


|> Hi, given the following induction definition: 
|> 
|>    Inductive R (A : Set) : Type := 
|>         Rep : A -> R(A).
|> 
|> assume that Set is a predicative universe (as in Coq 8.0),
|> 
|> Can I write a function F with the following type: 
|> 
|>             (forall A B : Set) A -> R(A -> B) -> R(B)
|> 
|> The naive way is to write it as: 
|> 
|>   Definition F (A B : Set) (x : A) (y : R(A->B)) : R(B) := 
|>      match y with 
|>        Rep y0 => Rep (y0 x)
|>      end.
|> 
|> which of course does not work since y0 does not has type A->B.
|> 
|> Thanks a lot,
|> 
|> -Zhong Shao
|> 
(shao-zhong AT cs.yale.edu)
|> _______________________________________________
|> Flint-core mailing list
|> 
Flint-core AT cs.yale.edu
|> http://netra.cs.yale.edu/mailman/listinfo/flint-core
|>