oxilean_std/bool/
functions.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::types::{BoolExpr, TruthTable};
8
9/// The Bool type expression.
10#[allow(dead_code)]
11pub fn bool_ty() -> Expr {
12    Expr::Const(Name::str("Bool"), vec![])
13}
14/// Create a `true` expression.
15pub fn bool_true() -> Expr {
16    Expr::Const(Name::str("true"), vec![])
17}
18/// Create a `false` expression.
19pub fn bool_false() -> Expr {
20    Expr::Const(Name::str("false"), vec![])
21}
22/// Create `Bool.not b`.
23#[allow(dead_code)]
24pub fn bool_not(b: Expr) -> Expr {
25    Expr::App(
26        Box::new(Expr::Const(Name::str("Bool.not"), vec![])),
27        Box::new(b),
28    )
29}
30/// Create `Bool.and a b`.
31#[allow(dead_code)]
32pub fn bool_and(a: Expr, b: Expr) -> Expr {
33    Expr::App(
34        Box::new(Expr::App(
35            Box::new(Expr::Const(Name::str("Bool.and"), vec![])),
36            Box::new(a),
37        )),
38        Box::new(b),
39    )
40}
41/// Create `Bool.or a b`.
42#[allow(dead_code)]
43pub fn bool_or(a: Expr, b: Expr) -> Expr {
44    Expr::App(
45        Box::new(Expr::App(
46            Box::new(Expr::Const(Name::str("Bool.or"), vec![])),
47            Box::new(a),
48        )),
49        Box::new(b),
50    )
51}
52/// Create `Bool.xor a b`.
53#[allow(dead_code)]
54pub fn bool_xor(a: Expr, b: Expr) -> Expr {
55    Expr::App(
56        Box::new(Expr::App(
57            Box::new(Expr::Const(Name::str("Bool.xor"), vec![])),
58            Box::new(a),
59        )),
60        Box::new(b),
61    )
62}
63/// Create `Bool.beq a b`.
64#[allow(dead_code)]
65pub fn bool_beq(a: Expr, b: Expr) -> Expr {
66    Expr::App(
67        Box::new(Expr::App(
68            Box::new(Expr::Const(Name::str("Bool.beq"), vec![])),
69            Box::new(a),
70        )),
71        Box::new(b),
72    )
73}
74/// Create `Bool.rec motive false_case true_case b`.
75#[allow(dead_code)]
76pub fn bool_rec(motive: Expr, false_case: Expr, true_case: Expr, b: Expr) -> Expr {
77    Expr::App(
78        Box::new(Expr::App(
79            Box::new(Expr::App(
80                Box::new(Expr::App(
81                    Box::new(Expr::Const(Name::str("Bool.rec"), vec![])),
82                    Box::new(motive),
83                )),
84                Box::new(false_case),
85            )),
86            Box::new(true_case),
87        )),
88        Box::new(b),
89    )
90}
91/// Create `Eq a b` where both are Bool.
92#[allow(dead_code)]
93pub fn mk_bool_eq(a: Expr, b: Expr) -> Expr {
94    Expr::App(
95        Box::new(Expr::App(
96            Box::new(Expr::App(
97                Box::new(Expr::Const(Name::str("Eq"), vec![])),
98                Box::new(bool_ty()),
99            )),
100            Box::new(a),
101        )),
102        Box::new(b),
103    )
104}
105pub fn arrow(a: Expr, b: Expr) -> Expr {
106    Expr::Pi(
107        BinderInfo::Default,
108        Name::Anonymous,
109        Box::new(a),
110        Box::new(b),
111    )
112}
113pub fn forall_bool(name: &str, body: Expr) -> Expr {
114    Expr::Pi(
115        BinderInfo::Default,
116        Name::str(name),
117        Box::new(bool_ty()),
118        Box::new(body),
119    )
120}
121pub fn eq_bool(lhs: Expr, rhs: Expr) -> Expr {
122    Expr::App(
123        Box::new(Expr::App(
124            Box::new(Expr::App(
125                Box::new(Expr::Const(Name::str("Eq"), vec![])),
126                Box::new(bool_ty()),
127            )),
128            Box::new(lhs),
129        )),
130        Box::new(rhs),
131    )
132}
133/// Build the Bool type and all associated declarations.
134pub fn build_bool_env(env: &mut Environment, _ind_env: &mut InductiveEnv) -> Result<(), String> {
135    let type1 = Expr::Sort(Level::succ(Level::zero()));
136    let bool_c = bool_ty();
137    env.add(Declaration::Axiom {
138        name: Name::str("Bool"),
139        univ_params: vec![],
140        ty: type1.clone(),
141    })
142    .map_err(|e| e.to_string())?;
143    env.add(Declaration::Axiom {
144        name: Name::str("true"),
145        univ_params: vec![],
146        ty: bool_c.clone(),
147    })
148    .map_err(|e| e.to_string())?;
149    env.add(Declaration::Axiom {
150        name: Name::str("false"),
151        univ_params: vec![],
152        ty: bool_c.clone(),
153    })
154    .map_err(|e| e.to_string())?;
155    env.add(Declaration::Axiom {
156        name: Name::str("Bool.not"),
157        univ_params: vec![],
158        ty: arrow(bool_c.clone(), bool_c.clone()),
159    })
160    .map_err(|e| e.to_string())?;
161    env.add(Declaration::Axiom {
162        name: Name::str("Bool.and"),
163        univ_params: vec![],
164        ty: arrow(bool_c.clone(), arrow(bool_c.clone(), bool_c.clone())),
165    })
166    .map_err(|e| e.to_string())?;
167    env.add(Declaration::Axiom {
168        name: Name::str("Bool.or"),
169        univ_params: vec![],
170        ty: arrow(bool_c.clone(), arrow(bool_c.clone(), bool_c.clone())),
171    })
172    .map_err(|e| e.to_string())?;
173    env.add(Declaration::Axiom {
174        name: Name::str("Bool.xor"),
175        univ_params: vec![],
176        ty: arrow(bool_c.clone(), arrow(bool_c.clone(), bool_c.clone())),
177    })
178    .map_err(|e| e.to_string())?;
179    env.add(Declaration::Axiom {
180        name: Name::str("Bool.beq"),
181        univ_params: vec![],
182        ty: arrow(bool_c.clone(), arrow(bool_c.clone(), bool_c.clone())),
183    })
184    .map_err(|e| e.to_string())?;
185    let u = Name::str("u");
186    let sort_u = Expr::Sort(Level::Param(u.clone()));
187    let motive_ty = arrow(bool_c.clone(), sort_u);
188    let rec_ty = Expr::Pi(
189        BinderInfo::Implicit,
190        Name::str("C"),
191        Box::new(motive_ty),
192        Box::new(Expr::Pi(
193            BinderInfo::Default,
194            Name::str("hf"),
195            Box::new(Expr::App(Box::new(Expr::BVar(0)), Box::new(bool_false()))),
196            Box::new(Expr::Pi(
197                BinderInfo::Default,
198                Name::str("ht"),
199                Box::new(Expr::App(Box::new(Expr::BVar(1)), Box::new(bool_true()))),
200                Box::new(Expr::Pi(
201                    BinderInfo::Default,
202                    Name::str("b"),
203                    Box::new(bool_c.clone()),
204                    Box::new(Expr::App(Box::new(Expr::BVar(3)), Box::new(Expr::BVar(0)))),
205                )),
206            )),
207        )),
208    );
209    env.add(Declaration::Axiom {
210        name: Name::str("Bool.rec"),
211        univ_params: vec![u.clone()],
212        ty: rec_ty,
213    })
214    .map_err(|e| e.to_string())?;
215    let cases_motive_ty = arrow(bool_c.clone(), Expr::Sort(Level::Param(u.clone())));
216    let cases_ty = Expr::Pi(
217        BinderInfo::Implicit,
218        Name::str("C"),
219        Box::new(cases_motive_ty),
220        Box::new(Expr::Pi(
221            BinderInfo::Default,
222            Name::str("b"),
223            Box::new(bool_c.clone()),
224            Box::new(Expr::Pi(
225                BinderInfo::Default,
226                Name::str("hf"),
227                Box::new(Expr::App(Box::new(Expr::BVar(1)), Box::new(bool_false()))),
228                Box::new(Expr::Pi(
229                    BinderInfo::Default,
230                    Name::str("ht"),
231                    Box::new(Expr::App(Box::new(Expr::BVar(2)), Box::new(bool_true()))),
232                    Box::new(Expr::App(Box::new(Expr::BVar(3)), Box::new(Expr::BVar(2)))),
233                )),
234            )),
235        )),
236    );
237    env.add(Declaration::Axiom {
238        name: Name::str("Bool.casesOn"),
239        univ_params: vec![u],
240        ty: cases_ty,
241    })
242    .map_err(|e| e.to_string())?;
243    let dec_eq_bool = Expr::App(
244        Box::new(Expr::Const(Name::str("DecidableEq"), vec![])),
245        Box::new(bool_c.clone()),
246    );
247    env.add(Declaration::Axiom {
248        name: Name::str("Bool.decEq"),
249        univ_params: vec![],
250        ty: dec_eq_bool,
251    })
252    .map_err(|e| e.to_string())?;
253    env.add(Declaration::Axiom {
254        name: Name::str("BEq"),
255        univ_params: vec![],
256        ty: arrow(
257            Expr::Sort(Level::succ(Level::zero())),
258            Expr::Sort(Level::succ(Level::zero())),
259        ),
260    })
261    .map_err(|e| e.to_string())?;
262    let beq_beq_ty = Expr::Pi(
263        BinderInfo::Implicit,
264        Name::str("a"),
265        Box::new(type1),
266        Box::new(Expr::Pi(
267            BinderInfo::InstImplicit,
268            Name::str("inst"),
269            Box::new(Expr::App(
270                Box::new(Expr::Const(Name::str("BEq"), vec![])),
271                Box::new(Expr::BVar(0)),
272            )),
273            Box::new(Expr::Pi(
274                BinderInfo::Default,
275                Name::str("x"),
276                Box::new(Expr::BVar(1)),
277                Box::new(Expr::Pi(
278                    BinderInfo::Default,
279                    Name::str("y"),
280                    Box::new(Expr::BVar(2)),
281                    Box::new(bool_c),
282                )),
283            )),
284        )),
285    );
286    env.add(Declaration::Axiom {
287        name: Name::str("BEq.beq"),
288        univ_params: vec![],
289        ty: beq_beq_ty,
290    })
291    .map_err(|e| e.to_string())?;
292    add_eq_if_missing(env)?;
293    add_bool_theorem(
294        env,
295        "Bool.not_not",
296        forall_bool(
297            "b",
298            eq_bool(bool_not(bool_not(Expr::BVar(0))), Expr::BVar(0)),
299        ),
300    )?;
301    add_bool_theorem(
302        env,
303        "Bool.and_true",
304        forall_bool(
305            "b",
306            eq_bool(bool_and(Expr::BVar(0), bool_true()), Expr::BVar(0)),
307        ),
308    )?;
309    add_bool_theorem(
310        env,
311        "Bool.true_and",
312        forall_bool(
313            "b",
314            eq_bool(bool_and(bool_true(), Expr::BVar(0)), Expr::BVar(0)),
315        ),
316    )?;
317    add_bool_theorem(
318        env,
319        "Bool.and_false",
320        forall_bool(
321            "b",
322            eq_bool(bool_and(Expr::BVar(0), bool_false()), bool_false()),
323        ),
324    )?;
325    add_bool_theorem(
326        env,
327        "Bool.false_and",
328        forall_bool(
329            "b",
330            eq_bool(bool_and(bool_false(), Expr::BVar(0)), bool_false()),
331        ),
332    )?;
333    add_bool_theorem(
334        env,
335        "Bool.or_true",
336        forall_bool(
337            "b",
338            eq_bool(bool_or(Expr::BVar(0), bool_true()), bool_true()),
339        ),
340    )?;
341    add_bool_theorem(
342        env,
343        "Bool.true_or",
344        forall_bool(
345            "b",
346            eq_bool(bool_or(bool_true(), Expr::BVar(0)), bool_true()),
347        ),
348    )?;
349    add_bool_theorem(
350        env,
351        "Bool.or_false",
352        forall_bool(
353            "b",
354            eq_bool(bool_or(Expr::BVar(0), bool_false()), Expr::BVar(0)),
355        ),
356    )?;
357    add_bool_theorem(
358        env,
359        "Bool.false_or",
360        forall_bool(
361            "b",
362            eq_bool(bool_or(bool_false(), Expr::BVar(0)), Expr::BVar(0)),
363        ),
364    )?;
365    add_bool_theorem(
366        env,
367        "Bool.and_comm",
368        forall_bool(
369            "a",
370            forall_bool(
371                "b",
372                eq_bool(
373                    bool_and(Expr::BVar(1), Expr::BVar(0)),
374                    bool_and(Expr::BVar(0), Expr::BVar(1)),
375                ),
376            ),
377        ),
378    )?;
379    add_bool_theorem(
380        env,
381        "Bool.or_comm",
382        forall_bool(
383            "a",
384            forall_bool(
385                "b",
386                eq_bool(
387                    bool_or(Expr::BVar(1), Expr::BVar(0)),
388                    bool_or(Expr::BVar(0), Expr::BVar(1)),
389                ),
390            ),
391        ),
392    )?;
393    add_bool_theorem(
394        env,
395        "Bool.and_assoc",
396        forall_bool(
397            "a",
398            forall_bool(
399                "b",
400                forall_bool(
401                    "c",
402                    eq_bool(
403                        bool_and(bool_and(Expr::BVar(2), Expr::BVar(1)), Expr::BVar(0)),
404                        bool_and(Expr::BVar(2), bool_and(Expr::BVar(1), Expr::BVar(0))),
405                    ),
406                ),
407            ),
408        ),
409    )?;
410    add_bool_theorem(
411        env,
412        "Bool.or_assoc",
413        forall_bool(
414            "a",
415            forall_bool(
416                "b",
417                forall_bool(
418                    "c",
419                    eq_bool(
420                        bool_or(bool_or(Expr::BVar(2), Expr::BVar(1)), Expr::BVar(0)),
421                        bool_or(Expr::BVar(2), bool_or(Expr::BVar(1), Expr::BVar(0))),
422                    ),
423                ),
424            ),
425        ),
426    )?;
427    add_bool_theorem(
428        env,
429        "Bool.and_or_distrib",
430        forall_bool(
431            "a",
432            forall_bool(
433                "b",
434                forall_bool(
435                    "c",
436                    eq_bool(
437                        bool_and(Expr::BVar(2), bool_or(Expr::BVar(1), Expr::BVar(0))),
438                        bool_or(
439                            bool_and(Expr::BVar(2), Expr::BVar(1)),
440                            bool_and(Expr::BVar(2), Expr::BVar(0)),
441                        ),
442                    ),
443                ),
444            ),
445        ),
446    )?;
447    add_bool_theorem(
448        env,
449        "Bool.not_true",
450        eq_bool(bool_not(bool_true()), bool_false()),
451    )?;
452    add_bool_theorem(
453        env,
454        "Bool.not_false",
455        eq_bool(bool_not(bool_false()), bool_true()),
456    )?;
457    add_bool_theorem(
458        env,
459        "Bool.xor_comm",
460        forall_bool(
461            "a",
462            forall_bool(
463                "b",
464                eq_bool(
465                    bool_xor(Expr::BVar(1), Expr::BVar(0)),
466                    bool_xor(Expr::BVar(0), Expr::BVar(1)),
467                ),
468            ),
469        ),
470    )?;
471    add_bool_theorem(
472        env,
473        "Bool.beq_refl",
474        forall_bool(
475            "b",
476            eq_bool(bool_beq(Expr::BVar(0), Expr::BVar(0)), bool_true()),
477        ),
478    )?;
479    add_bool_theorem(
480        env,
481        "Bool.eq_of_beq",
482        forall_bool(
483            "a",
484            forall_bool(
485                "b",
486                Expr::Pi(
487                    BinderInfo::Default,
488                    Name::str("h"),
489                    Box::new(eq_bool(bool_beq(Expr::BVar(1), Expr::BVar(0)), bool_true())),
490                    Box::new(eq_bool(Expr::BVar(2), Expr::BVar(1))),
491                ),
492            ),
493        ),
494    )?;
495    Ok(())
496}
497/// Add Eq to environment if not already present.
498pub fn add_eq_if_missing(env: &mut Environment) -> Result<(), String> {
499    if env.contains(&Name::str("Eq")) {
500        return Ok(());
501    }
502    let type1 = Expr::Sort(Level::succ(Level::zero()));
503    let eq_ty = Expr::Pi(
504        BinderInfo::Implicit,
505        Name::str("a"),
506        Box::new(type1),
507        Box::new(Expr::Pi(
508            BinderInfo::Default,
509            Name::str("x"),
510            Box::new(Expr::BVar(0)),
511            Box::new(Expr::Pi(
512                BinderInfo::Default,
513                Name::str("y"),
514                Box::new(Expr::BVar(1)),
515                Box::new(Expr::Sort(Level::zero())),
516            )),
517        )),
518    );
519    env.add(Declaration::Axiom {
520        name: Name::str("Eq"),
521        univ_params: vec![],
522        ty: eq_ty,
523    })
524    .map_err(|e| e.to_string())
525}
526/// Add a theorem declaration with a sorry placeholder proof.
527pub fn add_bool_theorem(env: &mut Environment, name: &str, ty: Expr) -> Result<(), String> {
528    let val = Expr::Const(Name::str("sorry"), vec![]);
529    env.add(Declaration::Theorem {
530        name: Name::str(name),
531        univ_params: vec![],
532        ty,
533        val,
534    })
535    .map_err(|e| e.to_string())
536}
537#[cfg(test)]
538mod tests {
539    use super::*;
540    fn setup_env() -> (Environment, InductiveEnv) {
541        let mut env = Environment::new();
542        let ind_env = InductiveEnv::new();
543        env.add(Declaration::Axiom {
544            name: Name::str("DecidableEq"),
545            univ_params: vec![],
546            ty: Expr::Pi(
547                BinderInfo::Default,
548                Name::str("a"),
549                Box::new(Expr::Sort(Level::succ(Level::zero()))),
550                Box::new(Expr::Sort(Level::succ(Level::zero()))),
551            ),
552        })
553        .expect("operation should succeed");
554        env.add(Declaration::Axiom {
555            name: Name::str("sorry"),
556            univ_params: vec![],
557            ty: Expr::Sort(Level::zero()),
558        })
559        .expect("operation should succeed");
560        (env, ind_env)
561    }
562    #[test]
563    fn test_build_bool_env_full() {
564        let (mut env, mut ind_env) = setup_env();
565        assert!(build_bool_env(&mut env, &mut ind_env).is_ok());
566        assert!(env.contains(&Name::str("Bool")));
567        assert!(env.contains(&Name::str("true")));
568        assert!(env.contains(&Name::str("false")));
569        assert!(env.contains(&Name::str("Bool.not")));
570        assert!(env.contains(&Name::str("Bool.and")));
571        assert!(env.contains(&Name::str("Bool.or")));
572        assert!(env.contains(&Name::str("Bool.xor")));
573        assert!(env.contains(&Name::str("Bool.beq")));
574        assert!(env.contains(&Name::str("Bool.rec")));
575        assert!(env.contains(&Name::str("Bool.casesOn")));
576        assert!(env.contains(&Name::str("Bool.decEq")));
577        assert!(env.contains(&Name::str("BEq")));
578        assert!(env.contains(&Name::str("BEq.beq")));
579        for name in &[
580            "Bool.not_not",
581            "Bool.and_true",
582            "Bool.true_and",
583            "Bool.and_false",
584            "Bool.false_and",
585            "Bool.or_true",
586            "Bool.true_or",
587            "Bool.or_false",
588            "Bool.false_or",
589            "Bool.and_comm",
590            "Bool.or_comm",
591            "Bool.and_assoc",
592            "Bool.or_assoc",
593            "Bool.and_or_distrib",
594            "Bool.not_true",
595            "Bool.not_false",
596            "Bool.xor_comm",
597            "Bool.beq_refl",
598            "Bool.eq_of_beq",
599        ] {
600            assert!(env.contains(&Name::str(*name)), "missing: {}", name);
601        }
602    }
603    #[test]
604    fn test_bool_ty() {
605        let ty = bool_ty();
606        assert!(matches!(ty, Expr::Const(_, _)));
607    }
608    #[test]
609    fn test_bool_not_expr() {
610        let not_b = bool_not(bool_true());
611        assert!(matches!(not_b, Expr::App(_, _)));
612    }
613    #[test]
614    fn test_bool_and_expr() {
615        let e = bool_and(bool_true(), bool_false());
616        assert!(matches!(e, Expr::App(_, _)));
617    }
618    #[test]
619    fn test_bool_or_expr() {
620        let e = bool_or(bool_true(), bool_false());
621        assert!(matches!(e, Expr::App(_, _)));
622    }
623    #[test]
624    fn test_bool_xor_expr() {
625        let e = bool_xor(bool_true(), bool_false());
626        assert!(matches!(e, Expr::App(_, _)));
627    }
628    #[test]
629    fn test_bool_beq_expr() {
630        let e = bool_beq(bool_true(), bool_true());
631        assert!(matches!(e, Expr::App(_, _)));
632    }
633    #[test]
634    fn test_bool_rec_expr() {
635        let motive = Expr::Lam(
636            BinderInfo::Default,
637            Name::str("b"),
638            Box::new(bool_ty()),
639            Box::new(Expr::Sort(Level::succ(Level::zero()))),
640        );
641        let fc = Expr::Const(Name::str("Nat"), vec![]);
642        let tc = Expr::Const(Name::str("Bool"), vec![]);
643        let b = Expr::BVar(0);
644        let rec = bool_rec(motive, fc, tc, b);
645        assert!(matches!(rec, Expr::App(_, _)));
646    }
647    #[test]
648    fn test_mk_bool_eq_expr() {
649        let e = mk_bool_eq(bool_true(), bool_false());
650        assert!(matches!(e, Expr::App(_, _)));
651    }
652    #[test]
653    fn test_bool_true_false_distinct() {
654        assert_ne!(bool_true(), bool_false());
655    }
656    #[test]
657    fn test_bool_not_double_structure() {
658        let double = bool_not(bool_not(bool_true()));
659        match double {
660            Expr::App(ref func, _) => {
661                assert!(matches!(**func, Expr::Const(_, _)));
662            }
663            _ => panic!("Expected App"),
664        }
665    }
666    #[test]
667    fn test_bool_and_not_commutative_syntactically() {
668        let a = bool_true();
669        let b = bool_false();
670        let ab = bool_and(a.clone(), b.clone());
671        let ba = bool_and(b, a);
672        assert_ne!(ab, ba);
673    }
674    #[test]
675    fn test_bool_or_not_commutative_syntactically() {
676        let a = bool_true();
677        let b = bool_false();
678        let ab = bool_or(a.clone(), b.clone());
679        let ba = bool_or(b, a);
680        assert_ne!(ab, ba);
681    }
682    #[test]
683    fn test_bool_xor_binary() {
684        let e = bool_xor(bool_true(), bool_false());
685        match e {
686            Expr::App(ref f, _) => assert!(matches!(**f, Expr::App(_, _))),
687            _ => panic!("Expected nested App"),
688        }
689    }
690    #[test]
691    fn test_bool_beq_self() {
692        let b = bool_true();
693        let e = bool_beq(b.clone(), b);
694        assert!(matches!(e, Expr::App(_, _)));
695    }
696    #[test]
697    fn test_bool_rec_depth() {
698        let motive = Expr::Const(Name::str("M"), vec![]);
699        let fc = Expr::Const(Name::str("FC"), vec![]);
700        let tc = Expr::Const(Name::str("TC"), vec![]);
701        let b = Expr::Const(Name::str("bval"), vec![]);
702        let rec = bool_rec(motive, fc, tc, b);
703        let mut depth = 0;
704        let mut cur = &rec;
705        while let Expr::App(f, _) = cur {
706            depth += 1;
707            cur = f;
708        }
709        assert_eq!(depth, 4);
710    }
711    #[test]
712    fn test_mk_bool_eq_structure() {
713        let e = mk_bool_eq(bool_true(), bool_false());
714        match e {
715            Expr::App(ref inner, ref rhs) => {
716                assert_eq!(**rhs, bool_false());
717                match **inner {
718                    Expr::App(ref inner2, ref lhs) => {
719                        assert_eq!(**lhs, bool_true());
720                        match **inner2 {
721                            Expr::App(ref eq_c, ref ty) => {
722                                assert_eq!(**eq_c, Expr::Const(Name::str("Eq"), vec![]));
723                                assert_eq!(**ty, bool_ty());
724                            }
725                            _ => panic!("Expected App(Eq, Bool)"),
726                        }
727                    }
728                    _ => panic!("Expected App"),
729                }
730            }
731            _ => panic!("Expected App"),
732        }
733    }
734    #[test]
735    fn test_arrow_helper() {
736        let arr = arrow(bool_ty(), bool_ty());
737        match arr {
738            Expr::Pi(info, name, _, _) => {
739                assert_eq!(info, BinderInfo::Default);
740                assert_eq!(name, Name::Anonymous);
741            }
742            _ => panic!("Expected Pi"),
743        }
744    }
745    #[test]
746    fn test_forall_bool_helper() {
747        let fa = forall_bool("x", Expr::Sort(Level::zero()));
748        match fa {
749            Expr::Pi(info, name, ref dom, _) => {
750                assert_eq!(info, BinderInfo::Default);
751                assert_eq!(name, Name::str("x"));
752                assert_eq!(**dom, bool_ty());
753            }
754            _ => panic!("Expected Pi"),
755        }
756    }
757    #[test]
758    fn test_eq_bool_helper() {
759        let e = eq_bool(bool_true(), bool_false());
760        assert!(matches!(e, Expr::App(_, _)));
761    }
762    #[test]
763    fn test_build_bool_env_old_compat() {
764        let (mut env, mut ind_env) = setup_env();
765        assert!(build_bool_env(&mut env, &mut ind_env).is_ok());
766        assert!(env.contains(&Name::str("Bool")));
767        assert!(env.contains(&Name::str("true")));
768        assert!(env.contains(&Name::str("false")));
769    }
770    #[test]
771    fn test_bool_helpers_smoke() {
772        let _ = bool_ty();
773        let _ = bool_true();
774        let _ = bool_false();
775        let _ = bool_not(bool_true());
776        let _ = bool_and(bool_true(), bool_false());
777        let _ = bool_or(bool_true(), bool_false());
778        let _ = bool_xor(bool_true(), bool_false());
779        let _ = bool_beq(bool_true(), bool_true());
780        let _ = mk_bool_eq(bool_true(), bool_false());
781    }
782    #[test]
783    fn test_bool_rec_concrete_motive() {
784        let motive = Expr::Lam(
785            BinderInfo::Default,
786            Name::str("_"),
787            Box::new(bool_ty()),
788            Box::new(Expr::Sort(Level::zero())),
789        );
790        let fc = Expr::Const(Name::str("proof_false"), vec![]);
791        let tc = Expr::Const(Name::str("proof_true"), vec![]);
792        let result = bool_rec(motive, fc, tc, bool_true());
793        let mut depth = 0;
794        let mut cur = &result;
795        while let Expr::App(f, _) = cur {
796            depth += 1;
797            cur = f;
798        }
799        assert_eq!(depth, 4);
800    }
801}
802/// Standard boolean truth tables.
803/// Truth table for logical AND.
804#[allow(dead_code)]
805pub fn and_table() -> TruthTable {
806    TruthTable::compute("and", |a, b| a && b)
807}
808/// Truth table for logical OR.
809#[allow(dead_code)]
810pub fn or_table() -> TruthTable {
811    TruthTable::compute("or", |a, b| a || b)
812}
813/// Truth table for logical XOR.
814#[allow(dead_code)]
815pub fn xor_table() -> TruthTable {
816    TruthTable::compute("xor", |a, b| a ^ b)
817}
818/// Truth table for logical NAND.
819#[allow(dead_code)]
820pub fn nand_table() -> TruthTable {
821    TruthTable::compute("nand", |a, b| !(a && b))
822}
823/// Truth table for logical NOR.
824#[allow(dead_code)]
825pub fn nor_table() -> TruthTable {
826    TruthTable::compute("nor", |a, b| !(a || b))
827}
828/// Truth table for logical IFF (biconditional).
829#[allow(dead_code)]
830pub fn iff_table() -> TruthTable {
831    TruthTable::compute("iff", |a, b| a == b)
832}
833/// Truth table for logical implication.
834#[allow(dead_code)]
835pub fn imply_table() -> TruthTable {
836    TruthTable::compute("imply", |a, b| !a || b)
837}
838#[cfg(test)]
839mod extra_bool_tests {
840    use super::*;
841    #[test]
842    fn test_truth_table_and() {
843        let t = and_table();
844        assert!(!t.lookup(false, false));
845        assert!(!t.lookup(false, true));
846        assert!(!t.lookup(true, false));
847        assert!(t.lookup(true, true));
848        assert!(t.is_commutative());
849        assert!(!t.is_tautology());
850        assert!(!t.is_contradiction());
851        assert_eq!(t.true_count(), 1);
852    }
853    #[test]
854    fn test_truth_table_or() {
855        let t = or_table();
856        assert!(t.is_commutative());
857        assert_eq!(t.true_count(), 3);
858    }
859    #[test]
860    fn test_truth_table_xor() {
861        let t = xor_table();
862        assert!(t.is_commutative());
863        assert_eq!(t.true_count(), 2);
864    }
865    #[test]
866    fn test_truth_table_iff_is_tautology_when_a_eq_b() {
867        let t = iff_table();
868        assert!(t.lookup(false, false));
869        assert!(!t.lookup(false, true));
870        assert_eq!(t.true_count(), 2);
871    }
872    #[test]
873    fn test_truth_table_nand() {
874        let t = nand_table();
875        assert!(t.lookup(false, false));
876        assert!(!t.lookup(true, true));
877        assert_eq!(t.true_count(), 3);
878    }
879    #[test]
880    fn test_truth_table_nor_is_contradiction() {
881        let t = nor_table();
882        assert!(!t.is_tautology());
883        assert_eq!(t.true_count(), 1);
884    }
885    #[test]
886    fn test_bool_expr_const() {
887        let env = std::collections::HashMap::new();
888        assert_eq!(BoolExpr::Const(true).eval(&env), Some(true));
889        assert_eq!(BoolExpr::Const(false).eval(&env), Some(false));
890    }
891    #[test]
892    fn test_bool_expr_var() {
893        let mut env = std::collections::HashMap::new();
894        env.insert("x", true);
895        assert_eq!(BoolExpr::Var("x".to_string()).eval(&env), Some(true));
896        assert_eq!(BoolExpr::Var("y".to_string()).eval(&env), None);
897    }
898    #[test]
899    fn test_bool_expr_not() {
900        let mut env = std::collections::HashMap::new();
901        env.insert("x", false);
902        let expr = BoolExpr::Not(Box::new(BoolExpr::Var("x".to_string())));
903        assert_eq!(expr.eval(&env), Some(true));
904    }
905    #[test]
906    fn test_bool_expr_and() {
907        let mut env = std::collections::HashMap::new();
908        env.insert("a", true);
909        env.insert("b", false);
910        let expr = BoolExpr::And(
911            Box::new(BoolExpr::Var("a".to_string())),
912            Box::new(BoolExpr::Var("b".to_string())),
913        );
914        assert_eq!(expr.eval(&env), Some(false));
915    }
916    #[test]
917    fn test_bool_expr_or() {
918        let mut env = std::collections::HashMap::new();
919        env.insert("a", true);
920        env.insert("b", false);
921        let expr = BoolExpr::Or(
922            Box::new(BoolExpr::Var("a".to_string())),
923            Box::new(BoolExpr::Var("b".to_string())),
924        );
925        assert_eq!(expr.eval(&env), Some(true));
926    }
927    #[test]
928    fn test_bool_expr_implies() {
929        let mut env = std::collections::HashMap::new();
930        env.insert("a", true);
931        env.insert("b", false);
932        let expr = BoolExpr::Implies(
933            Box::new(BoolExpr::Var("a".to_string())),
934            Box::new(BoolExpr::Var("b".to_string())),
935        );
936        assert_eq!(expr.eval(&env), Some(false));
937    }
938    #[test]
939    fn test_bool_expr_is_tautology_true() {
940        let a = BoolExpr::Var("a".to_string());
941        let not_a = BoolExpr::Not(Box::new(BoolExpr::Var("a".to_string())));
942        let taut = BoolExpr::Or(Box::new(a), Box::new(not_a));
943        assert!(taut.is_tautology());
944    }
945    #[test]
946    fn test_bool_expr_is_tautology_false() {
947        let expr = BoolExpr::Var("x".to_string());
948        assert!(!expr.is_tautology());
949    }
950    #[test]
951    fn test_bool_expr_variables() {
952        let expr = BoolExpr::And(
953            Box::new(BoolExpr::Var("x".to_string())),
954            Box::new(BoolExpr::Or(
955                Box::new(BoolExpr::Var("y".to_string())),
956                Box::new(BoolExpr::Var("x".to_string())),
957            )),
958        );
959        let vars = expr.variables();
960        assert_eq!(vars.len(), 2);
961        assert!(vars.contains(&"x".to_string()));
962        assert!(vars.contains(&"y".to_string()));
963    }
964    #[test]
965    fn test_imply_table_commutative() {
966        let t = imply_table();
967        assert!(!t.is_commutative());
968    }
969}
970/// Build the De Morgan AND-NOT law: ¬(a ∧ b) = ¬a ∨ ¬b
971pub fn bl_ext_demorgan_and(env: &mut Environment) -> Result<(), String> {
972    let ty = forall_bool(
973        "a",
974        forall_bool(
975            "b",
976            eq_bool(
977                bool_not(bool_and(Expr::BVar(1), Expr::BVar(0))),
978                bool_or(bool_not(Expr::BVar(1)), bool_not(Expr::BVar(0))),
979            ),
980        ),
981    );
982    add_bool_theorem(env, "Bool.demorgan_and", ty)
983}
984/// Build the De Morgan OR-NOT law: ¬(a ∨ b) = ¬a ∧ ¬b
985pub fn bl_ext_demorgan_or(env: &mut Environment) -> Result<(), String> {
986    let ty = forall_bool(
987        "a",
988        forall_bool(
989            "b",
990            eq_bool(
991                bool_not(bool_or(Expr::BVar(1), Expr::BVar(0))),
992                bool_and(bool_not(Expr::BVar(1)), bool_not(Expr::BVar(0))),
993            ),
994        ),
995    );
996    add_bool_theorem(env, "Bool.demorgan_or", ty)
997}
998/// Build the AND complementation law: a ∧ ¬a = false
999pub fn bl_ext_and_complement(env: &mut Environment) -> Result<(), String> {
1000    let ty = forall_bool(
1001        "a",
1002        eq_bool(
1003            bool_and(Expr::BVar(0), bool_not(Expr::BVar(0))),
1004            bool_false(),
1005        ),
1006    );
1007    add_bool_theorem(env, "Bool.and_complement", ty)
1008}
1009/// Build the OR complementation law: a ∨ ¬a = true
1010pub fn bl_ext_or_complement(env: &mut Environment) -> Result<(), String> {
1011    let ty = forall_bool(
1012        "a",
1013        eq_bool(bool_or(Expr::BVar(0), bool_not(Expr::BVar(0))), bool_true()),
1014    );
1015    add_bool_theorem(env, "Bool.or_complement", ty)
1016}
1017/// Build the AND idempotency law: a ∧ a = a
1018pub fn bl_ext_and_idempotent(env: &mut Environment) -> Result<(), String> {
1019    let ty = forall_bool(
1020        "a",
1021        eq_bool(bool_and(Expr::BVar(0), Expr::BVar(0)), Expr::BVar(0)),
1022    );
1023    add_bool_theorem(env, "Bool.and_idempotent", ty)
1024}
1025/// Build the OR idempotency law: a ∨ a = a
1026pub fn bl_ext_or_idempotent(env: &mut Environment) -> Result<(), String> {
1027    let ty = forall_bool(
1028        "a",
1029        eq_bool(bool_or(Expr::BVar(0), Expr::BVar(0)), Expr::BVar(0)),
1030    );
1031    add_bool_theorem(env, "Bool.or_idempotent", ty)
1032}
1033/// Build the AND-OR absorption law: a ∧ (a ∨ b) = a
1034pub fn bl_ext_and_absorption(env: &mut Environment) -> Result<(), String> {
1035    let ty = forall_bool(
1036        "a",
1037        forall_bool(
1038            "b",
1039            eq_bool(
1040                bool_and(Expr::BVar(1), bool_or(Expr::BVar(1), Expr::BVar(0))),
1041                Expr::BVar(1),
1042            ),
1043        ),
1044    );
1045    add_bool_theorem(env, "Bool.and_absorption", ty)
1046}
1047/// Build the OR-AND absorption law: a ∨ (a ∧ b) = a
1048pub fn bl_ext_or_absorption(env: &mut Environment) -> Result<(), String> {
1049    let ty = forall_bool(
1050        "a",
1051        forall_bool(
1052            "b",
1053            eq_bool(
1054                bool_or(Expr::BVar(1), bool_and(Expr::BVar(1), Expr::BVar(0))),
1055                Expr::BVar(1),
1056            ),
1057        ),
1058    );
1059    add_bool_theorem(env, "Bool.or_absorption", ty)
1060}
1061/// Build the Bool-as-ring XOR ring axiom: (Bool, XOR, AND) forms a field GF(2).
1062pub fn bl_ext_xor_ring(env: &mut Environment) -> Result<(), String> {
1063    let ty = forall_bool(
1064        "a",
1065        eq_bool(bool_xor(Expr::BVar(0), Expr::BVar(0)), bool_false()),
1066    );
1067    add_bool_theorem(env, "Bool.xor_self", ty)
1068}
1069/// Build the XOR associativity law.
1070pub fn bl_ext_xor_assoc(env: &mut Environment) -> Result<(), String> {
1071    let ty = forall_bool(
1072        "a",
1073        forall_bool(
1074            "b",
1075            forall_bool(
1076                "c",
1077                eq_bool(
1078                    bool_xor(bool_xor(Expr::BVar(2), Expr::BVar(1)), Expr::BVar(0)),
1079                    bool_xor(Expr::BVar(2), bool_xor(Expr::BVar(1), Expr::BVar(0))),
1080                ),
1081            ),
1082        ),
1083    );
1084    add_bool_theorem(env, "Bool.xor_assoc", ty)
1085}
1086/// Build the AND distributivity over XOR law: a ∧ (b XOR c) = (a ∧ b) XOR (a ∧ c).
1087pub fn bl_ext_and_distrib_xor(env: &mut Environment) -> Result<(), String> {
1088    let ty = forall_bool(
1089        "a",
1090        forall_bool(
1091            "b",
1092            forall_bool(
1093                "c",
1094                eq_bool(
1095                    bool_and(Expr::BVar(2), bool_xor(Expr::BVar(1), Expr::BVar(0))),
1096                    bool_xor(
1097                        bool_and(Expr::BVar(2), Expr::BVar(1)),
1098                        bool_and(Expr::BVar(2), Expr::BVar(0)),
1099                    ),
1100                ),
1101            ),
1102        ),
1103    );
1104    add_bool_theorem(env, "Bool.and_distrib_xor", ty)
1105}
1106/// Build the lattice join-commutativity axiom (OR is commutative join).
1107pub fn bl_ext_lattice_join_comm(env: &mut Environment) -> Result<(), String> {
1108    let ty = forall_bool(
1109        "a",
1110        forall_bool(
1111            "b",
1112            eq_bool(
1113                bool_or(Expr::BVar(1), Expr::BVar(0)),
1114                bool_or(Expr::BVar(0), Expr::BVar(1)),
1115            ),
1116        ),
1117    );
1118    add_bool_theorem(env, "Bool.lattice_join_comm", ty)
1119}
1120/// Build the lattice meet-commutativity axiom (AND is commutative meet).
1121pub fn bl_ext_lattice_meet_comm(env: &mut Environment) -> Result<(), String> {
1122    let ty = forall_bool(
1123        "a",
1124        forall_bool(
1125            "b",
1126            eq_bool(
1127                bool_and(Expr::BVar(1), Expr::BVar(0)),
1128                bool_and(Expr::BVar(0), Expr::BVar(1)),
1129            ),
1130        ),
1131    );
1132    add_bool_theorem(env, "Bool.lattice_meet_comm", ty)
1133}
1134/// Build the Heyting algebra implication axiom.
1135/// In Bool, a => b = ¬a ∨ b (material implication)
1136pub fn bl_ext_heyting_implication(env: &mut Environment) -> Result<(), String> {
1137    let type1 = Expr::Sort(Level::succ(Level::zero()));
1138    env.add(Declaration::Axiom {
1139        name: Name::str("BoolImply"),
1140        univ_params: vec![],
1141        ty: Expr::Pi(
1142            BinderInfo::Default,
1143            Name::str("_"),
1144            Box::new(bool_ty()),
1145            Box::new(Expr::Pi(
1146                BinderInfo::Default,
1147                Name::str("_"),
1148                Box::new(bool_ty()),
1149                Box::new(bool_ty()),
1150            )),
1151        ),
1152    })
1153    .map_err(|e| e.to_string())?;
1154    let _ = type1;
1155    let ty = forall_bool(
1156        "a",
1157        forall_bool(
1158            "b",
1159            eq_bool(
1160                Expr::App(
1161                    Box::new(Expr::App(
1162                        Box::new(Expr::Const(Name::str("BoolImply"), vec![])),
1163                        Box::new(Expr::BVar(1)),
1164                    )),
1165                    Box::new(Expr::BVar(0)),
1166                ),
1167                bool_or(bool_not(Expr::BVar(1)), Expr::BVar(0)),
1168            ),
1169        ),
1170    );
1171    add_bool_theorem(env, "Bool.imply_def", ty)
1172}
1173/// Build the Heyting reflexivity law: a => a = true
1174pub fn bl_ext_heyting_refl(env: &mut Environment) -> Result<(), String> {
1175    let ty = forall_bool(
1176        "a",
1177        eq_bool(bool_or(bool_not(Expr::BVar(0)), Expr::BVar(0)), bool_true()),
1178    );
1179    add_bool_theorem(env, "Bool.imply_refl", ty)
1180}
1181/// Build the B2 two-element Boolean algebra axiom.
1182/// B2 = {false, true} is the unique Boolean algebra of size 2.
1183pub fn bl_ext_b2_algebra(env: &mut Environment) -> Result<(), String> {
1184    env.add(Declaration::Axiom {
1185        name: Name::str("B2Card"),
1186        univ_params: vec![],
1187        ty: Expr::Sort(Level::zero()),
1188    })
1189    .map_err(|e| e.to_string())
1190}
1191/// Build the Bool-Prop decidability bridge axiom.
1192/// decide : Decidable P -> Bool  (extract boolean from decidable prop)
1193pub fn bl_ext_decidable_to_bool(env: &mut Environment) -> Result<(), String> {
1194    let type1 = Expr::Sort(Level::succ(Level::zero()));
1195    env.add(Declaration::Axiom {
1196        name: Name::str("DecidableToBool"),
1197        univ_params: vec![],
1198        ty: Expr::Pi(
1199            BinderInfo::Default,
1200            Name::str("α"),
1201            Box::new(type1.clone()),
1202            Box::new(Expr::Pi(
1203                BinderInfo::Default,
1204                Name::str("_"),
1205                Box::new(Expr::App(
1206                    Box::new(Expr::Const(Name::str("DecidableEq"), vec![])),
1207                    Box::new(Expr::BVar(0)),
1208                )),
1209                Box::new(Expr::Pi(
1210                    BinderInfo::Default,
1211                    Name::str("_"),
1212                    Box::new(Expr::BVar(1)),
1213                    Box::new(bool_ty()),
1214                )),
1215            )),
1216        ),
1217    })
1218    .map_err(|e| e.to_string())
1219}
1220/// Build the Bool reflection axiom: beq_iff_eq.
1221/// a = b <-> beq a b = true
1222pub fn bl_ext_bool_reflection(env: &mut Environment) -> Result<(), String> {
1223    let ty = forall_bool(
1224        "a",
1225        forall_bool(
1226            "b",
1227            eq_bool(bool_beq(Expr::BVar(1), Expr::BVar(0)), bool_true()),
1228        ),
1229    );
1230    add_bool_theorem(env, "Bool.beq_iff_eq_aux", ty)
1231}
1232/// Build the BEq class instance for Bool.
1233/// instance : BEq Bool via Bool.beq
1234pub fn bl_ext_beq_bool_instance(env: &mut Environment) -> Result<(), String> {
1235    env.add(Declaration::Axiom {
1236        name: Name::str("BEqBoolInst"),
1237        univ_params: vec![],
1238        ty: Expr::App(
1239            Box::new(Expr::Const(Name::str("BEq"), vec![])),
1240            Box::new(bool_ty()),
1241        ),
1242    })
1243    .map_err(|e| e.to_string())
1244}
1245/// Build the Bool-valued predicate functor axiom.
1246/// A Bool predicate P: α -> Bool can be lifted to Prop via (P x = true).
1247pub fn bl_ext_bool_pred_prop(env: &mut Environment) -> Result<(), String> {
1248    let type1 = Expr::Sort(Level::succ(Level::zero()));
1249    env.add(Declaration::Axiom {
1250        name: Name::str("BoolPredToProp"),
1251        univ_params: vec![],
1252        ty: Expr::Pi(
1253            BinderInfo::Implicit,
1254            Name::str("α"),
1255            Box::new(type1.clone()),
1256            Box::new(Expr::Pi(
1257                BinderInfo::Default,
1258                Name::str("p"),
1259                Box::new(Expr::Pi(
1260                    BinderInfo::Default,
1261                    Name::str("_"),
1262                    Box::new(Expr::BVar(0)),
1263                    Box::new(bool_ty()),
1264                )),
1265                Box::new(Expr::Pi(
1266                    BinderInfo::Default,
1267                    Name::str("x"),
1268                    Box::new(Expr::BVar(1)),
1269                    Box::new(Expr::Sort(Level::zero())),
1270                )),
1271            )),
1272        ),
1273    })
1274    .map_err(|e| e.to_string())
1275}
1276/// Build the short-circuit AND law: false && f = false (f not evaluated).
1277pub fn bl_ext_short_circuit_and(env: &mut Environment) -> Result<(), String> {
1278    let ty = forall_bool(
1279        "b",
1280        eq_bool(bool_and(bool_false(), Expr::BVar(0)), bool_false()),
1281    );
1282    add_bool_theorem(env, "Bool.short_circuit_and", ty)
1283}
1284/// Build the short-circuit OR law: true || f = true (f not evaluated).
1285pub fn bl_ext_short_circuit_or(env: &mut Environment) -> Result<(), String> {
1286    let ty = forall_bool(
1287        "b",
1288        eq_bool(bool_or(bool_true(), Expr::BVar(0)), bool_true()),
1289    );
1290    add_bool_theorem(env, "Bool.short_circuit_or", ty)
1291}
1292/// Build the XOR false identity: a XOR false = a.
1293pub fn bl_ext_xor_false(env: &mut Environment) -> Result<(), String> {
1294    let ty = forall_bool(
1295        "a",
1296        eq_bool(bool_xor(Expr::BVar(0), bool_false()), Expr::BVar(0)),
1297    );
1298    add_bool_theorem(env, "Bool.xor_false", ty)
1299}
1300/// Build the XOR true law: a XOR true = ¬a.
1301pub fn bl_ext_xor_true(env: &mut Environment) -> Result<(), String> {
1302    let ty = forall_bool(
1303        "a",
1304        eq_bool(
1305            bool_xor(Expr::BVar(0), bool_true()),
1306            bool_not(Expr::BVar(0)),
1307        ),
1308    );
1309    add_bool_theorem(env, "Bool.xor_true", ty)
1310}
1311/// Build the NAND functional completeness axiom.
1312/// Every boolean function is expressible via NAND alone.
1313pub fn bl_ext_nand_complete(env: &mut Environment) -> Result<(), String> {
1314    env.add(Declaration::Axiom {
1315        name: Name::str("Bool.nand"),
1316        univ_params: vec![],
1317        ty: Expr::Pi(
1318            BinderInfo::Default,
1319            Name::str("_"),
1320            Box::new(bool_ty()),
1321            Box::new(Expr::Pi(
1322                BinderInfo::Default,
1323                Name::str("_"),
1324                Box::new(bool_ty()),
1325                Box::new(bool_ty()),
1326            )),
1327        ),
1328    })
1329    .map_err(|e| e.to_string())?;
1330    let ty = forall_bool(
1331        "a",
1332        forall_bool(
1333            "b",
1334            eq_bool(
1335                Expr::App(
1336                    Box::new(Expr::App(
1337                        Box::new(Expr::Const(Name::str("Bool.nand"), vec![])),
1338                        Box::new(Expr::BVar(1)),
1339                    )),
1340                    Box::new(Expr::BVar(0)),
1341                ),
1342                bool_not(bool_and(Expr::BVar(1), Expr::BVar(0))),
1343            ),
1344        ),
1345    );
1346    add_bool_theorem(env, "Bool.nand_def", ty)
1347}
1348/// Build the NOR functional completeness axiom.
1349/// Every boolean function is expressible via NOR alone.
1350pub fn bl_ext_nor_complete(env: &mut Environment) -> Result<(), String> {
1351    env.add(Declaration::Axiom {
1352        name: Name::str("Bool.nor"),
1353        univ_params: vec![],
1354        ty: Expr::Pi(
1355            BinderInfo::Default,
1356            Name::str("_"),
1357            Box::new(bool_ty()),
1358            Box::new(Expr::Pi(
1359                BinderInfo::Default,
1360                Name::str("_"),
1361                Box::new(bool_ty()),
1362                Box::new(bool_ty()),
1363            )),
1364        ),
1365    })
1366    .map_err(|e| e.to_string())?;
1367    let ty = forall_bool(
1368        "a",
1369        forall_bool(
1370            "b",
1371            eq_bool(
1372                Expr::App(
1373                    Box::new(Expr::App(
1374                        Box::new(Expr::Const(Name::str("Bool.nor"), vec![])),
1375                        Box::new(Expr::BVar(1)),
1376                    )),
1377                    Box::new(Expr::BVar(0)),
1378                ),
1379                bool_not(bool_or(Expr::BVar(1), Expr::BVar(0))),
1380            ),
1381        ),
1382    );
1383    add_bool_theorem(env, "Bool.nor_def", ty)
1384}
1385/// Build the AND monoid identity axiom.
1386/// (Bool, AND, true) is a monoid.
1387pub fn bl_ext_and_monoid_id(env: &mut Environment) -> Result<(), String> {
1388    let ty_l = forall_bool(
1389        "b",
1390        eq_bool(bool_and(bool_true(), Expr::BVar(0)), Expr::BVar(0)),
1391    );
1392    add_bool_theorem(env, "Bool.and_monoid_left_id", ty_l)?;
1393    let ty_r = forall_bool(
1394        "b",
1395        eq_bool(bool_and(Expr::BVar(0), bool_true()), Expr::BVar(0)),
1396    );
1397    add_bool_theorem(env, "Bool.and_monoid_right_id", ty_r)
1398}
1399/// Build the OR monoid identity axiom.
1400/// (Bool, OR, false) is a monoid.
1401pub fn bl_ext_or_monoid_id(env: &mut Environment) -> Result<(), String> {
1402    let ty_l = forall_bool(
1403        "b",
1404        eq_bool(bool_or(bool_false(), Expr::BVar(0)), Expr::BVar(0)),
1405    );
1406    add_bool_theorem(env, "Bool.or_monoid_left_id", ty_l)?;
1407    let ty_r = forall_bool(
1408        "b",
1409        eq_bool(bool_or(Expr::BVar(0), bool_false()), Expr::BVar(0)),
1410    );
1411    add_bool_theorem(env, "Bool.or_monoid_right_id", ty_r)
1412}
1413/// Build the boolean fold-all axiom.
1414/// all p xs = foldr (∧) true (map p xs)
1415pub fn bl_ext_bool_fold_all(env: &mut Environment) -> Result<(), String> {
1416    let type1 = Expr::Sort(Level::succ(Level::zero()));
1417    env.add(Declaration::Axiom {
1418        name: Name::str("BoolAll"),
1419        univ_params: vec![],
1420        ty: Expr::Pi(
1421            BinderInfo::Implicit,
1422            Name::str("α"),
1423            Box::new(type1.clone()),
1424            Box::new(Expr::Pi(
1425                BinderInfo::Default,
1426                Name::str("p"),
1427                Box::new(Expr::Pi(
1428                    BinderInfo::Default,
1429                    Name::str("_"),
1430                    Box::new(Expr::BVar(0)),
1431                    Box::new(bool_ty()),
1432                )),
1433                Box::new(Expr::Pi(
1434                    BinderInfo::Default,
1435                    Name::str("_xs"),
1436                    Box::new(type1.clone()),
1437                    Box::new(bool_ty()),
1438                )),
1439            )),
1440        ),
1441    })
1442    .map_err(|e| e.to_string())
1443}
1444/// Build the boolean fold-any axiom.
1445/// any p xs = foldr (∨) false (map p xs)
1446pub fn bl_ext_bool_fold_any(env: &mut Environment) -> Result<(), String> {
1447    let type1 = Expr::Sort(Level::succ(Level::zero()));
1448    env.add(Declaration::Axiom {
1449        name: Name::str("BoolAny"),
1450        univ_params: vec![],
1451        ty: Expr::Pi(
1452            BinderInfo::Implicit,
1453            Name::str("α"),
1454            Box::new(type1.clone()),
1455            Box::new(Expr::Pi(
1456                BinderInfo::Default,
1457                Name::str("p"),
1458                Box::new(Expr::Pi(
1459                    BinderInfo::Default,
1460                    Name::str("_"),
1461                    Box::new(Expr::BVar(0)),
1462                    Box::new(bool_ty()),
1463                )),
1464                Box::new(Expr::Pi(
1465                    BinderInfo::Default,
1466                    Name::str("_xs"),
1467                    Box::new(type1.clone()),
1468                    Box::new(bool_ty()),
1469                )),
1470            )),
1471        ),
1472    })
1473    .map_err(|e| e.to_string())
1474}
1475/// Build the if-then-else semantics axiom.
1476/// ite true a b = a, ite false a b = b
1477pub fn bl_ext_ite_semantics(env: &mut Environment) -> Result<(), String> {
1478    let type1 = Expr::Sort(Level::succ(Level::zero()));
1479    env.add(Declaration::Axiom {
1480        name: Name::str("BoolIte"),
1481        univ_params: vec![],
1482        ty: Expr::Pi(
1483            BinderInfo::Implicit,
1484            Name::str("α"),
1485            Box::new(type1.clone()),
1486            Box::new(Expr::Pi(
1487                BinderInfo::Default,
1488                Name::str("cond"),
1489                Box::new(bool_ty()),
1490                Box::new(Expr::Pi(
1491                    BinderInfo::Default,
1492                    Name::str("t"),
1493                    Box::new(Expr::BVar(1)),
1494                    Box::new(Expr::Pi(
1495                        BinderInfo::Default,
1496                        Name::str("f"),
1497                        Box::new(Expr::BVar(2)),
1498                        Box::new(Expr::BVar(3)),
1499                    )),
1500                )),
1501            )),
1502        ),
1503    })
1504    .map_err(|e| e.to_string())
1505}
1506/// Build the ITE true branch law: ite true a b = a
1507pub fn bl_ext_ite_true(env: &mut Environment) -> Result<(), String> {
1508    let type1 = Expr::Sort(Level::succ(Level::zero()));
1509    env.add(Declaration::Axiom {
1510        name: Name::str("BoolIte.true_branch"),
1511        univ_params: vec![],
1512        ty: Expr::Pi(
1513            BinderInfo::Implicit,
1514            Name::str("α"),
1515            Box::new(type1.clone()),
1516            Box::new(Expr::Sort(Level::zero())),
1517        ),
1518    })
1519    .map_err(|e| e.to_string())
1520}
1521/// Build the ITE false branch law: ite false a b = b
1522pub fn bl_ext_ite_false(env: &mut Environment) -> Result<(), String> {
1523    let type1 = Expr::Sort(Level::succ(Level::zero()));
1524    env.add(Declaration::Axiom {
1525        name: Name::str("BoolIte.false_branch"),
1526        univ_params: vec![],
1527        ty: Expr::Pi(
1528            BinderInfo::Implicit,
1529            Name::str("α"),
1530            Box::new(type1.clone()),
1531            Box::new(Expr::Sort(Level::zero())),
1532        ),
1533    })
1534    .map_err(|e| e.to_string())
1535}
1536/// Build Kleene three-value extension axiom.
1537/// Kleene3 = {false, unknown, true} extends Bool with undecidability.
1538pub fn bl_ext_kleene_three_value(env: &mut Environment) -> Result<(), String> {
1539    env.add(Declaration::Axiom {
1540        name: Name::str("Kleene3"),
1541        univ_params: vec![],
1542        ty: Expr::Sort(Level::succ(Level::zero())),
1543    })
1544    .map_err(|e| e.to_string())?;
1545    env.add(Declaration::Axiom {
1546        name: Name::str("Kleene3.unknown"),
1547        univ_params: vec![],
1548        ty: Expr::Const(Name::str("Kleene3"), vec![]),
1549    })
1550    .map_err(|e| e.to_string())?;
1551    env.add(Declaration::Axiom {
1552        name: Name::str("Kleene3.and"),
1553        univ_params: vec![],
1554        ty: Expr::Pi(
1555            BinderInfo::Default,
1556            Name::str("_"),
1557            Box::new(Expr::Const(Name::str("Kleene3"), vec![])),
1558            Box::new(Expr::Pi(
1559                BinderInfo::Default,
1560                Name::str("_"),
1561                Box::new(Expr::Const(Name::str("Kleene3"), vec![])),
1562                Box::new(Expr::Const(Name::str("Kleene3"), vec![])),
1563            )),
1564        ),
1565    })
1566    .map_err(|e| e.to_string())
1567}
1568/// Build De Morgan duality as a meta-theorem axiom.
1569/// The De Morgan laws establish duality between ∧ and ∨.
1570pub fn bl_ext_demorgan_duality(env: &mut Environment) -> Result<(), String> {
1571    env.add(Declaration::Axiom {
1572        name: Name::str("DeMorganDuality"),
1573        univ_params: vec![],
1574        ty: Expr::Sort(Level::zero()),
1575    })
1576    .map_err(|e| e.to_string())
1577}
1578/// Build the SAT decidability axiom.
1579/// Boolean satisfiability is decidable by exhaustive enumeration.
1580pub fn bl_ext_sat_decidable(env: &mut Environment) -> Result<(), String> {
1581    env.add(Declaration::Axiom {
1582        name: Name::str("SATDecidable"),
1583        univ_params: vec![],
1584        ty: Expr::Sort(Level::zero()),
1585    })
1586    .map_err(|e| e.to_string())
1587}
1588/// Build the tautology-check axiom.
1589/// A formula is a tautology iff it evaluates to true for all assignments.
1590pub fn bl_ext_tautology_check(env: &mut Environment) -> Result<(), String> {
1591    env.add(Declaration::Axiom {
1592        name: Name::str("TautologyCheck"),
1593        univ_params: vec![],
1594        ty: Expr::Sort(Level::zero()),
1595    })
1596    .map_err(|e| e.to_string())
1597}
1598/// Build the OR-distrib-AND law: a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c).
1599pub fn bl_ext_or_distrib_and(env: &mut Environment) -> Result<(), String> {
1600    let ty = forall_bool(
1601        "a",
1602        forall_bool(
1603            "b",
1604            forall_bool(
1605                "c",
1606                eq_bool(
1607                    bool_or(Expr::BVar(2), bool_and(Expr::BVar(1), Expr::BVar(0))),
1608                    bool_and(
1609                        bool_or(Expr::BVar(2), Expr::BVar(1)),
1610                        bool_or(Expr::BVar(2), Expr::BVar(0)),
1611                    ),
1612                ),
1613            ),
1614        ),
1615    );
1616    add_bool_theorem(env, "Bool.or_distrib_and", ty)
1617}
1618/// Build the NOT-and-OR duality axiom.
1619/// ¬a ∨ ¬b = ¬(a ∧ b)  (alternate De Morgan form)
1620pub fn bl_ext_not_or_demorgan(env: &mut Environment) -> Result<(), String> {
1621    let ty = forall_bool(
1622        "a",
1623        forall_bool(
1624            "b",
1625            eq_bool(
1626                bool_not(bool_and(Expr::BVar(1), Expr::BVar(0))),
1627                bool_or(bool_not(Expr::BVar(1)), bool_not(Expr::BVar(0))),
1628            ),
1629        ),
1630    );
1631    add_bool_theorem(env, "Bool.not_and_demorgan", ty)
1632}
1633/// Build the XOR-not-beq relationship: a XOR b = ¬(beq a b).
1634pub fn bl_ext_xor_not_beq(env: &mut Environment) -> Result<(), String> {
1635    let ty = forall_bool(
1636        "a",
1637        forall_bool(
1638            "b",
1639            eq_bool(
1640                bool_xor(Expr::BVar(1), Expr::BVar(0)),
1641                bool_not(bool_beq(Expr::BVar(1), Expr::BVar(0))),
1642            ),
1643        ),
1644    );
1645    add_bool_theorem(env, "Bool.xor_not_beq", ty)
1646}
1647/// Build the beq-true-iff law: beq a true = a.
1648pub fn bl_ext_beq_true(env: &mut Environment) -> Result<(), String> {
1649    let ty = forall_bool(
1650        "a",
1651        eq_bool(bool_beq(Expr::BVar(0), bool_true()), Expr::BVar(0)),
1652    );
1653    add_bool_theorem(env, "Bool.beq_true", ty)
1654}
1655/// Build the beq-false-iff law: beq a false = ¬a.
1656pub fn bl_ext_beq_false(env: &mut Environment) -> Result<(), String> {
1657    let ty = forall_bool(
1658        "a",
1659        eq_bool(
1660            bool_beq(Expr::BVar(0), bool_false()),
1661            bool_not(Expr::BVar(0)),
1662        ),
1663    );
1664    add_bool_theorem(env, "Bool.beq_false", ty)
1665}
1666/// Build the AND-false-annihilation axiom: a ∧ false = false.
1667pub fn bl_ext_and_false_annihilate(env: &mut Environment) -> Result<(), String> {
1668    let ty = forall_bool(
1669        "a",
1670        eq_bool(bool_and(Expr::BVar(0), bool_false()), bool_false()),
1671    );
1672    add_bool_theorem(env, "Bool.and_false_annihilate", ty)
1673}
1674/// Build the OR-true-annihilation axiom: a ∨ true = true.
1675pub fn bl_ext_or_true_annihilate(env: &mut Environment) -> Result<(), String> {
1676    let ty = forall_bool(
1677        "a",
1678        eq_bool(bool_or(Expr::BVar(0), bool_true()), bool_true()),
1679    );
1680    add_bool_theorem(env, "Bool.or_true_annihilate", ty)
1681}
1682/// Build the AND-self law: a ∧ a = a (idempotency alias).
1683pub fn bl_ext_and_self(env: &mut Environment) -> Result<(), String> {
1684    let ty = forall_bool(
1685        "a",
1686        eq_bool(bool_and(Expr::BVar(0), Expr::BVar(0)), Expr::BVar(0)),
1687    );
1688    add_bool_theorem(env, "Bool.and_self", ty)
1689}
1690/// Build the OR-self law: a ∨ a = a (idempotency alias).
1691pub fn bl_ext_or_self(env: &mut Environment) -> Result<(), String> {
1692    let ty = forall_bool(
1693        "a",
1694        eq_bool(bool_or(Expr::BVar(0), Expr::BVar(0)), Expr::BVar(0)),
1695    );
1696    add_bool_theorem(env, "Bool.or_self", ty)
1697}
1698/// Register all extended Bool axioms into the environment.
1699pub fn register_bool_extended_axioms(env: &mut Environment) {
1700    let builders: &[fn(&mut Environment) -> Result<(), String>] = &[
1701        bl_ext_demorgan_and,
1702        bl_ext_demorgan_or,
1703        bl_ext_and_complement,
1704        bl_ext_or_complement,
1705        bl_ext_and_idempotent,
1706        bl_ext_or_idempotent,
1707        bl_ext_and_absorption,
1708        bl_ext_or_absorption,
1709        bl_ext_xor_ring,
1710        bl_ext_xor_assoc,
1711        bl_ext_and_distrib_xor,
1712        bl_ext_lattice_join_comm,
1713        bl_ext_lattice_meet_comm,
1714        bl_ext_heyting_implication,
1715        bl_ext_heyting_refl,
1716        bl_ext_b2_algebra,
1717        bl_ext_decidable_to_bool,
1718        bl_ext_bool_reflection,
1719        bl_ext_beq_bool_instance,
1720        bl_ext_bool_pred_prop,
1721        bl_ext_short_circuit_and,
1722        bl_ext_short_circuit_or,
1723        bl_ext_xor_false,
1724        bl_ext_xor_true,
1725        bl_ext_nand_complete,
1726        bl_ext_nor_complete,
1727        bl_ext_and_monoid_id,
1728        bl_ext_or_monoid_id,
1729        bl_ext_bool_fold_all,
1730        bl_ext_bool_fold_any,
1731        bl_ext_ite_semantics,
1732        bl_ext_ite_true,
1733        bl_ext_ite_false,
1734        bl_ext_kleene_three_value,
1735        bl_ext_demorgan_duality,
1736        bl_ext_sat_decidable,
1737        bl_ext_tautology_check,
1738        bl_ext_or_distrib_and,
1739        bl_ext_not_or_demorgan,
1740        bl_ext_xor_not_beq,
1741        bl_ext_beq_true,
1742        bl_ext_beq_false,
1743        bl_ext_and_false_annihilate,
1744        bl_ext_or_true_annihilate,
1745        bl_ext_and_self,
1746        bl_ext_or_self,
1747    ];
1748    for builder in builders {
1749        let _ = builder(env);
1750    }
1751}
1752/// Evaluate boolean XOR as ring addition in GF(2).
1753#[allow(dead_code)]
1754pub fn gf2_add(a: bool, b: bool) -> bool {
1755    a ^ b
1756}
1757/// Evaluate boolean AND as ring multiplication in GF(2).
1758#[allow(dead_code)]
1759pub fn gf2_mul(a: bool, b: bool) -> bool {
1760    a && b
1761}
oxilean_std/bool/functions.rs

oxilean_std/bool/
functions.rs
