pocket_prover-set

Crates.iopocket_prover-set
lib.rspocket_prover-set
version0.5.0
sourcesrc
created_at2018-02-23 11:06:07.215792
updated_at2022-10-07 21:47:16.557389
descriptionA base logical system for PocketProver to reason about set properties
homepagehttps://github.com/advancedresearch/pocket_prover-set
repositoryhttps://github.com/advancedresearch/pocket_prover-set.git
max_upload_size
id52503
size19,088
Sven Nilsen (bvssvni)

documentation

https://docs.rs/pocket_prover-set

README

pocket_prover-set

A base logical system for PocketProver to reason about set properties

extern crate pocket_prover;
extern crate pocket_prover_set;

use pocket_prover::*;
use pocket_prover_set::*;

fn main() {
    println!("Result {}", Set::imply(
        |s| s.fin_many,
        |s| not(s.inf_many)
    ));
}

There are 4 bits of information, used to derive all other properties:

  • any - All types, including those not defined
  • uniq - A unique value
  • fin_many - Many but finite number of values
  • inf_many - Many but infinite number of values

A set is empty (.none()) when all bits are set to 0.

A set is non-empty (.some()) when at least bit is set to 1.

A set is undefined when it is any but neither unique, finite or infinite.

Here is an example of a proof of 8 sets:

extern crate pocket_prover;
extern crate pocket_prover_set;

use pocket_prover::*;
use pocket_prover_set::*;

fn main() {
    println!("Result {}", <(Set, Set, Set, Set, Set, Set, Set, Set)>::imply(
        |sets| and(sets.uniqs(|xs| xorn(xs)), sets.0.uniq),
        |sets| not(sets.7.uniq)
    ));
}
Commit count: 18

cargo fmt