#![allow(unreachable_code)]
use crate::*;
pub fn symmetry<A: Prop, B: Prop>((f0, f1): And<A, B>) -> And<B, A> {
(f1, f0)
}
pub fn assoc<A: Prop, B: Prop, C: Prop>(
((x0, x1), x2): And<And<A, B>, C>
) -> And<A, And<B, C>> {
(x0, (x1, x2))
}
pub fn rev_assoc<A: Prop, B: Prop, C: Prop>(
(x0, (x1, x2)): And<A, And<B, C>>
) -> And<And<A, B>, C> {
((x0, x1), x2)
}
pub fn distrib<A: Prop, B: Prop, C: Prop>(
(a, x): And<A, Or<B, C>>
) -> Or<And<A, B>, And<A, C>> {
match x {
Left(b) => Left((a, b)),
Right(c) => Right((a, c)),
}
}
pub fn rev_distrib<A: Prop, B: Prop, C: Prop>(
x: Or<And<A, B>, And<A, C>>
) -> And<A, Or<B, C>> {
match x {
Left((a, b)) => (a, Left(b)),
Right((a, c)) => (a, Right(c)),
}
}
pub fn exc_left<A: Prop, B: Prop>((not_a, x): And<Not<A>, Or<A, B>>) -> B {
match x {
Left(a) => match not_a(a) {},
Right(b) => b
}
}
pub fn exc_right<A: Prop, B: Prop>(
(not_b, x): And<Not<B>, Or<A, B>>
) -> A {
match x {
Left(a) => a,
Right(b) => match not_b(b) {},
}
}
pub fn exc_both<A: Prop, B: Prop>(
((not_a, not_b), x): And<And<Not<A>, Not<B>>, Or<A, B>>
) -> False {
match x {
Left(a) => match not_a(a) {},
Right(b) => match not_b(b) {},
}
}
pub fn from_de_morgan<A: Prop, B: Prop>(f: Not<Or<A, B>>) -> And<Not<A>, Not<B>> {
let f2 = f.clone();
(
Rc::new(move |a| f(Left(a))),
Rc::new(move |b| f2(Right(b))),
)
}
pub fn to_de_morgan<A: Prop, B: Prop>((f0, f1): And<Not<A>, Not<B>>) -> Not<Or<A, B>> {
Rc::new(move |or_ab| match or_ab {
Left(a) => match f0(a) {},
Right(b) => match f1(b) {},
})
}
pub fn false_arg<A: Prop>((x, _): And<False, A>) -> False {x}
pub fn true_arg<A: Prop>((_, x): And<True, A>) -> A {x}
pub fn in_left_arg<A: Prop, B: Prop, C: Prop>(
(x, y): And<A, B>, g: Imply<A, C>
) -> And<C, B> {
(g(x), y)
}
pub fn in_right_arg<A: Prop, B: Prop, C: Prop>(
(x, y): And<A, B>, g: Imply<B, C>
) -> And<A, C> {
(x, g(y))
}
pub fn in_left<A: Prop, B: Prop, C: Prop, F>(
(x, y): And<A, B>, f: F
) -> And<C, B> where F: Fn(A) -> C {
(f(x), y)
}
pub fn in_right<A: Prop, B: Prop, C: Prop, F>(
(x, y): And<A, B>, f: F
) -> And<A, C> where F: Fn(B) -> C {
(x, f(y))
}
pub fn eq_left<A: Prop, B: Prop, C: Prop>((ab, ba): Eq<A, B>) -> Eq<And<A, C>, And<B, C>> {
(Rc::new(move |(a, c)| (ab(a), c)), Rc::new(move |(b, c)| (ba(b), c)))
}
pub fn eq_right<A: Prop, B: Prop, C: Prop>((ab, ba): Eq<A, B>) -> Eq<And<C, A>, And<C, B>> {
(Rc::new(move |(c, a)| (c, ab(a))), Rc::new(move |(c, b)| (c, ba(b))))
}
pub fn eq_left_false<A: Prop, B: Prop, C: Prop>(nc: Not<C>) -> Eq<And<A, C>, And<B, C>> {
let x = imply::in_left(nc.clone(), |(_, c)| c);
let y = imply::in_left(nc, |(_, c)| c);
to_eq_neg((x, y))
}
pub fn eq_right_false<A: Prop, B: Prop, C: Prop>(nc: Not<C>) -> Eq<And<C, A>, And<C, B>> {
let x = imply::in_left(nc.clone(), |(c, _)| c);
let y = imply::in_left(nc, |(c, _)| c);
to_eq_neg((x, y))
}
pub fn rev_eq_left_true<A: Prop, B: Prop, C: Prop>(
(f, g): Eq<And<A, C>, And<B, C>>,
c: C
) -> Eq<A, B> {
let c2 = c.clone();
(Rc::new(move |a| f((a, c.clone())).0), Rc::new(move |b| g((b, c2.clone())).0))
}
pub fn rev_eq_right_true<A: Prop, B: Prop, C: Prop>(
(f, g): Eq<And<C, A>, And<C, B>>,
c: C
) -> Eq<A, B> {
let c2 = c.clone();
(Rc::new(move |a| f((c.clone(), a)).1), Rc::new(move |b| g((c2.clone(), b)).1))
}
pub fn from_imply<A: DProp, B: Prop>(f: Not<Imply<A, B>>) -> And<A, Not<B>> {
let f2 = Rc::new(move |x| imply::from_or(x));
let g = imply::rev_modus_ponens(f2, f);
let h = from_de_morgan(g);
and::in_left_arg(h, Rc::new(move |x| not::rev_double(x)))
}
pub fn to_imply<A: Prop, B: Prop>((a, nb): And<A, Not<B>>) -> Not<Imply<A, B>> {
Rc::new(move |ab| nb.clone()(ab(a.clone())))
}
pub fn to_eq_pos<A: Prop, B: Prop>((f0, f1): And<A, B>) -> Eq<A, B> {
(f1.map_any(), f0.map_any())
}
pub fn to_eq_neg<A: Prop, B: Prop>((f0, f1): And<Not<A>, Not<B>>) -> Eq<A, B> {
(Rc::new(move |x| match f0.clone()(x) {}), Rc::new(move |x| match f1.clone()(x) {}))
}
pub fn to_or<A: Prop, B: Prop>((x, _): And<A, B>) -> Or<A, B> {Left(x)}
pub fn paradox<A: Prop>((a, na): And<A, Not<A>>) -> False {na(a)}
pub fn paradox_e<A: Prop>((nna, na): And<Not<Not<A>>, Not<A>>) -> False {nna(na)}
pub fn fst<A: Prop, B: Prop>((a, _): And<A, B>) -> A {a}
pub fn snd<A: Prop, B: Prop>((_, b): And<A, B>) -> B {b}