Stream: math-comp users

Topic: ✔ Bigop sum of types


view this post on Zulip 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 *)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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