Ssreflect Users Discussion List

The lemma big_trivIset doesn't work on operations

   \big[op/idx]_(x \in cover P)

because this value isn't in the form of \big[op/idx]_(x \in cover P | K x)

In order to use this lemma you need to convert it to

  \big[op/idx]_(x \in cover P | true)

And there is no lemma to do this in the bigop.v libary that I found.

My current solution is:

have HP : (fun i => i \in cover [set (set_of_coset x) | x <- s]) =1
          (fun i => (i \in cover [set (set_of_coset x) | x <- s]) && true).
 by move => i; rewrite /= andbT.
rewrite (eq_bigl _ _ HP).

which is pretty heavy.

I found in PFsection2.v the somewhat lighter-weight:

have big_andT := eq_bigl _ _ (fun _ => andbT _).
rewrite -big_andT.

But still, if everyone who uses big_trivIset has to do this manipulation; 
it seems like a defect in the library; either in the bigops library, or a 
problem with big_trivIset lemma.

I'm a little surprised that the notation for this is defined as:

Notation "\big [ op / idx ]_ ( i \in A | P ) F" :=
  (\big[op/idx]_(i | (i \in A) && P) F) : big_scope.

instead of as

Notation "\big [ op / idx ]_ ( i \in A | P ) F" :=
  (\big[op/idx]_(i | P && (i \in A)) F) : big_scope.

Because if the latter were the notation, then I think

\big[op/idx]_(x \in cover P)
and
\big[op/idx]_(x \in cover P | true)

would be convertable; which would seem to be much more convinient.  I 
presume there is some clever reason for defining the notation the way it 
is defined.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''