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 *)
```

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.

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

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

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).
```

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).
```

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

Pierre Jouvelot has marked this topic as resolved.

Last updated: Jul 15 2024 at 20:02 UTC