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
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

use super::*;

/// Proof of path semantical order.
#[derive(Copy)]
pub struct POrdProof<T, U>(std::marker::PhantomData<(T, U)>);

impl<T: POrd<U>, U> Default for POrdProof<T, U> {
    fn default() -> Self {
        POrdProof(std::marker::PhantomData)
    }
}

impl<T, U> Clone for POrdProof<T, U> {
    fn clone(&self) -> POrdProof<T, U> {
        POrdProof(std::marker::PhantomData)
    }
}

impl<T: 'static, U: 'static> Decidable for POrdProof<T, U> {
    fn decide() -> ExcM<POrdProof<T, U>> {
        Left(POrdProof(std::marker::PhantomData))
    }
}

impl<T, U> POrdProof<T, U> {
    /// Creates a new proof from trait constraints.
    pub fn new() -> Self where T: POrd<U> {
        Self::default()
    }

    /// Transivity of path semantical order.
    pub fn transitivity<V>(self, _: POrdProof<U, V>) -> POrdProof<T, V> {
        POrdProof(std::marker::PhantomData)
    }

    /// Transform left argument by equivalence.
    pub fn by_eq_left<V>(self, _: Eq<T, V>) -> POrdProof<V, U> {
        POrdProof(std::marker::PhantomData)
    }

    /// Transform right argument by equivalence.
    ///
    /// # Safety
    ///
    /// This theorem is unsafe due to use of [POrdProof::by_imply_right].
    pub unsafe fn by_eq_right<V>(self, eq: Eq<U, V>) -> POrdProof<T, V> {
        self.by_imply_right(eq.0)
    }

    /// Transform right argument by implication.
    ///
    /// # Safety
    ///
    /// There are some situations where a type might be coerced into another type,
    /// e.g. `f : a -> b` (function pointer) gets coerced into `f : a => b` (lambda).
    ///
    /// These transformations might depend on the specific model being used.
    /// What constitutes safety in one model might differ from safety in another model.
    ///
    /// Unsafe code is used to reduce the strength of assumptions in axioms for safe invariants.
    ///
    /// All such transformations are considered unsafe by default,
    /// but makes it also possible for derived models to create safe invariants.
    pub unsafe fn by_imply_right<V>(self, _: Imply<U, V>) -> POrdProof<T, V> {
        POrdProof(std::marker::PhantomData)
    }

    /// Merges two proofs of order at right side.
    pub fn merge_right<V>(self, _: POrdProof<T, V>) -> POrdProof<T, And<U, V>> {
        POrdProof(std::marker::PhantomData)
    }

    /// Merges two proofs of order at left side.
    pub fn merge_left<V>(self, _: POrdProof<V, U>) -> POrdProof<And<T, V>, U> {
        POrdProof(std::marker::PhantomData)
    }

    /// Combine two proofs into one using AND.
    pub fn and<T2, U2>(self, _: POrdProof<T2, U2>) -> POrdProof<And<T, T2>, And<U, U2>> {
        POrdProof(std::marker::PhantomData)
    }

    /// Combine two proofs into one using OR.
    pub fn or<T2, U2>(self, _: POrdProof<T2, U2>) -> POrdProof<Or<T, T2>, Or<U, U2>> {
        POrdProof(std::marker::PhantomData)
    }

    /// Combine two proofs into one using IMPLY.
    pub fn imply<T2, U2>(self, _: POrdProof<T2, U2>) -> POrdProof<Imply<T, T2>, Imply<U, U2>> {
        POrdProof(std::marker::PhantomData)
    }

    /// Combine two proofs into one using EQ.
    pub fn eq<T2, U2>(self, x: POrdProof<T2, U2>) -> POrdProof<Eq<T, T2>, Eq<U, U2>> {
        self.clone().imply(x.clone()).and(x.imply(self))
    }

    /// Lift to qubit.
    pub fn qu(self) -> POrdProof<Qu<T>, Qu<U>> {
        POrdProof(std::marker::PhantomData)
    }

    /// Combine two proofs into one using path semantical quality.
    pub fn q<T2, U2>(self, x: POrdProof<T2, U2>) -> POrdProof<Q<T, T2>, Q<U, U2>> {
        self.clone().eq(x.clone()).and(self.qu().and(x.qu()))
    }
}

impl<A, B, C> POrdProof<A, Or<B, C>> {
    /// Get sub order proof `a < b`.
    pub fn or_left(self) -> POrdProof<A, B> {
        POrdProof(std::marker::PhantomData)
    }

    /// Get sub order proof `a < c`.
    pub fn or_right(self) -> POrdProof<A, C> {
        POrdProof(std::marker::PhantomData)
    }
}

impl<A, B> POrdProof<A, Imply<A, B>> {
    /// Get reduced proof `a < b`.
    pub fn imply_reduce(self) -> POrdProof<A, B> {
        POrdProof(std::marker::PhantomData)
    }
}

/// Path semantical order.
///
/// This is implemented by types to define an order
/// such that symbols can not be used inconsistently.
///
/// Uses a marker feature to allow overlapping impls.
#[marker]
pub trait POrd<T> {}

impl<A, B, T> POrd<T> for And<A, B>
    where A: POrd<T>, B: POrd<T> {}
impl<A, B, T> POrd<T> for Or<A, B>
    where A: POrd<T>, B: POrd<T> {}
impl<A, B, T> POrd<T> for Imply<A, B>
    where A: POrd<T>, B: POrd<T> {}
impl<A, B> POrd<Qu<B>> for Qu<A>
    where A: POrd<B> {}

impl<T, U> POrd<U> for T where T: LProp, U: LProp, T::N: Lt<U::N> {}