The Coq mailing list

[popescu2 AT uiuc.edu]

I apologize for the possible multiple postings (the message sent from my 
other email account did not make it to the mailing list so far).  

Given the definition 

Definition Less (n:nat) : Set := {i | i < n}.

I am trying to define a sum operator that takes a number n, a predicate P : 
Less n -> Prop, 
and a function f : {i : Less n | P i} -> nat, and returns the sum of all 
numbers f i such that
 i : Less n and P i holds.  Informally I would define this sum by doing a 
case analysis, at the induction step n' to n'+1, on whether P n' holds, case 
in which I add 0, otherwise I add f n'.  However, even if I assume excluded 
middle, Coq would not let me do this case analysis, since I am attempting to 
eliminate Prop on Set. 

Working with boolean predicates P : Less n -> bool does not seem to help 
either, since then the functions f would be in 
f : {i : Less n | P i = true} -> nat and after matching P n' with true I do 
not seem to have access to a proof of 
P i = true in order to apply f to n'.

(In the discussion above, I have identified elements of Less n with elements 
of nat, in the "Program" style, to keep the ideas clear.) 

Is what I am trying to do violating the constructivity principles behind Coq? 
I would be grateful for any advice on this.  

Regards, 
   Andrei Popescu