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
History
File Mode Size
config
examples
lint
scripts
src
theories
.dir-locals.el -rw-r--r-- 285 bytes
.gitignore -rw-r--r-- 515 bytes
.merlin -rw-r--r-- 241 bytes
.travis.yml -rw-r--r-- 2.0 KB
COPYRIGHT -rw-r--r-- 581 bytes
COPYRIGHT.yaml -rw-r--r-- 596 bytes
MANIFEST -rw-r--r-- 596 bytes
Makefile -rw-r--r-- 4.8 KB
Makefile.system -rw-r--r-- 555 bytes
README.md -rw-r--r-- 8.3 KB
_tags -rw-r--r-- 812 bytes
default.nix -rw-r--r-- 225 bytes
myocamlbuild.ml -rw-r--r-- 2.3 KB

README.md

back to top