Revision 9e114126d5961fa73a21372b8a44f64723d79242 authored by François Dupressoir on 16 January 2020, 20:48:25 UTC, committed by François Dupressoir on 16 January 2020, 20:48:25 UTC
This pushes several complex low-level arguments related to sampling
in restricted distributions into the related distribution file.

This also generalizes these arguments, so that:
- TwoStepSampling no longer requires a full distribution,
- WhileSampling takes distributions and tests as procedure arguments
  rather than clone parameters.

Specialized versions of theories and lemmas that reproduce the old
behaviours are also included.

The Dice_Sampling theory is removed, replaced with
Dexcepted.WhileSamplingFixedTest (an abstract theory).

Squashed commit of the following:

commit e4bf1725f2a327bc58dda51d0079acb8dbb8fb1a
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Jan 16 20:40:23 2020 +0000

    trailing white space in modified files

commit 12d5ff0ae8607be10f7e925d1f0d44dd8e78dbde
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Dec 19 15:49:41 2019 +0000

    minor cleanup

commit 7921a24e13e9f6d19ad02c0a22e8efb49bc37184
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Dec 19 13:47:19 2019 +0000

    More general ways of sampling out of a predicate

    TwoStep no longer requires losslessness. More sharing of proof could be
    obtained

commit 393700f85b47b9d373be983b1451b08ae3d3be94
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Dec 5 21:40:16 2019 +0000

    PRP<->PRF uses generic resampling

commit 74b9aef924cc313e358510ab9f83bc7410489db4
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Dec 5 21:27:12 2019 +0000

    Slight generalization: no longer need a full distribution

commit 0853fc0e313bb6adac0ad956417480ebd70f512f
Author: François Dupressoir <fdupress@gmail.com>
Date:   Thu Dec 5 18:34:43 2019 +0000

    Dexcepted: equivalence between two ways of sampling

    used in PRP<->PRF, but also in a current proof

    TODO: make PRP<->PRF use this
1 parent cd341ca
Raw File
.gitignore
*~
_build
*.native
*.byte
*.exe
*.pyc
*.pyo
.vagrant
/local
/why3
/_tools
/proofgeneral/_local
setup.data
setup.log
/attic
/attic.ec*
/theories/attic

/system/*.o
/system/callprover
/system/callprover.exe

*.aux
*.bbl
*.blg
*.brf
*.fdb_latexmk
*.fls
*.idx
*.ilg
*.ind
*.log
*.out
*.toc
*.synctex.gz
*.kilepr
*.eco
/src/ecVersion.ml

/doc/refman/easycrypt.pdf
/doc/userman/easycrypt.pdf

/extraction/Makefile
/extraction/setup.*
/extraction/configure
/extraction/_build/

/sandbox
/attic

/*.ec
*.eco

/*.smt
/*.why
back to top