Mathcomp and SSReflect FAQ

Boolean reflexion

• proving a reflect A B lemma

  apply: (iffP idP).
  

• This works with more complicated reflexion lemmas than idP , for example:

  reflect (forall x, x \in E -> ...) [forall (x | x \in E), ...]
  

  is proved using:

  apply (iffP forall_inP)
  

• proving the equality of two booleans by double implications:

  apply/idP/idP.
  

congr in hypothesis:

• My goal is of the form

  a = b -> P
  

  I'd like to transform it as

  f a = f b -> P
  

  This is achieved by

  move/(congr1 f).
  

Bigops

Bigops of the form \big_(i <- r | P i) F i

In general lemmas on bigops on sequences are not relativized by the sequence. e.g. eq_bigr asks to prove forall i, P i -> _ instead of forall i, i \in r -> P i -> _...

The reason is threefold:

1. the dependency on the indexes drops from eqType to Type
2. the lemma applies seamlessly to other summations, on fintypes, without introducing a spurious forall r, r \in T, ... quantification in the premisse
3. the relativisation can always be recovered using big_seq_cond.

Bigops of the form \big_(i in A | P i) F i

They might seem not general enough to cover goals containing a bigop of the form \big_(i <- r | P i) _, but they can always be used by turning the latter into \big_(i < size r | P (tnth r i)) F (tnth r i) through big_tnth.