Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello,

I realized that the equations I sketched the other day did not make much
sense. What I meant was more like the following:

\big'[op/x0]_(x <- [::]) F x = x0 (* should never happen *)
\big'[op/x0]_(x <- [:: a]) F x = F a
\big'[op/x0]_(x <- a :: b :: s) F x =
  op (F a) (\big'[op/x0]_(x <- b :: s) F x)

That is,

\big[op/x0]_(x <- [:: a]) F x = op (F a) x0

is not good enough in my context context since [op] may not have an
identity element. The underlying [foldr1] I had in mind was something
like this:

Definition foldr1 (I R : Type) (op : R -> R -> R) F (x0 : R) :=
  fix foldr1_rec (s : seq I) : R :=
    match s with
    | [::] => x0
    | a :: s' => if nilp s' then F a else op (F a) (foldr1_rec s')
    end.

Variable (a b c d : nat) (F : nat -> nat).
Eval simpl in foldr1 addn F d [:: a; b; c].
(*  = F a + (F b + F c) *)

Anyone done something like this? In any case, I suppose

Definition mybig (I R : Type) (op : R -> R -> R) F (x0 : R) (s : seq I)
:= if s is a :: s' then \big[op/F a]_(x <- s') F x else x0.

is (at last for commutative op) one possible implementation.

Best,
Christian

On 27/11/17 17:37, Christian Doczkal wrote:
> Hello,
> 
> I'm currently working on a development where I would like to use bigops
> in a setting where I don't have identity elements (but where the ranges
> will always be nonempty)
> 
> I'm imagining something like
> 
>       \big'[op/x0]_(x <- s | p) F
> 
> where
> 
>       \big'[op/x0]_(x <- [::] | p) F = F x0
>       \big'[op/x0]_(x <- a::s | p) F = F (\big'[op/a]_(x <- s | p))
> 
> (i.e., "\big[op/x0]_(x <- a::s | p) F" does not depend on "x0") I would
> want to treat both associative and commutative operators.
> 
> I guess this can be achieved using a variant of bigops where foldr is
> replaced with a suitable "foldr1". But before I start duplicating the
> relevant parts of the bigop library, I would like to ask if someone has
> - done this already
> - tried this an rejected the idea due to the theory getting messy
> - or can think of a simpler alternative
> 
> Thanks in advance,
> Christian
>