prop/
or.rs

1//! Tactics for Logical OR.
2
3#![allow(unreachable_code)]
4
5use crate::*;
6
7/// `a ∨ b => b ∨ a`.
8pub fn symmetry<A: Prop, B: Prop>(or: Or<A, B>) -> Or<B, A> {
9    use Either::*;
10
11    match or {
12        Left(x) => Right(x),
13        Right(x) => Left(x)
14    }
15}
16
17/// `(a ∨ b) ∨ c  =>  a ∨ (b ∨ c)`
18pub fn assoc<A: Prop, B: Prop, C: Prop>(
19    f: Or<Or<A, B>, C>
20) -> Or<A, Or<B, C>> {
21    use Either::*;
22
23    match f {
24        Left(x) => match x {
25            Left(a) => Left(a),
26            Right(b) => Right(Left(b)),
27        }
28        Right(c) => Right(Right(c))
29    }
30}
31
32/// `(a ∧ b) ∨ (a ∧ c)  =>  a ∧ (b ∨ c)`
33pub fn distrib<A: Prop, B: Prop, C: Prop>(
34    x: Or<And<A, B>, And<A, C>>
35) -> And<A, Or<B, C>> {
36    use Either::*;
37
38    match x {
39        Left((a, b)) => (a, Left(b)),
40        Right((a, c)) => (a, Right(c))
41    }
42}
43
44/// `¬(a ∧ b) => (¬a ∨ ¬b)`.
45pub fn from_de_morgan<A: DProp, B: DProp>(
46    f: Not<And<A, B>>
47) -> Or<Not<A>, Not<B>> {
48    use Either::*;
49
50    match (A::decide(), B::decide()) {
51        (Left(a), Left(b)) => match f((a, b)) {},
52        (_, Right(b)) => Right(Rc::new(move |x| b.clone()(x))),
53        (Right(a), _) => Left(Rc::new(move |x| a.clone()(x))),
54    }
55}
56
57/// `(¬a ∨ ¬b) => ¬(a ∧ b)`.
58pub fn to_de_morgan<A: Prop, B: Prop>(f: Or<Not<A>, Not<B>>) -> Not<And<A, B>> {
59    Rc::new(move |(a, b)| match f.clone() {
60        Left(fa) => fa(a),
61        Right(fb) => fb(b)
62    })
63}
64
65/// `(a ∨ b) ∧ (a => c)  =>  (c ∨ b)`.
66pub fn in_left_arg<A: Prop, B: Prop, C: Prop>(
67    or_x_y: Or<A, B>, g: Imply<A, C>
68) -> Or<C, B> {
69    match or_x_y {
70        Left(x) => Left(g(x)),
71        Right(y) => Right(y),
72    }
73}
74
75/// `(a ∨ b) ∧ (b => c)  =>  (a ∨ c)`.
76pub fn in_right_arg<A: Prop, B: Prop, C: Prop>(
77    or_x_y: Or<A, B>, g: Imply<B, C>
78) -> Or<A, C> {
79    match or_x_y {
80        Left(x) => Left(x),
81        Right(y) => Right(g(y)),
82    }
83}
84
85/// `(¬a ∧ b) ∨ a  =>  (b ∨ a)`.
86pub fn bound_neg<A: Prop, B: Prop>(f: Or<And<Not<A>, B>, A>) -> Or<B, A> {
87    match f {
88        Left((_, b)) => Left(b),
89        Right(a) => Right(a)
90    }
91}
92
93/// `(a ∧ b) ∨ ¬a  =>  (b ∨ ¬a)`.
94pub fn bound_pos<A: Prop, B: Prop>(f: Or<And<A, B>, Not<A>>) -> Or<B, Not<A>> {
95    match f {
96        Left((_, b)) => Left(b),
97        Right(not_a) => Right(not_a)
98    }
99}
100
101/// `¬¬a == (a ∨ ¬¬a)`.
102pub fn eq_nn<A: Prop, B: Prop>() -> Eq<Not<Not<A>>, Or<A, Not<Not<A>>>> {
103    (
104        Rc::new(move |x| Right(x)),
105        Rc::new(|x| match x {
106            Left(a) => not::double(a),
107            Right(nna) => nna,
108        }),
109    )
110}
111
112/// `a ∨ a  =>  a`.
113pub fn both<A: Prop>(x: Or<A, A>) -> A {
114    match x {
115        Left(a) => a,
116        Right(a) => a,
117    }
118}
prop/or.rs

prop/
or.rs
