Stream: math-comp analysis

Topic: interchange_psum


view this post on Zulip Bas Spitters (Mar 09 2021 at 09:07):

Is there a reason this is Admitted, other then that people are busy?

view this post on Zulip Cyril Cohen (Mar 09 2021 at 11:53):

No other reason to my knowledge. Actually all files in the subdirectorythoeries/altreal predate most of the contents of the main theories directory and are here for bookkeeping mainly. Some maintainers of the library are in the middle of a refactoring that will port realsum.v(among other files) to the main theories directory (which contains and will never contain Admitted results).

view this post on Zulip Bas Spitters (Mar 09 2021 at 12:54):

Thanks! We're using it for a cryptographic library soon to be released.

view this post on Zulip Cyril Cohen (Mar 09 2021 at 13:06):

Which parts of mathcomp analysis are you using?

view this post on Zulip Théo Winterhalter (Mar 09 2021 at 14:32):

I'm not the most familiar with this, but we are using it for (sub-)distributions mostly I think.

view this post on Zulip Bas Spitters (Mar 09 2021 at 15:18):

https://github.com/SSProve/ssprove
Paper to be released soon.

view this post on Zulip Enrico Tassi (Mar 09 2021 at 15:25):

Finally, by using mathcomp-analysis we also inherit an admitted lemma they have:

interchange_psum :
  ∀ (R : realType) (T U : choiceType) (S : T → U → R),
    (∀ x : T, summable (T:=U) (R:=R) (S x)) →
    summable (T:=T) (R:=R) (λ x : T, psum (λ y : U, S x y)) →
    psum (λ x : T, psum (λ y : U, S x y)) =
    psum (λ y : U, psum (λ x : T, S x y))

view this post on Zulip Bas Spitters (Mar 09 2021 at 15:27):

Yep, that's the reason I asked :-)

view this post on Zulip Pierre-Yves Strub (Mar 10 2021 at 10:57):

I think this is on my shoulders. Indeed, I am currently refactoring this module and fixing the last admits (including the ones in distr.v). I will also import some of the developments I made on couplings in distr.v. E.g., the ones in https://github.com/strub/xhl/blob/master/prhl/prhl.v

view this post on Zulip Catalin Hritcu (Mar 27 2021 at 08:27):

https://github.com/SSProve/ssprove
Paper to be released soon.

Here it goes: https://eprint.iacr.org/2021/397

Beyond interchange_psum, we're also disclosing the following mathcomp-analysis axiom :)

R : realType

One could plug in any real number construction: Cauchy, Dedekind, ...
In mathcomps Rstruct.v an instance is built from any instance of the
abstract stdlib reals. An instance of the latter is built from the
(constructive) Cauchy reals in Coq.Reals.ClassicalConstructiveReals.

view this post on Zulip Bas Spitters (Mar 27 2021 at 10:53):

@Pierre-Yves Strub @Théo Winterhalter will look into porting SSProve to the newest version of mc analysis. Is there anything we should be aware of in regards to the changes you are planning?
BTW: Once again, thanks for the great library on distributions!

view this post on Zulip Pierre-Yves Strub (Mar 27 2021 at 16:22):

Currently, in the last version of mc analysis, distr.ec has been unchanged. However, for the next release, I'll push a major revamp of the library.

view this post on Zulip Bas Spitters (Mar 28 2021 at 09:09):

@Pierre-Yves Strub What would be the best way to make sure our code doesn't break (too much...)
Is there anything we should anticipate?


Last updated: Aug 19 2022 at 20:03 UTC