oxilean_std/bool/
functions_2.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, InductiveEnv, Level, Name};
6
7use super::functions::*;
8use super::types::*;
9
10/// Check that (Bool, XOR, AND) satisfies ring axioms by exhaustive verification.
11#[allow(dead_code)]
12pub fn verify_gf2_ring() -> bool {
13    let vals = [false, true];
14    for &a in &vals {
15        for &b in &vals {
16            for &c in &vals {
17                if gf2_add(gf2_add(a, b), c) != gf2_add(a, gf2_add(b, c)) {
18                    return false;
19                }
20                if gf2_mul(a, gf2_add(b, c)) != gf2_add(gf2_mul(a, b), gf2_mul(a, c)) {
21                    return false;
22                }
23            }
24        }
25    }
26    true
27}
28/// Verify De Morgan laws by exhaustive truth table check.
29#[allow(dead_code)]
30pub fn verify_demorgan() -> bool {
31    let vals = [false, true];
32    for &a in &vals {
33        for &b in &vals {
34            if !(a && b) != (!a || !b) {
35                return false;
36            }
37            if !(a || b) != (!a && !b) {
38                return false;
39            }
40        }
41    }
42    true
43}
44/// Verify lattice absorption laws by exhaustive check.
45#[allow(dead_code, clippy::overly_complex_bool_expr)]
46pub fn verify_lattice_absorption() -> bool {
47    let vals = [false, true];
48    for &a in &vals {
49        for &b in &vals {
50            if (a && (a || b)) != a {
51                return false;
52            }
53            if (a || (a && b)) != a {
54                return false;
55            }
56        }
57    }
58    true
59}
60/// Verify all basic Boolean algebra laws exhaustively.
61#[allow(dead_code)]
62pub fn verify_boolean_algebra() -> bool {
63    verify_demorgan() && verify_gf2_ring() && verify_lattice_absorption()
64}
65/// Verify Kleene three-value logic satisfies De Morgan-like laws.
66#[allow(dead_code)]
67pub fn verify_kleene_demorgan() -> bool {
68    let vals = [Kleene3Val::False, Kleene3Val::Unknown, Kleene3Val::True];
69    for &a in &vals {
70        for &b in &vals {
71            if a.and(b).not() != a.not().or(b.not()) {
72                return false;
73            }
74            if a.or(b).not() != a.not().and(b.not()) {
75                return false;
76            }
77        }
78    }
79    true
80}
81/// A decision procedure for Bool predicates that checks all values.
82#[allow(dead_code)]
83pub fn decide_bool_pred(pred: impl Fn(bool) -> bool) -> Option<bool> {
84    if pred(true) {
85        Some(true)
86    } else if pred(false) {
87        Some(false)
88    } else {
89        None
90    }
91}
92/// Verify XOR monoid laws: (Bool, XOR, false) is a commutative group.
93#[allow(dead_code)]
94pub fn verify_xor_monoid() -> bool {
95    let vals = [false, true];
96    for &a in &vals {
97        if a ^ false != a {
98            return false;
99        }
100        #[allow(clippy::eq_op)]
101        if a ^ a {
102            return false;
103        }
104        for &b in &vals {
105            #[allow(clippy::eq_op)]
106            if (a ^ b) != (b ^ a) {
107                return false;
108            }
109            for &c in &vals {
110                if ((a ^ b) ^ c) != (a ^ (b ^ c)) {
111                    return false;
112                }
113            }
114        }
115    }
116    true
117}
118/// Check NAND functional completeness by expressing NOT via NAND.
119/// NOT a = NAND a a
120#[allow(dead_code, clippy::eq_op)]
121pub fn nand_not(a: bool) -> bool {
122    !(a && a)
123}
124/// Check NOR functional completeness by expressing NOT via NOR.
125/// NOT a = NOR a a
126#[allow(dead_code, clippy::eq_op)]
127pub fn nor_not(a: bool) -> bool {
128    !(a || a)
129}
130/// Verify that NAND and NOR implement NOT correctly.
131#[allow(dead_code)]
132pub fn verify_functional_completeness() -> bool {
133    !nand_not(true) && nand_not(false) && !nor_not(true) && nor_not(false)
134}
135#[cfg(test)]
136mod extended_bool_tests {
137    use super::*;
138    fn setup_extended_env() -> (Environment, InductiveEnv) {
139        let mut env = Environment::new();
140        let ind_env = InductiveEnv::new();
141        env.add(Declaration::Axiom {
142            name: Name::str("DecidableEq"),
143            univ_params: vec![],
144            ty: Expr::Pi(
145                BinderInfo::Default,
146                Name::str("a"),
147                Box::new(Expr::Sort(Level::succ(Level::zero()))),
148                Box::new(Expr::Sort(Level::succ(Level::zero()))),
149            ),
150        })
151        .expect("operation should succeed");
152        env.add(Declaration::Axiom {
153            name: Name::str("sorry"),
154            univ_params: vec![],
155            ty: Expr::Sort(Level::zero()),
156        })
157        .expect("operation should succeed");
158        (env, ind_env)
159    }
160    #[test]
161    fn test_register_bool_extended_axioms() {
162        let (mut env, mut ind_env) = setup_extended_env();
163        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
164        register_bool_extended_axioms(&mut env);
165        assert!(env.contains(&Name::str("Bool.demorgan_and")));
166        assert!(env.contains(&Name::str("Bool.demorgan_or")));
167        assert!(env.contains(&Name::str("Bool.and_complement")));
168        assert!(env.contains(&Name::str("Bool.or_complement")));
169        assert!(env.contains(&Name::str("Bool.and_idempotent")));
170        assert!(env.contains(&Name::str("Bool.or_idempotent")));
171        assert!(env.contains(&Name::str("Bool.and_absorption")));
172        assert!(env.contains(&Name::str("Bool.or_absorption")));
173    }
174    #[test]
175    fn test_bool_extended_xor_axioms() {
176        let (mut env, mut ind_env) = setup_extended_env();
177        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
178        register_bool_extended_axioms(&mut env);
179        assert!(env.contains(&Name::str("Bool.xor_self")));
180        assert!(env.contains(&Name::str("Bool.xor_assoc")));
181        assert!(env.contains(&Name::str("Bool.and_distrib_xor")));
182        assert!(env.contains(&Name::str("Bool.xor_false")));
183        assert!(env.contains(&Name::str("Bool.xor_true")));
184        assert!(env.contains(&Name::str("Bool.xor_not_beq")));
185    }
186    #[test]
187    fn test_bool_extended_heyting() {
188        let (mut env, mut ind_env) = setup_extended_env();
189        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
190        register_bool_extended_axioms(&mut env);
191        assert!(env.contains(&Name::str("BoolImply")));
192        assert!(env.contains(&Name::str("Bool.imply_def")));
193        assert!(env.contains(&Name::str("Bool.imply_refl")));
194    }
195    #[test]
196    fn test_bool_extended_sat_instance() {
197        let mut sat = SATInstance::new(2);
198        sat.add_clause(vec![1, 2]);
199        sat.add_clause(vec![-1, 2]);
200        let solution = sat.solve();
201        assert!(solution.is_some());
202        let sol = solution.expect("solution should be valid");
203        assert!(sat.evaluate(&sol));
204    }
205    #[test]
206    fn test_sat_unsat() {
207        let mut sat = SATInstance::new(1);
208        sat.add_clause(vec![1]);
209        sat.add_clause(vec![-1]);
210        assert!(sat.solve().is_none());
211    }
212    #[test]
213    fn test_gf2_ring_verify() {
214        assert!(verify_gf2_ring());
215    }
216    #[test]
217    fn test_demorgan_verify() {
218        assert!(verify_demorgan());
219    }
220    #[test]
221    fn test_lattice_absorption_verify() {
222        assert!(verify_lattice_absorption());
223    }
224    #[test]
225    fn test_boolean_algebra_full_verify() {
226        assert!(verify_boolean_algebra());
227    }
228    #[test]
229    fn test_xor_monoid_verify() {
230        assert!(verify_xor_monoid());
231    }
232    #[test]
233    fn test_functional_completeness() {
234        assert!(verify_functional_completeness());
235    }
236    #[test]
237    fn test_kleene_three_value_not() {
238        assert_eq!(Kleene3Val::True.not(), Kleene3Val::False);
239        assert_eq!(Kleene3Val::False.not(), Kleene3Val::True);
240        assert_eq!(Kleene3Val::Unknown.not(), Kleene3Val::Unknown);
241    }
242    #[test]
243    fn test_kleene_three_value_and() {
244        assert_eq!(Kleene3Val::True.and(Kleene3Val::True), Kleene3Val::True);
245        assert_eq!(Kleene3Val::True.and(Kleene3Val::False), Kleene3Val::False);
246        assert_eq!(
247            Kleene3Val::True.and(Kleene3Val::Unknown),
248            Kleene3Val::Unknown
249        );
250        assert_eq!(
251            Kleene3Val::False.and(Kleene3Val::Unknown),
252            Kleene3Val::False
253        );
254    }
255    #[test]
256    fn test_kleene_three_value_or() {
257        assert_eq!(Kleene3Val::False.or(Kleene3Val::False), Kleene3Val::False);
258        assert_eq!(Kleene3Val::False.or(Kleene3Val::True), Kleene3Val::True);
259        assert_eq!(
260            Kleene3Val::False.or(Kleene3Val::Unknown),
261            Kleene3Val::Unknown
262        );
263        assert_eq!(Kleene3Val::True.or(Kleene3Val::Unknown), Kleene3Val::True);
264    }
265    #[test]
266    fn test_kleene_demorgan() {
267        assert!(verify_kleene_demorgan());
268    }
269    #[test]
270    fn test_decide_bool_pred_some() {
271        let result = decide_bool_pred(|b| b);
272        assert_eq!(result, Some(true));
273    }
274    #[test]
275    fn test_decide_bool_pred_none() {
276        let result = decide_bool_pred(|_| false);
277        assert_eq!(result, None);
278    }
279    #[test]
280    fn test_nand_not() {
281        assert!(!nand_not(true));
282        assert!(nand_not(false));
283    }
284    #[test]
285    fn test_nor_not() {
286        assert!(!nor_not(true));
287        assert!(nor_not(false));
288    }
289    #[test]
290    fn test_bool_algebra_struct() {
291        let ba = BoolAlgebra {
292            carrier_size: 2,
293            involutive: true,
294            de_morgan: true,
295        };
296        assert_eq!(ba.carrier_size, 2);
297        assert!(ba.involutive);
298        assert!(ba.de_morgan);
299    }
300    #[test]
301    fn test_xor_monoid_struct() {
302        let xm = XorMonoid {
303            identity: false,
304            associative: true,
305            self_inverse: true,
306        };
307        assert!(!xm.identity);
308        assert!(xm.self_inverse);
309    }
310    #[test]
311    fn test_bool_lattice_struct() {
312        let bl = BoolLattice {
313            bottom: false,
314            top: true,
315            distributive: true,
316            complemented: true,
317        };
318        assert!(!bl.bottom);
319        assert!(bl.top);
320        assert!(bl.distributive);
321        assert!(bl.complemented);
322    }
323    #[test]
324    fn test_decidable_pred_struct() {
325        let dp: DecidablePred<i32> = DecidablePred {
326            decide: Box::new(|x| *x > 0),
327            name: "positive".to_string(),
328        };
329        assert!((dp.decide)(&5));
330        assert!(!(dp.decide)(&-1));
331    }
332    #[test]
333    fn test_kleene3_from_bool() {
334        assert_eq!(Kleene3Val::from_bool(true), Kleene3Val::True);
335        assert_eq!(Kleene3Val::from_bool(false), Kleene3Val::False);
336    }
337    #[test]
338    fn test_bool_extended_monoid_axioms() {
339        let (mut env, mut ind_env) = setup_extended_env();
340        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
341        register_bool_extended_axioms(&mut env);
342        assert!(env.contains(&Name::str("Bool.and_monoid_left_id")));
343        assert!(env.contains(&Name::str("Bool.and_monoid_right_id")));
344        assert!(env.contains(&Name::str("Bool.or_monoid_left_id")));
345        assert!(env.contains(&Name::str("Bool.or_monoid_right_id")));
346    }
347    #[test]
348    fn test_bool_extended_fold_axioms() {
349        let (mut env, mut ind_env) = setup_extended_env();
350        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
351        register_bool_extended_axioms(&mut env);
352        assert!(env.contains(&Name::str("BoolAll")));
353        assert!(env.contains(&Name::str("BoolAny")));
354    }
355    #[test]
356    fn test_bool_extended_ite_axioms() {
357        let (mut env, mut ind_env) = setup_extended_env();
358        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
359        register_bool_extended_axioms(&mut env);
360        assert!(env.contains(&Name::str("BoolIte")));
361        assert!(env.contains(&Name::str("BoolIte.true_branch")));
362        assert!(env.contains(&Name::str("BoolIte.false_branch")));
363    }
364    #[test]
365    fn test_bool_extended_nand_nor() {
366        let (mut env, mut ind_env) = setup_extended_env();
367        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
368        register_bool_extended_axioms(&mut env);
369        assert!(env.contains(&Name::str("Bool.nand")));
370        assert!(env.contains(&Name::str("Bool.nand_def")));
371        assert!(env.contains(&Name::str("Bool.nor")));
372        assert!(env.contains(&Name::str("Bool.nor_def")));
373    }
374    #[test]
375    fn test_bool_extended_kleene3_registered() {
376        let (mut env, mut ind_env) = setup_extended_env();
377        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
378        register_bool_extended_axioms(&mut env);
379        assert!(env.contains(&Name::str("Kleene3")));
380        assert!(env.contains(&Name::str("Kleene3.unknown")));
381        assert!(env.contains(&Name::str("Kleene3.and")));
382    }
383    #[test]
384    fn test_bool_extended_beq_axioms() {
385        let (mut env, mut ind_env) = setup_extended_env();
386        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
387        register_bool_extended_axioms(&mut env);
388        assert!(env.contains(&Name::str("Bool.beq_true")));
389        assert!(env.contains(&Name::str("Bool.beq_false")));
390        assert!(env.contains(&Name::str("Bool.beq_iff_eq_aux")));
391        assert!(env.contains(&Name::str("BEqBoolInst")));
392    }
393    #[test]
394    fn test_sat_instance_empty() {
395        let sat = SATInstance::new(3);
396        let solution = sat.solve();
397        assert!(solution.is_some());
398    }
399    #[test]
400    fn test_sat_instance_tautological_clause() {
401        let mut sat = SATInstance::new(1);
402        sat.add_clause(vec![1, -1]);
403        assert!(sat.solve().is_some());
404    }
405    #[test]
406    fn test_gf2_add_mul() {
407        assert!(!gf2_add(false, false));
408        assert!(gf2_add(true, false));
409        assert!(gf2_add(false, true));
410        assert!(!gf2_add(true, true));
411        assert!(!gf2_mul(false, false));
412        assert!(!gf2_mul(true, false));
413        assert!(!gf2_mul(false, true));
414        assert!(gf2_mul(true, true));
415    }
416    #[test]
417    fn test_bool_extended_demorgan_duality() {
418        let (mut env, mut ind_env) = setup_extended_env();
419        build_bool_env(&mut env, &mut ind_env).expect("build_bool_env should succeed");
420        register_bool_extended_axioms(&mut env);
421        assert!(env.contains(&Name::str("DeMorganDuality")));
422        assert!(env.contains(&Name::str("SATDecidable")));
423        assert!(env.contains(&Name::str("TautologyCheck")));
424    }
425}
oxilean_std/bool/functions_2.rs

oxilean_std/bool/
functions_2.rs
