pocket_prover_set/
lib.rs

1#![deny(missing_docs)]
2
3//! # pocket_prover-set
4//! A base logical system for PocketProver to reason about set properties
5//!
6//! ```rust
7//! extern crate pocket_prover;
8//! extern crate pocket_prover_set;
9//!
10//! use pocket_prover::*;
11//! use pocket_prover_set::*;
12//!
13//! fn main() {
14//!     println!("Result {}", Set::imply(
15//!         |s| s.fin_many,
16//!         |s| not(s.inf_many)
17//!     ));
18//! }
19//! ```
20//!
21//! There are 4 bits of information, used to derive all other properties:
22//!
23//! - `any` - All types, including those not defined
24//! - `uniq` - A unique value
25//! - `fin_many` - Many but finite number of values
26//! - `inf_many` - Many but infinite number of values
27//!
28//! A set is empty (`.none()`) when all bits are set to 0.
29//!
30//! A set is non-empty (`.some()`) when at least bit is set to 1.
31//!
32//! A set is undefined when it is `any` but neither unique, finite or infinite.
33//!
34//! Here is an example of a proof of 6 sets:
35//!
36//! ```rust
37//! extern crate pocket_prover;
38//! extern crate pocket_prover_set;
39//!
40//! use pocket_prover::*;
41//! use pocket_prover_set::*;
42//!
43//! fn main() {
44//!     println!("Result {}", <(Set, Set, Set, Set, Set, Set)>::imply(
45//!         |sets| and(sets.uniqs(|xs| xorn(xs)), sets.0.uniq),
46//!         |sets| not(sets.5.uniq)
47//!     ));
48//! }
49//! ```
50//!
51
52extern crate pocket_prover;
53#[macro_use]
54extern crate pocket_prover_derive;
55
56use pocket_prover::*;
57
58/// Conditions that holds for a set in general.
59#[derive(Copy, Clone, Construct)]
60pub struct Set {
61    /// All types, including those who are not defined.
62    pub any: u64,
63    /// A unique value.
64    pub uniq: u64,
65    /// Many but finite number of values.
66    pub fin_many: u64,
67    /// Many but infinite number of values.
68    pub inf_many: u64,
69}
70
71impl CoreRules for Set {
72    fn core_rules(&self) -> u64 {self.rules()}
73}
74
75impl ExtendRules for Set {
76    type Inner = ();
77    fn inner(&self) -> &() {&()}
78    fn extend_rules(&self, _: &Self::Inner) -> u64 {T}
79}
80
81impl Set {
82    /// Rules for sets.
83    pub fn rules(&self) -> u64 {
84        and(
85            imply(or3(self.uniq, self.fin_many, self.inf_many), and(self.some(), not(self.any))),
86            imply(self.some(), xor4(self.uniq, self.fin_many, self.inf_many, self.any))
87        )
88    }
89
90    /// Returns whether the set is empty.
91    pub fn none(&self) -> u64 {
92        not(or4(self.any, self.uniq, self.fin_many, self.inf_many))
93    }
94
95    /// Returns whether the set is non-empty.
96    pub fn some(&self) -> u64 {
97        or4(self.any, self.uniq, self.fin_many, self.inf_many)
98    }
99
100    /// Returns whether the set is undefined.
101    /// This can be a set of higher cardinality.
102    pub fn undefined(&self) -> u64 {
103        and4(self.any, not(self.uniq), not(self.fin_many), not(self.inf_many))
104    }
105
106    /// Returns whether the set contains more than one.
107    /// The set must be well defined.
108    pub fn multiple(&self) -> u64 {
109        or(self.fin_many, self.inf_many)
110    }
111
112    /// Counts the number of true cases.
113    pub fn count<F: Fn(Set) -> u64>(f: F) -> u64 {
114        count4(&mut |any, uniq, fin_many, inf_many| {
115            f(Set {any, uniq, fin_many, inf_many})
116        })
117    }
118}
119
120/// Implemented on tuples of sets to access arrays of same kind of bits.
121pub trait MSet {
122    /// Do something with the `any` bits.
123    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
124    /// Do something with the `uniq` bits.
125    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
126    /// Do something with the `fin_many` bits.
127    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
128    /// Do something with the `inf_many` bits.
129    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64;
130}
131
132impl MSet for (Set, Set) {
133    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
134        f(&[self.0.any, self.1.any])
135    }
136    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
137        f(&[self.0.uniq, self.1.uniq])
138    }
139    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
140        f(&[self.0.fin_many, self.1.fin_many])
141    }
142    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
143        f(&[self.0.inf_many, self.1.inf_many])
144    }
145}
146
147impl MSet for (Set, Set, Set) {
148    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
149        f(&[self.0.any, self.1.any, self.2.any])
150    }
151    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
152        f(&[self.0.uniq, self.1.uniq, self.2.uniq])
153    }
154    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
155        f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many])
156    }
157    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
158        f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many])
159    }
160}
161
162impl MSet for (Set, Set, Set, Set) {
163    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
164        f(&[self.0.any, self.1.any, self.2.any, self.3.any])
165    }
166    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
167        f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq])
168    }
169    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
170        f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many])
171    }
172    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
173        f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many])
174    }
175}
176
177impl MSet for (Set, Set, Set, Set, Set) {
178    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
179        f(&[self.0.any, self.1.any, self.2.any, self.3.any, self.4.any])
180    }
181    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
182        f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq, self.4.uniq])
183    }
184    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
185        f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many, self.4.fin_many])
186    }
187    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
188        f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many, self.4.inf_many])
189    }
190}
191
192impl MSet for (Set, Set, Set, Set, Set, Set) {
193    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
194        f(&[self.0.any, self.1.any, self.2.any, self.3.any, self.4.any, self.5.any])
195    }
196    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
197        f(&[self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq, self.4.uniq, self.5.uniq])
198    }
199    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
200        f(&[self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
201            self.4.fin_many, self.5.fin_many])
202    }
203    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
204        f(&[self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
205            self.4.inf_many, self.5.inf_many])
206    }
207}
208
209impl MSet for (Set, Set, Set, Set, Set, Set, Set) {
210    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
211        f(&[
212            self.0.any, self.1.any, self.2.any, self.3.any,
213            self.4.any, self.5.any, self.6.any
214        ])
215    }
216    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
217        f(&[
218            self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq,
219            self.4.uniq, self.5.uniq, self.6.uniq
220        ])
221    }
222    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
223        f(&[
224            self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
225            self.4.fin_many, self.5.fin_many, self.6.fin_many
226        ])
227    }
228    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
229        f(&[
230            self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
231            self.4.inf_many, self.5.inf_many, self.6.inf_many
232        ])
233    }
234}
235
236impl MSet for (Set, Set, Set, Set, Set, Set, Set, Set) {
237    fn anys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
238        f(&[
239            self.0.any, self.1.any, self.2.any, self.3.any,
240            self.4.any, self.5.any, self.6.any, self.7.any
241        ])
242    }
243    fn uniqs<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
244        f(&[
245            self.0.uniq, self.1.uniq, self.2.uniq, self.3.uniq,
246            self.4.uniq, self.5.uniq, self.6.uniq, self.7.uniq
247        ])
248    }
249    fn fin_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
250        f(&[
251            self.0.fin_many, self.1.fin_many, self.2.fin_many, self.3.fin_many,
252            self.4.fin_many, self.5.fin_many, self.6.fin_many, self.7.fin_many
253        ])
254    }
255    fn inf_manys<F: Fn(&[u64]) -> u64>(&self, f: F) -> u64 {
256        f(&[
257            self.0.inf_many, self.1.inf_many, self.2.inf_many, self.3.inf_many,
258            self.4.inf_many, self.5.inf_many, self.6.inf_many, self.7.inf_many
259        ])
260    }
261}
262
263#[cfg(test)]
264mod tests {
265    use super::*;
266
267    #[test]
268    fn both_none_and_some_means_uniq_is_nonsense() {
269        assert!(!Set::means(
270            |s| and(s.none(), s.some()),
271            |s| not(s.uniq)
272        ));
273    }
274
275    #[test]
276    fn multiple_is_exclusive_from_undefined() {
277        assert!(Set::exc(
278            |s| s.multiple(),
279            |s| s.undefined()
280        ));
281    }
282
283    #[test]
284    fn some_includes_undefined() {
285        assert!(!Set::exc(
286            |s| s.some(),
287            |s| s.undefined()
288        ));
289    }
290
291    #[test]
292    fn none_is_not_some() {
293        assert!(Set::imply(|s| s.none(), |s| not(s.some())));
294    }
295
296    #[test]
297    fn some_is_not_none() {
298        assert!(Set::imply(|s| s.some(), |s| not(s.none())));
299    }
300
301    #[test]
302    fn some_is_eq_not_none() {
303        assert!(Set::eq(|s| s.some(), |s| not(s.none())));
304    }
305
306    #[test]
307    fn uniq_is_some() {
308        assert!(Set::imply(|s| s.uniq, |s| s.some()));
309    }
310
311    #[test]
312    fn uniq_is_not_fin_many() {
313        assert!(Set::imply(|s| s.uniq, |s| not(s.fin_many)))
314    }
315
316    #[test]
317    fn any_is_some() {
318        assert!(Set::imply(|s| s.any, |s| s.some()));
319    }
320
321    #[test]
322    fn fin_many_is_some() {
323        assert!(Set::imply(|s| s.fin_many, |s| s.some()));
324    }
325
326    #[test]
327    fn inf_many_is_some() {
328        assert!(Set::imply(|s| s.inf_many, |s| s.some()));
329    }
330
331    #[test]
332    fn some_does_not_mean_any() {
333        assert!(Set::does_not_mean(|s| s.some(), |s| s.any));
334    }
335
336    #[test]
337    fn not_uniq_and_not_none_is_either_fin_many_inf_many_or_any() {
338        assert!(Set::imply(
339            |s| and(not(s.uniq), not(s.none())),
340            |s| or3(s.fin_many, s.inf_many, s.any)
341        ));
342    }
343
344    #[test]
345    fn fin_many_is_not_inf_many() {
346        assert!(Set::imply(|s| s.fin_many, |s| not(s.inf_many)));
347    }
348
349    #[test]
350    fn not_fin_many_does_not_mean_inf_many() {
351        assert!(Set::does_not_mean(|s| not(s.fin_many), |s| s.inf_many));
352    }
353
354    #[test]
355    fn none_is_equal_to_neither_uniq_fin_many_inf_many_or_any() {
356        assert!(Set::eq(
357            |s| s.none(),
358            |s| not(or4(s.uniq, s.fin_many, s.inf_many, s.any))
359        ));
360    }
361
362    #[test]
363    fn undefined_is_some() {
364        assert!(Set::imply(
365            |s| s.undefined(),
366            |s| s.some()
367        ));
368    }
369}
pocket_prover_set/lib.rs

pocket_prover_set/
lib.rs
