The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Zhong Shao 
<shao AT cs.yale.edu>:



Hello,

 When you define RR, A is no more a general parameter of your definition, and
becomes a plain argument. Thus elimination schemes become more complex
and hard to apply.


 If you try to build interactively your function F, you will see the
difference.

Inductive RR : Set -> Type :=
         RRep : forall A:Set,  A -> RR(A).


Definition F (A B : Set) (y : RR(A->B)) (x:A): RR(B).
  intros A B y ; case y.
(*
  A : Set
  B : Set
  y : RR (A -> B)
  ============================
   forall A0 : Set, A0 -> A -> RR B

   :-(  :-(   :-(

*)

(* instead of case, we can try inversion. *)
  Undo.
  intros A b y ; inversion y.

(*

  A : Set
  b : Set
  y : RR (A -> b)
  A0 : Set
  H : A0
  H0 : A0 = (A -> b)
  ============================
   A -> RR b

*)

 subst A0.
 constructor.
 apply H.
 auto.
Defined.


But, if you print F, you can see that the term is quite complex.

In order to understand the difference between the two approaches, the best
is to compare the two elimination schemes, namely R_rect and RR_rect.

Pierre

-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.