Skip to Content.
Sympa Menu

ssreflect - RE: [ssreflect] a new question about bigop (for Sophie...)

Subject: Ssreflect Users Discussion List

List archive

RE: [ssreflect] a new question about bigop (for Sophie...)


Chronological Thread 
  • From: Georges Gonthier <>
  • To: Laurence Rideau <>, "" <>
  • Subject: RE: [ssreflect] a new question about bigop (for Sophie...)
  • Date: Thu, 19 Jun 2014 08:55:36 +0000
  • Accept-language: en-GB, en-US
  • Authentication-results: spf=pass (sender IP is 131.107.125.37) ;

Mostly, because the lemmas were most useful in this form. The most
important bigop lemmas, which provide exchange and reindexing, are restricted
to finType-indexed bigops, so in practice most uses of bigops use finType
indexes, i.e., ranging over index_enum I, possibly with a filter predicate.
Wherever possible I have tried to generalize bigop lemmas to work with
explicit ranges whenever the more general form handles the index_enum case
transparently. In some cases this involved strengthening some assumptions to
match the finType case: e.g., eq_bigl assumes P1 =1 P2, forcing P1 and P2 to
coincide even outside of the range r. However for the big_max lemmas the
assumptions for the general range case would have been stronger than those
for the finType case, so we would have to use the more complicated general
form, exposing spurious "i \in index_enum I" conditions in "normal"
conditions.
In such cases my design decision was to provide only the simpler form,
letting the user convert his bigop to the finType form using
big_nth/big_mkord or big_tnth. That said, we have been extending support for
explicit ranges, though mostly for explicit-range lemmas that can't be easily
emulated via such a conversion.
Cheers,
Georges

-----Original Message-----
From:
[] On Behalf Of Laurence Rideau
Sent: 18 June 2014 14:43
To:
Subject: [ssreflect] a new question about bigop (for Sophie...)

We are trying to use bigop for the max operator.
The question is :
why are the properties proved on finite types (and not on sequences)?

thanks
laurence & sophie.





Archive powered by MHonArc 2.6.18.

Top of Page