Stream: math-comp analysis

Topic: interchange_psum

Bas Spitters (Mar 09 2021 at 09:07):

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

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

Bas Spitters (Mar 09 2021 at 12:54):

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

Cyril Cohen (Mar 09 2021 at 13:06):

Which parts of mathcomp analysis are you using?

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.

Bas Spitters (Mar 09 2021 at 15:18):

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

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

Bas Spitters (Mar 09 2021 at 15:27):

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

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

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.

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!

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.

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