Ssreflect Users Discussion List

[Vladimir Komendantsky <>]

Dear ssr users,

I would appreciate to have your advice. What would be the canonical
way of handling the following? Is it better to use more higher-level
kinds of "big" expressions as opposed to those that range over plain
sequences?

For example, there is a pair of congruent "big" expressions where
range of the first expression is (seq 'I_n) and the range of the
second is (seq 'I_(n + m)). So, using congr_big from scratch would
fail, because congr_big has a simple equality of range #1 and range #2
among the premisses, while this situation expects some kind of a
dependent one.

The second range of type ('I_(n + m)) can be formed by (pmap insub r)
where r is the sequence of naturals by projecting the first range of
type ('I_n) with val (that is, nat_of_ord).  The range (pmap insub r)
can be mapped to r by the lemma big_pmap that I prove below, and then
r can be lifted to type ('I_n) again by pmap insub, but now with
different implicit parameters.

It doesn't seem that (pmap insub) is used directly often in the
libraries. So, maybe my method is too low-level. I mean, maybe
unifying somehow the types of ranges from the start would help? The
crux of the problem, as it seems, is that there is no straightforward
way to subtype 'I_n in 'I_(n + m), which is why I pull back to nat...


Lemma insub_pmapK (T : eqType) (s : seq T) (P : pred T)
    (sT : subType P) (u : sub_eqType sT) n :
  all P s ->
  val (nth u (pmap insub s) n) = nth (val u) s n.
elim: s n => [n | a s IHs n all_s /=]; first by rewrite !nth_nil.
case: insubP; last by move/negP; case/andP: all_s.
by case: n => [|n] //=; rewrite -IHs //; case/andP: all_s.
Qed.

(* a variation on big_map from bigop.v *)
Lemma big_pmap (T : Type) (idx : T) (op : T -> T -> T) (J : eqType) (r : seq 
J)
    (sJ : pred J) (I : subType sJ) (P : pred I) (F : I -> T) (j0 :
sub_eqType I) :
  all sJ r ->
  \big[op/idx]_(i <- pmap insub r | P i) F i =
  \big[op/idx]_(j <- r | P (insubd j0 j)) F (insubd j0 j).
move=> all_r.
rewrite (big_nth j0) (big_nth (val j0)).
have nth_sub: forall i, i < size r -> nth (val j0) r i \in sJ.
  by move=> i i_size; move/allP: all_r; apply; apply: mem_nth.
apply: congr_big_nat => // [| i i_size | i /andP [Pi i_size]].
  by rewrite size_pmap_sub; apply/eqP; rewrite -all_count.
  by congr P; apply: val_inj; rewrite insub_pmapK // insubdK //; exact: 
nth_sub.
by congr F; apply: val_inj; rewrite insub_pmapK // insubdK //; exact: nth_sub.
Qed.


Best regards,
Vladimir