Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

add_bool_theorem

Add a theorem declaration with a sorry placeholder proof.

add_eq_if_missing

Add Eq to environment if not already present.

and_table

Standard boolean truth tables. Truth table for logical AND.

arrow

bl_ext_and_absorption

Build the AND-OR absorption law: a ∧ (a ∨ b) = a

bl_ext_and_complement

Build the AND complementation law: a ∧ ¬a = false

bl_ext_and_distrib_xor

Build the AND distributivity over XOR law: a ∧ (b XOR c) = (a ∧ b) XOR (a ∧ c).

bl_ext_and_false_annihilate

Build the AND-false-annihilation axiom: a ∧ false = false.

bl_ext_and_idempotent

Build the AND idempotency law: a ∧ a = a

bl_ext_and_monoid_id

Build the AND monoid identity axiom. (Bool, AND, true) is a monoid.

bl_ext_and_self

Build the AND-self law: a ∧ a = a (idempotency alias).

bl_ext_b2_algebra

Build the B2 two-element Boolean algebra axiom. B2 = {false, true} is the unique Boolean algebra of size 2.

bl_ext_beq_bool_instance

Build the BEq class instance for Bool. instance : BEq Bool via Bool.beq

bl_ext_beq_false

Build the beq-false-iff law: beq a false = ¬a.

bl_ext_beq_true

Build the beq-true-iff law: beq a true = a.

bl_ext_bool_fold_all

Build the boolean fold-all axiom. all p xs = foldr (∧) true (map p xs)

bl_ext_bool_fold_any

Build the boolean fold-any axiom. any p xs = foldr (∨) false (map p xs)

bl_ext_bool_pred_prop

Build the Bool-valued predicate functor axiom. A Bool predicate P: α -> Bool can be lifted to Prop via (P x = true).

bl_ext_bool_reflection

Build the Bool reflection axiom: beq_iff_eq. a = b <-> beq a b = true

bl_ext_decidable_to_bool

Build the Bool-Prop decidability bridge axiom. decide : Decidable P -> Bool (extract boolean from decidable prop)

bl_ext_demorgan_and

Build the De Morgan AND-NOT law: ¬(a ∧ b) = ¬a ∨ ¬b

bl_ext_demorgan_duality

Build De Morgan duality as a meta-theorem axiom. The De Morgan laws establish duality between ∧ and ∨.

bl_ext_demorgan_or

Build the De Morgan OR-NOT law: ¬(a ∨ b) = ¬a ∧ ¬b

bl_ext_heyting_implication

Build the Heyting algebra implication axiom. In Bool, a => b = ¬a ∨ b (material implication)

bl_ext_heyting_refl

Build the Heyting reflexivity law: a => a = true

bl_ext_ite_false

Build the ITE false branch law: ite false a b = b

bl_ext_ite_semantics

Build the if-then-else semantics axiom. ite true a b = a, ite false a b = b

bl_ext_ite_true

Build the ITE true branch law: ite true a b = a

bl_ext_kleene_three_value

Build Kleene three-value extension axiom. Kleene3 = {false, unknown, true} extends Bool with undecidability.

bl_ext_lattice_join_comm

Build the lattice join-commutativity axiom (OR is commutative join).

bl_ext_lattice_meet_comm

Build the lattice meet-commutativity axiom (AND is commutative meet).

bl_ext_nand_complete

Build the NAND functional completeness axiom. Every boolean function is expressible via NAND alone.

bl_ext_nor_complete

Build the NOR functional completeness axiom. Every boolean function is expressible via NOR alone.

bl_ext_not_or_demorgan

Build the NOT-and-OR duality axiom. ¬a ∨ ¬b = ¬(a ∧ b) (alternate De Morgan form)

bl_ext_or_absorption

Build the OR-AND absorption law: a ∨ (a ∧ b) = a

bl_ext_or_complement

Build the OR complementation law: a ∨ ¬a = true

bl_ext_or_distrib_and

Build the OR-distrib-AND law: a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c).

bl_ext_or_idempotent

Build the OR idempotency law: a ∨ a = a

bl_ext_or_monoid_id

Build the OR monoid identity axiom. (Bool, OR, false) is a monoid.

bl_ext_or_self

Build the OR-self law: a ∨ a = a (idempotency alias).

bl_ext_or_true_annihilate

Build the OR-true-annihilation axiom: a ∨ true = true.

bl_ext_sat_decidable

Build the SAT decidability axiom. Boolean satisfiability is decidable by exhaustive enumeration.

bl_ext_short_circuit_and

Build the short-circuit AND law: false && f = false (f not evaluated).

bl_ext_short_circuit_or

Build the short-circuit OR law: true || f = true (f not evaluated).

bl_ext_tautology_check

Build the tautology-check axiom. A formula is a tautology iff it evaluates to true for all assignments.

bl_ext_xor_assoc

Build the XOR associativity law.

bl_ext_xor_false

Build the XOR false identity: a XOR false = a.

bl_ext_xor_not_beq

Build the XOR-not-beq relationship: a XOR b = ¬(beq a b).

bl_ext_xor_ring

Build the Bool-as-ring XOR ring axiom: (Bool, XOR, AND) forms a field GF(2).

bl_ext_xor_true

Build the XOR true law: a XOR true = ¬a.

bool_and

Create Bool.and a b.

bool_beq

Create Bool.beq a b.

bool_false

Create a false expression.

bool_not

Create Bool.not b.

bool_or

Create Bool.or a b.

bool_rec

Create Bool.rec motive false_case true_case b.

bool_true

Create a true expression.

bool_ty

The Bool type expression.

bool_xor

Create Bool.xor a b.

build_bool_env

Build the Bool type and all associated declarations.

eq_bool

forall_bool

gf2_add

Evaluate boolean XOR as ring addition in GF(2).

gf2_mul

Evaluate boolean AND as ring multiplication in GF(2).

iff_table

Truth table for logical IFF (biconditional).

imply_table

Truth table for logical implication.

mk_bool_eq

Create Eq a b where both are Bool.

nand_table

Truth table for logical NAND.

nor_table

Truth table for logical NOR.

or_table

Truth table for logical OR.

register_bool_extended_axioms

Register all extended Bool axioms into the environment.

xor_table

Truth table for logical XOR.