Revision #2410 → #3063 · back to history
modifiedBoolean algebra expression2f59177f24d8
| Field | From #2410 | To #3063 |
|---|
| note | Boolean algebras are formalized in Mathlib as the `BooleanAlgebra` typeclass, but the notion of a symbolic Boolean-algebra expression (as a syntactic object to be simplified) is not. | Boolean algebras themselves are formalized as `BooleanAlgebra` (verified via decl_exists), but the notion of a symbolic Boolean-algebra expression as a syntactic object to be simplified is not. |
modifiedCells and minterms18feeb022f9d
| Field | From #2410 | To #3063 |
|---|
| note | The notion of a minterm (a conjunction over all input variables) is not defined in Mathlib (grep for 'minterm' yields no matches). | Grep for 'minterm' in Mathlib returns no matches; the minterm notion is not formalized. |
modifiedCanonical form from truth-table groupingd5109aea55ca
| Field | From #2410 | To #3063 |
|---|
| note | Disjunctive/conjunctive normal forms (canonical sum-of-products / product-of-sums) of Boolean functions are not formalized in Mathlib. | Canonical DNF/CNF sum-of-products / product-of-sums normal forms for Boolean functions are not formalized in Mathlib. |
modifiedSum-of-products and product-of-sums implementation0ce17cf620cf
| Field | From #2410 | To #3063 |
|---|
| note | SOP/POS normal forms for Boolean expressions and their gate-level implementations are not formalized in Mathlib. | SOP/POS normal forms and their gate-level implementations are not formalized in Mathlib. |
addedTruth table representation5177593dd473
modifiedGray code ordering of indices5586c1f64bc8
| Field | From #2410 | To #3063 |
|---|
| note | Gray code is not defined in Mathlib (case-insensitive grep returns no matches). | Gray code is not defined in Mathlib (case-insensitive grep for 'gray code' returns no matches). |
addedGray code single-bit adjacencye046615d87fb
modifiedProduct of sums via De Morgan's laws596d9776a285
| Field | From #2410 | To #3063 |
|---|
| note | De Morgan's laws themselves are in Mathlib (`compl_inf : (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ` and its dual), but their application to convert a SOP K-map result into POS form is not formalized. | De Morgan's laws themselves are in Mathlib (`compl_inf : (x ⊓ y)ᶜ = xᶜ ⊔ yᶜ`, verified via decl_exists), but their application to convert a SOP K-map result into POS form is not formalized. |
addedDe Morgan's laws (POS from don't-care inverse)426e3fd4a40b