## Stream: math-comp users

### Topic: ✔ Bigop sum of types

#### Pierre Jouvelot (Feb 14 2023 at 20:12):

Is there a way to make `Bar` work?

``````Definition Foo := ('I_0 + 'I_1 + 'I_2)%type. (* typechecks *)
Definition Bar := (\sum_(n < 3) 'I_n)%type. (*fails *)
``````

#### Enrico Tassi (Feb 14 2023 at 20:23):

Maybe, but you then won't get all the theory, since I don't see how `X + empty = X` can be proved (without axioms).
In any case, what you need is something like this https://github.com/math-comp/math-comp/blob/a9ac8e97405122cbccabf205465c4622a34c8e9c/mathcomp/ssreflect/bigop.v#L627 for type_scope.

#### Pierre Jouvelot (Feb 14 2023 at 20:31):

I was more thinking in terms of separate union, for which such an equality doesn't hold.

#### Alexander Gryzlov (Feb 14 2023 at 21:27):

We have stuff like that in FCSL-PCM, but yeah, you need setoid rewriting and it's generally not very flexible: https://github.com/imdea-software/fcsl-pcm/blob/master/pcm/pcm.v#L1376-L1377

#### Emilio Jesús Gallego Arias (Feb 15 2023 at 15:16):

Indeed @Pierre Jouvelot , unless you want to add some axioms about type equality, the theory will be quite weak so may be better off with just

``````Fixpoint isum n (T : nat -> Type) :=
match n with
| O => T 0
| S n => (isum n T + T n)%type
end.

Compute (isum 2 ordinal).
``````

#### Laurent Théry (Feb 15 2023 at 15:49):

In a recent PR, I saw this trick to jump to option type to get a neutral element (this was for `big_max` I think). You can do the same here but I am not sure it makes sense in your case but the trick is nice

``````Definition otpair (A B : option Type) :=
if A is Some A1 then if B is Some B1 then Some (A1 * B1)%type else A else B.

Check \big[otpair/None]_(i < 3) (Some 'I_i).
``````

#### Pierre Roux (Feb 15 2023 at 15:58):

I think it's available in the last coq-mathcomp-ssreflect.1.16.0 : https://github.com/math-comp/math-comp/blob/a9ac8e97405122cbccabf205465c4622a34c8e9c/mathcomp/ssreflect/bigop.v#L824

#### Notification Bot (Feb 15 2023 at 19:30):

Pierre Jouvelot has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC