Pierre Jouvelot (Feb 14 2023 at 20:12): 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 *)
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).
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
Notification Bot (Feb 15 2023 at 19:30):Pierre Jouvelot has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC