#![allow(unreachable_code)]
use crate::*;
pub fn transitivity<A: Prop, B: Prop, C: Prop>((f0, f1): Eq<A, B>, (g0, g1): Eq<B, C>) -> Eq<A, C> {
(Rc::new(move |x| g0(f0(x))), Rc::new(move |x| f1(g1(x))))
}
pub fn trans3<A: Prop, B: Prop, C: Prop, D: Prop>(
ab: Eq<A, B>,
bc: Eq<B, C>,
cd: Eq<C, D>
) -> Eq<A, D> {transitivity(ab, transitivity(bc, cd))}
pub fn trans4<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop>(
ab: Eq<A, B>,
bc: Eq<B, C>,
cd: Eq<C, D>,
de: Eq<D, E>
) -> Eq<A, E> {transitivity(trans3(ab, bc, cd), de)}
pub fn trans5<A: Prop, B: Prop, C: Prop, D: Prop, E: Prop, F: Prop>(
ab: Eq<A, B>,
bc: Eq<B, C>,
cd: Eq<C, D>,
de: Eq<D, E>,
ef: Eq<E, F>,
) -> Eq<A, F> {transitivity(trans4(ab, bc, cd, de), ef)}
pub fn double_neg<A: Prop>(a: A) -> Eq<A, Not<Not<A>>> {
let double_neg = a.double_neg();
(Rc::new(move |x| not::double(x)), Rc::new(move |x| double_neg(x)))
}
pub fn symmetry<A: Prop, B: Prop>((f0, f1): Eq<A, B>) -> Eq<B, A> {
(f1, f0)
}
pub fn neq_symmetry<A: Prop, B: Prop>(neq: Not<Eq<A, B>>) -> Not<Eq<B, A>> {
Rc::new(move |eq| neq(symmetry(eq)))
}
pub fn imply_to_or_da<A: DProp, B: Prop>() -> Eq<Imply<A, B>, Or<Not<A>, B>> {
(Rc::new(move |x| imply::to_or_da(x)), Rc::new(move |x| imply::from_or(x)))
}
pub fn imply_to_or_db<A: Prop, B: DProp>() -> Eq<Imply<A, B>, Or<Not<A>, B>> {
(Rc::new(move |x| imply::to_or_db(x)), Rc::new(move |x| imply::from_or(x)))
}
pub fn refl<A: Prop>() -> Eq<A, A> {
(Rc::new(move |x| x), Rc::new(move |x| x))
}
pub fn anti<A: Prop>((f0, f1): Eq<A, Not<A>>) -> False {
let na: Not<A> = Rc::new(move |a| f0(a.clone())(a));
let a = f1(na.clone());
na(a)
}
pub fn true_eq<A: Prop>(a: A) -> Eq<A, True> {
(True.map_any(), Rc::new(move |_| a.clone()))
}
pub fn modus_tollens<A: Prop, B: Prop>((f0, f1): Eq<A, B>) -> Eq<Not<B>, Not<A>> {
let f02 = imply::modus_tollens(f0);
let f12 = imply::modus_tollens(f1);
(f02, f12)
}
pub fn rev_modus_tollens<A: DProp, B: DProp>((f0, f1): Eq<Not<A>, Not<B>>) -> Eq<B, A> {
let f02 = imply::rev_modus_tollens(f0);
let f12 = imply::rev_modus_tollens(f1);
(f02, f12)
}
pub fn rev_modus_tollens_excm<A: Prop, B: Prop>(
(f0, f1): Eq<Not<A>, Not<B>>,
excm_a: ExcM<A>,
excm_b: ExcM<B>,
) -> Eq<B, A> {
let f02 = imply::rev_modus_tollens_excm(f0, excm_b.clone(), excm_a.clone());
let f12 = imply::rev_modus_tollens_excm(f1, excm_a, excm_b);
(f02, f12)
}
pub fn rev_modus_tollens_eq_excm<A: Prop, B: Prop>(
(f0, f1): Eq<Not<A>, Not<B>>,
eq_excm_a_excm_b: Eq<ExcM<A>, ExcM<B>>,
) -> Eq<B, A> {
let f02 = imply::rev_modus_tollens_eq_excm(f0, eq::symmetry(eq_excm_a_excm_b.clone()));
let f12 = imply::rev_modus_tollens_eq_excm(f1, eq_excm_a_excm_b);
(f02, f12)
}
pub fn rev_modus_tollens_imply_excm<A: Prop, B: Prop>(
(f0, f1): Eq<Not<A>, Not<B>>,
a_excm_b: Imply<A, ExcM<B>>,
b_excm_a: Imply<B, ExcM<A>>,
) -> Eq<B, A> {
let f02 = imply::rev_modus_tollens_imply_excm(f0, b_excm_a);
let f12 = imply::rev_modus_tollens_imply_excm(f1, a_excm_b);
(f02, f12)
}
pub fn is_true<A: Prop>((f0, _): Eq<True, A>) -> A {
f0(True)
}
pub fn is_false<A: Prop>((_, f1): Eq<False, A>) -> Not<A> {
f1
}
pub fn to_eq_false<A: Prop>(n_a: Not<A>) -> Eq<A, False> {
(n_a, imply::absurd())
}
pub fn contra<A: Prop, B: DProp>(f: Not<Eq<A, B>>, a: A) -> Not<B> {
contra_excm(f, a, B::decide())
}
pub fn contra_excm<A: Prop, B: Prop>(
f: Not<Eq<A, B>>,
a: A,
excm_b: ExcM<B>
) -> Not<B> {
match excm_b {
Left(b) => not::absurd(f, and::to_eq_pos((a, b))),
Right(not_b) => not_b,
}
}
pub fn assoc_right<A: DProp, B: DProp, C: DProp>((f0, f1): Eq<Eq<A, B>, C>) -> Imply<A, Eq<B, C>> {
match (A::decide(), C::decide()) {
(Right(not_a), _) => Rc::new(move |x| match not_a.clone()(x) {}),
(_, Left(c)) =>
Rc::new(move |x| (c.clone().map_any(), f1.clone()(c.clone()).0(x).map_any())),
(Left(a), Right(not_c)) => {
let g = imply::rev_modus_ponens(f0, not_c.clone());
let not_b = eq::contra(g, a);
and::to_eq_neg((not_b, not_c)).map_any()
}
}
}
pub fn assoc_left<A: DProp, B: DProp, C: DProp>((f0, f1): Eq<Eq<A, B>, C>) -> Imply<Eq<B, C>, A> {
match (A::decide(), B::decide(), C::decide()) {
(Left(a), _, _) => a.map_any(),
(Right(not_a), Right(not_b), Right(not_c)) =>
match not_c(f0(and::to_eq_neg((not_a, not_b)))) {},
(_, Left(b), Right(not_c)) =>
Rc::new(move |(fb, _)| match not_c.clone()(fb(b.clone())) {}),
(_, Right(not_b), Left(c)) =>
Rc::new(move |(_, fc)| match not_b.clone()(fc(c.clone())) {}),
(Right(not_a), Left(b), Left(c)) => {
let (_, g1) = f1(c);
let a = g1(b);
match not_a(a) {}
}
}
}
pub fn assoc<A: DProp, B: DProp, C: DProp>(f: Eq<Eq<A, B>, C>) -> Eq<A, Eq<B, C>> {
(assoc_right(f.clone()), assoc_left(f))
}
pub fn swap_right<A: Prop, B: Prop, C: Prop>((f0, f1): Eq<A, Eq<B, C>>) -> Eq<A, Eq<C, B>> {
(Rc::new(move |x| {let (g0, g1) = f0(x); (g1, g0)}),
Rc::new(move |(g1, g0)| f1((g0, g1))))
}
pub fn swap_left<A: Prop, B: Prop, C: Prop>(f: Eq<Eq<A, B>, C>) -> Eq<Eq<B, A>, C> {
symmetry(swap_right(symmetry(f)))
}
pub fn in_left_arg<A: Prop, B: Prop, C: Prop>(f: Eq<A, B>, g: Eq<A, C>) -> Eq<C, B> {
symmetry(transitivity(symmetry(f), g))
}
pub fn in_right_arg<A: Prop, B: Prop, C: Prop>(f: Eq<A, B>, g: Eq<B, C>) -> Eq<A, C> {
transitivity(f, g)
}
pub fn in_left<A: Prop, B: Prop, C: Prop, F, G>(
eq_ab: Eq<A, B>,
f: F,
g: G,
) -> Eq<C, B>
where F: Fn(A) -> C + 'static,
G: Fn(C) -> A + 'static
{in_left_arg(eq_ab, (Rc::new(f), Rc::new(g)))}
pub fn in_right<A: Prop, B: Prop, C: Prop, F, G>(
eq_ab: Eq<A, B>,
f: F,
g: G,
) -> Eq<A, C>
where F: Fn(B) -> C + 'static,
G: Fn(C) -> B + 'static
{eq::symmetry(in_left(eq::symmetry(eq_ab), f, g))}
pub fn eq_left<A: Prop, B: Prop, C: Prop>(x: Eq<A, B>) -> Eq<Eq<A, C>, Eq<B, C>> {
let x2 = symmetry(x.clone());
(Rc::new(move |ac| in_left_arg(ac, x.clone())),
Rc::new(move |bc| in_left_arg(bc, x2.clone())))
}
pub fn eq_right<A: Prop, B: Prop, C: Prop>(x: Eq<A, B>) -> Eq<Eq<C, A>, Eq<C, B>> {
let x2 = symmetry(x.clone());
(Rc::new(move |ac| in_right_arg(ac, x.clone())),
Rc::new(move |bc| in_right_arg(bc, x2.clone())))
}
pub fn symmetry_eq<A: Prop, B: Prop>() -> Eq<Eq<A, B>, Eq<B, A>> {
(Rc::new(move |x| eq::symmetry(x)),
Rc::new(move |x| eq::symmetry(x)))
}
pub fn assoc_eq<A: DProp, B: DProp, C: DProp>() -> Eq<Eq<Eq<A, B>, C>, Eq<A, Eq<B, C>>> {
(Rc::new(move |x| eq::assoc(x)), Rc::new(move |x| {
let x2 = eq::symmetry(x);
let x3 = eq::in_left_arg(x2, symmetry_eq());
let x4 = eq::assoc(x3);
let x5 = eq::symmetry(x4);
eq::in_left_arg(x5, symmetry_eq())
}))
}
pub fn transpose<A: DProp, B: DProp, C: DProp, D: DProp>(
f: Eq<Eq<A, B>, Eq<C, D>>
) -> Eq<Eq<A, C>, Eq<B, D>> {
let f = eq::in_left_arg(f, eq::symmetry_eq());
let f = eq::in_right_arg(f, eq::symmetry_eq());
let f = eq::assoc(f);
let f = eq::in_right_arg(f, eq::symmetry_eq());
let f = eq::in_right_arg(f, eq::assoc_eq());
let f = eq::symmetry(f);
let f = eq::assoc(f);
let f = eq::symmetry(f);
let f = eq::assoc(f);
eq::in_left_arg(f, eq::symmetry_eq())
}
pub fn triangle<A: DProp, B: DProp, C: DProp>(f: Eq<Eq<A, B>, Eq<C, B>>) -> Eq<A, C> {
let f = eq::transpose(f);
f.1(eq::refl())
}
pub fn inv_triangle<A: DProp, B: DProp, C: DProp>(
f: Eq<Not<Eq<A, B>>, Not<Eq<C, B>>>
) -> Eq<A, C> {
let f = eq::rev_modus_tollens(f);
let f = eq::symmetry(f);
eq::triangle(f)
}
pub fn absurd() -> Eq<False, False> {
(imply::absurd(), imply::absurd())
}
pub fn neq_left<A: Prop, B: Prop, C: Prop>(
eq_ab: Eq<A, B>,
neq_ac: Not<Eq<A, C>>
) -> Not<Eq<B, C>> {
Rc::new(move |eq_bc| neq_ac(transitivity(eq_ab.clone(), eq_bc)))
}
pub fn neq_right<A: Prop, B: Prop, C: Prop>(
eq_ab: Eq<A, B>,
neq_bc: Not<Eq<B, C>>
) -> Not<Eq<A, C>> {
Rc::new(move |eq_ac| neq_bc(transitivity(symmetry(eq_ab.clone()), eq_ac)))
}
pub fn neq_to_nand<A: Prop, B: Prop>(neq: Not<Eq<A, B>>) -> Not<And<A, B>> {
Rc::new(move |(a, b)| neq((b.map_any(), a.map_any())))
}
pub fn neq_to_eq_not<A: DProp, B: DProp>(x: Not<Eq<A, B>>) -> Eq<A, Not<B>> {
let x2 = x.clone();
(Rc::new(move |a| {
let x = x2.clone();
Rc::new(move |b| x.clone()((b.map_any(), a.clone().map_any())))
}),
Rc::new(move |nb| match A::decide() {
Left(a) => a,
Right(na) => not::absurd(x.clone(), eq::rev_modus_tollens((na.map_any(), nb.map_any()))),
}))
}
pub fn eq_not_to_neq<A: Prop, B: Prop>(f: Eq<A, Not<B>>) -> Not<Eq<A, B>> {
Rc::new(move |eq_ab| anti(in_left_arg(f.clone(), eq_ab)))
}
pub fn eq_to_eq_excm<A: Prop, B: Prop>(x: Eq<A, B>) -> Eq<ExcM<A>, ExcM<B>> {
let x2 = x.clone();
(
Rc::new(move |excm_a| {
let x = x2.clone();
match excm_a {
Left(a) => Left(x.0(a)),
Right(na) => Right(eq::modus_tollens(x).1(na)),
}
}),
Rc::new(move |excm_b| {
let x = x.clone();
match excm_b {
Left(b) => Left(x.1(b)),
Right(nb) => Right(eq::modus_tollens(x).0(nb)),
}
})
)
}