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

//! Tactics for Logical OR.

use crate::*;

/// `a ∨ b => b ∨ a`.
pub fn commute<A: Prop, B: Prop>(or: Or<A, B>) -> Or<B, A> {
    use Either::*;

    match or {
        Left(x) => Right(x),
        Right(x) => Left(x)
    }
}

/// `(a ∨ b) ∨ c  =>  a ∨ (b ∨ c)`
pub fn assoc<A: Prop, B: Prop, C: Prop>(
    f: Or<Or<A, B>, C>
) -> Or<A, Or<B, C>> {
    use Either::*;

    match f {
        Left(x) => match x {
            Left(a) => Left(a),
            Right(b) => Right(Left(b)),
        }
        Right(c) => Right(Right(c))
    }
}

/// `(a ∧ b) ∨ (a ∧ c)  =>  a ∧ (b ∨ c)`
pub fn distrib<A: Prop, B: Prop, C: Prop>(
    x: Or<And<A, B>, And<A, C>>
) -> And<A, Or<B, C>> {
    use Either::*;

    match x {
        Left((a, b)) => (a, Left(b)),
        Right((a, c)) => (a, Right(c))
    }
}

/// `¬(a ∧ b) => (¬a ∨ ¬b)`.
pub fn from_de_morgan<A: DProp, B: DProp>(
    f: Not<And<A, B>>
) -> Or<Not<A>, Not<B>> {
    use Either::*;

    match (A::decide(), B::decide()) {
        (Left(a), Left(b)) => match f((a, b)) {},
        (_, Right(b)) => Right(Rc::new(move |x| b.clone()(x))),
        (Right(a), _) => Left(Rc::new(move |x| a.clone()(x))),
    }
}

/// `(¬a ∨ ¬b) => ¬(a ∧ b)`.
pub fn to_de_morgan<A: DProp, B: DProp>(
    f: Or<Not<A>, Not<B>>
) -> Not<And<A, B>> {
    use Either::*;

    match f {
        Left(fa) => match A::decide() {
            Left(a) => match fa(a) {},
            Right(not_a) => Rc::new(move |(x, _)| match not_a.clone()(x) {}),
        }
        Right(fb) => match B::decide() {
            Left(b) => match fb(b) {},
            Right(not_b) => Rc::new(move |(_, x)| match not_b.clone()(x) {}),
        }
    }
}