Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Felipe,

Felipe Cerqueira 
<>
 writes:

> When you provide these reflection lemmas, does it help with the Eval
> of the computation?

It was an example of replacing "A :|: B" by "union A B".

The first is a "locked" operation, (that is to say, it won't compute),
whereas the second should be able to.

I'm sorry for the example that now I realize it was confusing.

The idea there was that, as it currently stands, you'll have a non-ideal
time computing with some operations in ssreflect, thus sometimes you can
replace them with computable versions as a workaround.

> I was not able to pinpoint where the computation stops, but after
> looking at the end of the file it really seems to be the big sum
> operator (\big plus):

Indeed that's a likely candidate, as Laurent pointed out, a \bigop won't
compute by default, but you can "unlock" it and it will compute.

However, you may still have problems with the enumeration of the indexes
(the function that generates the list of "i"s in "\big_i F") computing.

In that case you may need to define your operations directly with a fold
+ an explicit enumeration, and prove them equivalent to the bigop
(usually easy if your operator is commutative)

You may wonder what is this "locking" about?

I think you can get some more details in the original bigop paper and in
the ssreflect manual, but the basic idea is that "locked" definitions
are prevented from expanding to its body to help type checking and proofs.

For instance, a bigop is defined as:

> CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
>
> Definition applybig {R I} (body : bigbody R I) x :=
>   let: BigBody _ op b v := body in if b then op v x else x.
>
> Definition reducebig R I idx r (body : I -> bigbody R I) :=
>   foldr (applybig \o body) idx r.

which even if it looks technical it really boils down to a foldr + a
filter over a list "r". (You can try yourself).

However, it would be very inconvenient if in the middle of a proof,
your nice "\sum_i n^+i" would get reduced to some:

"foldr (applybig \o [fun i => ...]) 0 (enum ...).

making it unreadable and what is worse, hard to reach for most rewriting
lemmas.

Thus, locking the bigop definition avoids that problem, at the cost of
impeding computation, that is, \sum_i F won't reduce at all.

Many other definitions are locked in ssreflect (ffuns, finsets,
matrices), in order not to expose their internals.

In order to reduce them, you can use "rewrite unlock" but usually it
works a bit better to use the corresponding E lemmas (ffunE, mxE), to
perform reduction in a more controlled, if not automatic :(, way.

Note that in this case, "big_cons" and "big_nil" would be the natural
alternative to unlocking.

I hope it helps, sorry if the above sounds a bit confusing.

Best regards,
E.