The Coq mailing list

["Zhaozhong Ni" <nzz AT acm.org>]

The following works in this case:

Definition F (A B : Set) (x : A) (y : RR(A->B)) : RR(B) :=
 match y in RR(C) return C=(A->B) -> RR(B) with
   RRep C y0 => fun pf => RRep B (eq_rect C (fun T => T) y0 (A->B) pf x)
 end (refl_equal (A->B)).

-Zhaozhong

----- Original Message ----- 
From: "Zhong Shao" <shao AT cs.yale.edu>
To: 
<coq-club AT pauillac.inria.fr>
Cc: 
<flint-core AT cs.yale.edu>
Sent: Thursday, February 03, 2005 3:11 PM
Subject: Re: [Flint-core] Dependent elimination question?


> 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
> |> 
> _______________________________________________
> Flint-core mailing list
> Flint-core AT cs.yale.edu
> http://netra.cs.yale.edu/mailman/listinfo/flint-core