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

//! # Path Semantical Qubit
//!
//! For an implementation, see the [Pocket-Prover](https://github.com/advancedresearch/pocket_prover) library.

use crate::*;
use hooo::Tauto;
use nat::{Nat, Z, S};
use quality::{Aq, Q};

/// Represents a recursive qubit proposition.
#[derive(Copy, Clone)]
pub struct Qubit<N, A>(N, A);

/// The qubit proposition `~a`.
pub type Qu<A> = Qubit<S<Z>, A>;

impl<A: DProp> Decidable for Qu<A> {fn decide() -> ExcM<Qu<A>> {decide()}}

impl<A: Prop> Qubit<Z, A> {
    /// Get proposition.
    pub fn to(self) -> A {self.1}
    /// From proposition.
    pub fn from(a: A) -> Self {Qubit(Z, a)}
}

impl<A: Prop> Qubit<S<Z>, A> {
    /// Convert to self-quality.
    pub fn to_q(self) -> Q<A, A> {(eq::refl(), (self.clone(), self))}
    /// Convert from self-quality.
    pub fn from_q((_, (x, _)): Q<A, A>) -> Self {x}
}

impl<A: Prop> Qubit<S<Z>, Not<A>> {
    /// Convert to self-quality.
    pub fn to_aq(self) -> Aq<A, A> {(eq::refl(), (self.clone(), self))}
    /// Convert from self-quality.
    pub fn from_aq((_, (x, _)): Aq<A, A>) -> Self {x}
}

/// `~a ⋁ ¬~a`.
pub fn decide<A: DProp>() -> ExcM<Qu<A>> {decide_tauto_excm(tauto!(A::decide()))}

/// `(a ⋁ ¬a)^true  =>  (~a ⋁ ¬~a)`.
pub fn decide_tauto_excm<A: Prop>(_: Tauto<ExcM<A>>) -> ExcM<Qu<A>> {unimplemented!()}

/// `~qubit^n(a)  =>  qubit^(n+1)(a)`.
pub fn normalize<A: Prop, N: Nat>(x: Qubit<S<Z>, Qubit<N, A>>) -> Qubit<S<N>, A> {
    Qubit(S(x.1.0), x.1.1)
}
/// `qubit^(n+1)(a)  =>  ~qubit^n(a)`.
pub fn rev_normalize<A: Prop, N: Nat>(x: Qubit<S<N>, A>) -> Qubit<S<Z>, Qubit<N, A>> {
    Qubit(S(Z), Qubit(x.0.0, x.1))
}

/// `¬~a => ~¬a`.
pub fn sesh_to_inv<A: Prop>(_: Not<Qu<A>>) -> Qu<Not<A>> {unimplemented!()}
/// `~¬a => ¬~a`.
pub fn inv_to_sesh<A: Prop>(_: Qu<Not<A>>) -> Not<Qu<A>> {unimplemented!()}
/// `¬~a == ~¬a`.
pub fn eq_sesh_inv<A: Prop>() -> Eq<Not<Qu<A>>, Qu<Not<A>>> {
    (Rc::new(sesh_to_inv), Rc::new(inv_to_sesh))
}

/// Convert to equality.
pub fn to_eq<A: Prop, B: Prop>(x: Eq<Qubit<Z, A>, Qubit<Z, B>>) -> Eq<A, B> {
    let x2 = x.clone();
    (
        Rc::new(move |a| x2.0(Qubit::from(a)).to()),
        Rc::new(move |b| x.1(Qubit::from(b)).to()),
    )
}

/// Convert from equality.
pub fn from_eq<A: Prop, B: Prop>(x: Eq<A, B>) -> Eq<Qubit<Z, A>, Qubit<Z, B>> {
    let x2 = x.clone();
    (
        Rc::new(move |a| Qubit::from(x2.0(a.to()))),
        Rc::new(move |b| Qubit::from(x.1(b.to())))
    )
}

/// Convert to equality.
pub fn to_eq_q<A: Prop, B: Prop>(x: Eq<Qubit<S<Z>, A>, Qubit<S<Z>, B>>) -> Eq<Q<A, A>, Q<B, B>> {
    let x2 = x.clone();
    (
        Rc::new(move |qa| x2.0(Qubit::from_q(qa)).to_q()),
        Rc::new(move |qb| x.1(Qubit::from_q(qb)).to_q())
    )
}

/// Convert from equality.
pub fn from_eq_q<A: Prop, B: Prop>(x: Eq<Q<A, A>, Q<B, B>>) -> Eq<Qubit<S<Z>, A>, Qubit<S<Z>, B>> {
    let x2 = x.clone();
    (
        Rc::new(move |qa| Qubit::from_q(x2.0(qa.to_q()))),
        Rc::new(move |qb| Qubit::from_q(x.1(qb.to_q())))
    )
}

/// `(~a == ~b) => (~¬a == ~¬b)`.`
pub fn eq_to_eq_inv<A: Prop, B: Prop>(eq_q: Eq<Qu<A>, Qu<B>>) -> Eq<Qu<Not<A>>, Qu<Not<B>>> {
    let eq_q = eq::symmetry(eq::modus_tollens(eq_q));
    let eq_q = eq::in_left_arg(eq_q, (
        Rc::new(move |x| qubit::sesh_to_inv(x)),
        Rc::new(move |x| qubit::inv_to_sesh(x))
    ));
    let eq_q = eq::in_right_arg(eq_q, (
        Rc::new(move |x| qubit::sesh_to_inv(x)),
        Rc::new(move |x| qubit::inv_to_sesh(x))
    ));
    eq_q
}

/// `~a ∧ (a == b)^true  =>  ~b`.
///
/// This requires `(a == b)^true` to make reasoning about randomness properly.
pub fn in_arg<A: Prop, B: Prop, N>(x: Qubit<N, A>, y: Tauto<Eq<A, B>>) -> Qubit<N, B> {
    Qubit(x.0, y(True).0(x.1))
}

/// `~a  ==  (a ~~ a)`.
pub fn eq_qu_q<A: Prop>() -> Eq<Qu<A>, Q<A, A>> {(Rc::new(Qu::to_q), Rc::new(Qu::from_q))}

/// `(a ~~ a)  == ~a`.
pub fn eq_q_qu<A: Prop>() -> Eq<Q<A, A>, Qu<A>> {eq::symmetry(eq_qu_q())}