The Coq mailing list

[Pablo Argon <pargon AT cadence.com>]

Hello all,
        I'm confuse by the following error:
(example completely dummy)

-------------------------------
$ coqtop
Welcome to Coq V6.3.1 (December 1999)
 
Coq < Variable ValuationA : Type.
ValuationA is assumed
 
Coq < Variable SymbolSet : Set.
SymbolSet is assumed
 
Coq < Inductive Set GroundTAbs :=
      gta_intro: SymbolSet -> ValuationA -> GroundTAbs.

GroundTAbs_ind is defined
GroundTAbs_rec is defined
GroundTAbs is defined
 
Coq < Check [y :GroundTAbs ]
            (<Prop> Cases y of (gta_intro s2 va)=>true=true end).

Toplevel input, characters 7-91
> ..... [y :GroundTAbs ]
>   (<Prop> Cases y of (gta_intro s2 va)=>true=true end)

Error: Incorrect elimination of y in the inductive type
  GroundTAbs
 The elimination predicate Prop has type Type
 It should be one of :
  GroundTAbs->Prop, GroundTAbs->Set, Prop, Set
 
 Elimination of an inductive object of sort : Type
 is not allowed on a predicate in sort : Set
 because
 strong elimination on non-small inductive types leads to paradoxes.
-------------------------------
                      
On the other hand, the following is accepted "as expected":

Variable Valuation : Set.

Inductive Set GroundT :=
gt_intro: SymbolSet -> Valuation -> GroundT.

Check [y :GroundT ]
  (<Prop> Cases y of (gt_intro s2 va)=>true=true end).

Why Coq don't allow the Case analysis in the first definition,
which is simply a "let" ?
Thank you in advance.

best wishes, Pablo

NB: Obviously, I can get around writing:

Coq < Check [y :GroundTAbs ]
Coq <   ((s2:SymbolSet)(va:ValuationA)
Coq <     (y=(gta_intro s2 va))-> true=true).
[y:GroundTAbs]
 (s2:SymbolSet; va:ValuationA)y=(gta_intro s2 va)->true=true
     : GroundTAbs->PropVariable Valuation : Set.
Variable ValuationA : Type.
Variable SymbolSet : Set.

Inductive Set GroundT :=
gt_intro: SymbolSet -> Valuation -> GroundT.

Inductive Set GroundTAbs := 
gta_intro: SymbolSet -> ValuationA -> GroundTAbs.

Check [ y :GroundT ]
  (<Prop> Cases y of (gt_intro s2 va)=>true=true end).

Check [y :GroundTAbs ]
  ((s2:SymbolSet)(va:ValuationA)
    (y=(gta_intro s2 va))-> true=true).

Check [y :GroundTAbs ]
  (<Prop> Cases y of (gta_intro s2 va)=>true=true end).