type_proof/lib.rs
1#![doc(html_playground_url = "https://play.rust-lang.org/")]
2#![deny(
3 rustdoc::broken_intra_doc_links,
4 rustdoc::private_intra_doc_links,
5 rustdoc::missing_crate_level_docs,
6 rustdoc::invalid_codeblock_attributes,
7 rustdoc::invalid_html_tags,
8 rustdoc::invalid_rust_codeblocks,
9 rustdoc::bare_urls,
10 rustdoc::unescaped_backticks,
11 missing_docs
12)]
13
14//! A Rust crate for type-checked [propositional logic](https://en.wikipedia.org/wiki/Propositional_logic) proofs.
15//!
16//! ## Key features
17//!
18//! - Construction of Boolean values with True and False each being its own type
19//! - Includes type-level Boolean operations
20//! - Construction of the natural numbers with each number being its own type
21//! - Includes type-level arithmetic operations
22//! - Construction of propositional formulas with each formula being its own type
23//! - Construction of a proof system where a proof is valid if and only if it type checks
24//! - Valuation of formulas at the type level
25//!
26//! ## More detail
27//!
28//! Instead of defining Booleans / numbers / formulas / proofs as instances of a type (e.g. a natural number as a
29//! [`usize`]), we define each Boolean / number / formula / proof as its own type: e.g. 0 is the type [`N0`], 1 is
30//! the type [`N1`], etc. These types never need to be instantiated - we work solely with the definitions of the
31//! types.
32//!
33//! For example, the formula `(p0 -> ¬p2)` is constructed as the following type:
34//!
35//! ```rust
36//! use type_proof::formula::{Implies, Not, P0, P2};
37//!
38//! type P = Implies<P0, Not<P2>>;
39//! ```
40//!
41//! Likewise, proofs can be defined as types. The type of a **valid** proof will automatically implement the
42//! [`Proof`] trait. This trait contains an associated type, which will be that of the formula it proves. Therefore,
43//! the validity of a proof can be checked by the type checker, by determining whether the [`Proof`] trait is
44//! implemented.
45//!
46//! Here's an example of a proof of `(P -> P)`, where `P` is an arbitrary formula:
47//!
48//! ```rust
49//! use type_proof::{
50//! formula::{Formula, Implies, P0},
51//! proof::{Axiom1, Axiom2, MP, assert_proves},
52//! };
53//!
54//! type ToProve<P> = Implies<P, P>;
55//!
56//! type Step1<P> = Axiom1<P, Implies<P0, P>>;
57//! type Step2<P> = Axiom2<P, Implies<P0, P>, P>;
58//! type Step3<P> = MP<Step1<P>, Step2<P>>;
59//! type Step4<P> = Axiom1<P, P0>;
60//! type Step5<P> = MP<Step4<P>, Step3<P>>;
61//!
62//! fn for_all<P: Formula>() {
63//! // This type checks, so it's a valid proof
64//! assert_proves::<Step5<P>, ToProve<P>>();
65//! }
66//! ```
67//!
68//! For more details on the construction of the types and on the details of the logical language / proof system, see
69//! the individual modules' documentation.
70//!
71//! As well as writing proofs, we can also evaluate formulas for different values of the propositional variables,
72//! evaluated at the type level to either the [`True`] type or the [`False`] type:
73//!
74//! ```rust
75//! use type_proof::{
76//! boolean::{False, True},
77//! formula::{And, Not, P0, P2, Valuation},
78//! type_utils::assert_type_eq,
79//! };
80//!
81//! type P = And<P0, Not<P2>>;
82//!
83//! struct V;
84//! impl Valuation<P0> for V {
85//! type Value = True;
86//! }
87//! impl Valuation<P2> for V {
88//! type Value = False;
89//! }
90//!
91//! type ValueOfP = <V as Valuation<P>>::Value;
92//! assert_type_eq::<ValueOfP, True>();
93//! ```
94//!
95//! [`False`]: crate::boolean::False
96//! [`N0`]: crate::peano::N0
97//! [`N1`]: crate::peano::N1
98//! [`Proof`]: crate::proof::Proof
99//! [`True`]: crate::boolean::True
100
101extern crate self as type_proof; // so that the path to this crate works in macros when used in this crate
102
103pub mod boolean;
104pub mod formula;
105pub mod peano;
106pub mod proof;
107pub mod type_utils;
108
109#[allow(unused)]
110#[cfg(doctest)]
111#[doc = include_str!("../../README.md")]
112struct ReadmeDoctests;