Is there a reason this is Admitted, other then that people are busy?
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).
Thanks! We're using it for a cryptographic library soon to be released.
Which parts of mathcomp analysis are you using?
I'm not the most familiar with this, but we are using it for (sub-)distributions mostly I think.
https://github.com/SSProve/ssprove
Paper to be released soon.
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))
Yep, that's the reason I asked :-)
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
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, ...
Inmathcomp
sRstruct.v
an instance is built from any instance of the
abstractstdlib
reals. An instance of the latter is built from the
(constructive) Cauchy reals inCoq.Reals.ClassicalConstructiveReals
.
@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!
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.
@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: Feb 05 2023 at 07:03 UTC