The Coq mailing list

[Andrei Popescu <uuomul AT yahoo.com>]

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 analysis, since I am attempting to eliminate Prop on Set. I would be grateful for any advice about this.  Is what I am trying to do violating the constructivity principles behind Coq?

Regards,
   Andrei Popescu

---

Be a better friend, newshound, and 
know-it-all with Yahoo! Mobile.  Try it now.