Ssreflect Users Discussion List

[Daniel Selsam <>]

Hi,

I am trying to do a simple calculation involving bigops, but can't figure out 
how to actually perform the computation. 
Here is a toy example that illustrates the problem:

<<
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype 
tuple finfun bigop.

Definition eval_ffun (f : {ffun unit -> bool}) := if f tt then 1 else 0.
Goal \sum_(f : {ffun unit -> bool}) eval_ffun f = 1.
Proof. (* ?? *)
>>

Is there a particular solution for the case of bigops with finTypes? 

I have similar issues all the time with various parts of the Mathematical 
Components library, though I often get lucky by not using notations, and 
alternating between searching for elimination lemmas and manually unfolding 
everything I see. Is there a generic way to perform exhaustive computations 
(e.g. a tactic that unlocks everything and computes as much as possible)?

The CoqEAL methodology seems to address this problem in spirit, though I am 
not sure how I would apply it to this problem.

Thanks,

Daniel