prop 0.47.0

Propositional logic with types in Rust
Documentation 
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

//! # Quantifiers
//!
//! This module contains traits for emulating predicates with
//! for-all (`All`) and there-exists (`Any`) quantifiers.
//!
//! 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).
//! However, this library has limited support for first-order logic.

use crate::*;

/// Apply a single argument to predicate.
pub type App<P, A> = <P as Pred>::Out<A>;
/// Apply two arguments to predicate.
pub type App2<P, A, B> = <P as Pred>::Out<And<A, B>>;

/// Implemented by predicates.
pub trait Pred: 'static + Clone {
    /// The output proposition.
    type Out<A: Prop>: Prop;
}

/// Implemented for predicates with a reflexivity property.
pub trait Reflexivity: Pred {
    /// `∀ a { p(a, a) }`.
    fn refl<A: Prop>(&self) -> Self::Out<And<A, A>>;
}

/// Implemented for predicates with an irreflexivity property.
pub trait Irreflexivity: Pred {
    /// `∀ a { ¬p(a, a) }`.
    fn irrefl<A: Prop>(&self) -> Not<Self::Out<And<A, A>>>;
}

/// Implemented for predicates with a symmetry property.
pub trait Symmetry: Pred {
    /// `∀ a, b { p(a, b) => p(b, a) }`.
    fn symmetry<A: Prop, B: Prop>(&self) -> Imply<App2<Self, A, B>, App2<Self, B, A>>;
}

/// Implemented for predicates with an antisymmetry property.
pub trait Antisymmetry: Pred {
    /// `∀ a, b { p(a, b) ⋀ p(b, a) => (a == b) }`.
    fn antisymmetry<A: Prop, B: Prop>(&self) ->
        Imply<And<App2<Self, A, B>, App2<Self, B, A>>, Eq<A, B>>;
}

/// Implemented for predicates with an asymmetry property.
pub trait Asymmetry: Pred {
    /// `∀ a, b { p(a, b) => ¬p(b, a) }`.
    fn asymmetry<A: Prop, B: Prop>(&self) -> Imply<App2<Self, A, B>, Not<App2<Self, B, A>>>;
}

/// Implemented for predicates with a transitivity property.
pub trait Transitivity: Pred {
    /// `∀ a, b, c { p(a, b) ⋀ p(b, c) => p(a, c) }`.
    fn transitivity<A: Prop, B: Prop, C: Prop>(&self) ->
        Imply<And<App2<Self, A, B>, App2<Self, B, C>>, App2<Self, A, C>>;
}

/// Implemented for predicates with a connectivity property.
pub trait Connectivity: Pred {
    /// `∀ a, b { (a ¬= b) => p(a, b) ⋁ p(b, a) }`.
    fn connectivity<A: Prop, B: Prop>(&self) ->
        Imply<Not<Eq<A, B>>, Or<App2<Self, A, B>, App2<Self, B, A>>>;
}

/// Implemented for predicates with a strong connectivity property.
pub trait StrongConnectivity: Pred {
    /// `∀ a, b { p(a, b) ⋁ p(b, a) }`.
    fn strong_connectivity<A: Prop, B: Prop>(&self) -> Or<App2<Self, A, B>, App2<Self, B, A>>;
}

/// Represents a for-all quantifier.
pub trait All<P: Pred>: Prop {
    /// Apply to some argument.
    fn all<A: Prop>(&self) -> App<P, A>;
}

/// Compose two predicates with implication.
#[derive(Clone)]
pub struct PImply<B: Pred, C: Pred>(std::marker::PhantomData<(B, C)>);

impl<B: Pred, C: Pred> Pred for PImply<B, C> {
    type Out<A: Prop> = Imply<App<B, A>, App<C, A>>;
}

impl<P: Pred> All<PImply<P, P>> for () {
    fn all<A: Prop>(&self) -> Imply<App<P, A>, App<P, A>> {
        Rc::new(move |pa| pa)
    }
}

/// Represents a there-exists quantifier.
pub trait Any<B: Pred>: Prop {
    /// `∃ x : A { B(x) } <=> ∀ C : P { ∀ x : A { B(x) => C(x) } => C }`.
    ///
    /// Uses the definition of the existential quantifier
    /// from [Calculus of Constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions).
    fn any<C: Pred>(&self, f: impl All<PImply<B, C>>) -> C;
}

/// Wraps a proposition as a predicate.
///
/// This is used with `Any` to define a finite set of propositions.
#[derive(Clone)]
pub struct Singleton<X: Prop>(pub X);

impl<X: Prop> Pred for Singleton<X> {
    type Out<A: Prop> = X;
}