1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202
#![deny(missing_docs)]
#![deny(dead_code)]
#![feature(marker_trait_attr)]
#![feature(generic_associated_types)]
#![allow(incomplete_features)]
//! # Prop
//! Propositional logic with types in Rust.
//!
//! A library in Rust for theorem proving with [Intuitionistic Propositional Logic](https://en.wikipedia.org/wiki/Intuitionistic_logic).
//! Supports theorem proving in [Classical Propositional Logic](https://en.wikipedia.org/wiki/Propositional_calculus).
//!
//! - Used in research on [Path Semantics](https://github.com/advancedresearch/path_semantics)
//! - Brought to you by the [AdvancedResearch Community](https://advancedresearch.github.io/)
//! - [Join us on Discord!](https://discord.gg/JkrhJJRBR2)
//!
//! Abbreviations:
//!
//! - IPL: Intuitionistic/Constructive Propositional Logic
//! - PL: Classical Propositional Logic
//! - PSI: Path Semantical Intuitionistic/Constructive Propositional Logic
//! - PSL: Path Semantical Classical Propositional Logic
//!
//! ### Motivation
//!
//! [Path Semantics](https://github.com/advancedresearch/path_semantics)
//! extends dependent types with normal paths and is also used to extend
//! Classical Propositional Logic with multiple levels of propositions.
//! It is also used to explore higher dimensional mathematics.
//! A popular research subject in Path Semantics is [Avatar Extensions](https://advancedresearch.github.io/avatar-extensions/summary.html).
//!
//! When researching, in some cases it is useful to figure out whether a proof is
//! provable in classical logic, but not in constructive logic.
//! This requires comparing proofs easily.
//!
//! This library uses a lifting mechanism for making it easier
//! to produce proofs in classical logic and compare them to
//! proofs in constructive logic.
//!
//! ### Design
//!
//! This library contains:
//!
//! - `Prop`: Propositions that might or might not be decidable (constructive logic)
//! - `DProp`: Decidable propositions (classical logic)
//! - `LProp`: Like `Prop`, but with path semantics (path semantical constructive logic)
//! - `DLProp`: Like `DProp`, but with path semantics (path semantical classical logic)
//! - Automatic lifting of Excluded Middle to decidable propositions
//! - Double Negation for proofs of `Prop`
//! - A model of Path Semantical Quality in IPL
//! - Formalization of the core axiom of Path Semantics
//! - Tactics organized in modules by constructs (e.g. `and` or `imply`)
//!
//! Due to first-order logic requiring dependent types,
//! which is not yet supported in Rust,
//! this library is limited to zeroth-order logic (propositional logic).
//!
//! ### Examples
//!
//! ```rust
//! use prop::*;
//!
//! fn proof<A: Prop, B: Prop>(f: Imply<A, B>, a: A) -> B {
//! imply::modus_ponens(f, a)
//! }
//! ```
//!
//! Notice that there is no `DProp` used here,
//! which means that it is a constructive proof.
//!
//! ```rust
//! use prop::*;
//!
//! fn proof<A: DProp, B: DProp>(f: Imply<Not<A>, Not<B>>) -> Imply<B, A> {
//! imply::rev_modus_tollens(f)
//! }
//! ```
//!
//! Here, `DProp` is needed because `rev_modus_tollens` needs Excluded Middle.
//! This limits the proof to decidable propositions.
//!
//! ### Path Semantics
//!
//! Path Semantics is an extremely expressive language for mathematical programming.
//! It uses a single core axiom, which models semantics of symbols.
//!
//! Basically, mathematical languages contain a hidden symmetry due to use of symbols.
//! Counter-intuitively, symbols are not "inherently" in logic.
//!
//! One way to put it, is that the symbols "themselves" encode laws of mathematics.
//! The hidden symmetry can be exploited to prove semantics and sometimes
//! improve performance of automated theorem provers.
//!
//! For more information, see the [Path Semantics Project](https://github.com/advancedresearch/path_semantics).
use std::rc::Rc;
use Either::*;
pub mod and;
pub mod avatar_extensions;
pub mod imply;
pub mod eq;
pub mod not;
pub mod or;
pub mod path_semantics;
pub mod nat;
pub mod quality;
pub mod univalence;
/// Logical true.
#[derive(Copy, Clone)]
pub struct True;
/// Logical false.
#[derive(Copy, Clone)]
pub enum False {}
/// Sum type of left and right case.
#[derive(Copy, Clone)]
pub enum Either<T, U> {
/// Left case.
Left(T),
/// Right case.
Right(U),
}
/// Logical AND.
pub type And<T, U> = (T, U);
/// Double negation.
pub type Dneg<T> = Imply<Not<Not<T>>, T>;
/// Logical EQ.
pub type Eq<T, U> = And<Imply<T, U>, Imply<U, T>>;
/// Alternative to Logical EQ.
pub type Iff<T, U> = Eq<T, U>;
/// Logical IMPLY.
pub type Imply<T, U> = Rc<dyn Fn(T) -> U>;
/// Excluded middle.
pub type ExcM<T> = Or<T, Not<T>>;
/// Logical NOT.
pub type Not<T> = Imply<T, False>;
/// Logical OR.
pub type Or<T, U> = Either<T, U>;
/// A proposition that might be decidable or undecidable.
pub trait Prop: 'static + Sized + Clone {
/// Get double negation rule from proof.
fn double_neg(self) -> Dneg<Self> {self.map_any()}
/// Maps anything into itself.
fn map_any<T>(self) -> Imply<T, Self> {Rc::new(move |_| self.clone())}
}
impl<T: 'static + Sized + Clone> Prop for T {}
/// Implemented by decidable types.
pub trait Decidable: Prop {
/// Get excluded middle rule.
fn decide() -> ExcM<Self>;
}
impl Decidable for True {
fn decide() -> ExcM<True> {Left(True)}
}
impl Decidable for False {
fn decide() -> ExcM<False> {Right(Rc::new(move |x| x))}
}
impl<T, U> Decidable for And<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(Left(a), Left(b)) => Left((a, b)),
(_, Right(b)) => Right(Rc::new(move |(_, x)| b.clone()(x))),
(Right(a), _) => Right(Rc::new(move |(x, _)| a.clone()(x))),
}
}
}
impl<T, U> Decidable for Or<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(Left(a), _) => Left(Left(a)),
(_, Left(b)) => Left(Right(b)),
(Right(a), Right(b)) => Right(Rc::new(move |f| match f {
Left(x) => a.clone()(x),
Right(y) => b.clone()(y),
}))
}
}
}
impl<T, U> Decidable for Imply<T, U> where T: Decidable, U: Decidable {
fn decide() -> ExcM<Self> {
match (<T as Decidable>::decide(), <U as Decidable>::decide()) {
(_, Left(b)) => Left(b.map_any()),
(Left(a), Right(b)) =>
Right(Rc::new(move |f| b.clone()(f(a.clone())))),
(Right(a), _) => {
let g: Imply<Not<U>, Not<T>> = a.map_any();
Left(imply::rev_modus_tollens(g))
}
}
}
}
/// Shorthand for decidable proposition.
pub trait DProp: Decidable {}
impl<T: Decidable> DProp for T {}