use crate::*;
use hooo::*;
pub use protection::*;
mod protection {
use super::*;
#[derive(Clone)]
pub struct Pos<A>(Para<Para<A>>);
pub type Nec<A> = Not<Pos<Not<A>>>;
impl<A> Pos<A> {
pub fn new(x: Para<Para<A>>) -> Self {Pos(x)}
}
pub unsafe fn pos_to_para_para<A: Prop>(Pos(x): Pos<A>) -> Para<Para<A>> {x}
}
impl<A: DProp> Decidable for Pos<A> {
fn decide() -> ExcM<Pos<A>> {
match para_decide() {
Left(x) => Left(Pos::new(x)),
Right(y) => Right(imply::in_left(y, |x| unsafe {pos_to_para_para(x)})),
}
}
}
pub fn nec_to_tauto<A: DProp>(nec_a: Nec<A>) -> Tauto<A> {
match tauto_decide() {
Left(tauto_a) => tauto_a,
Right(ntauto_a) => {
let para_a = tauto_not_to_para(hooo_rev_not(ntauto_a));
let x: Para<Not<A>> = npos_to_para(nec_a);
imply::absurd()(para_rev_not(x)(para_a))
}
}
}
pub unsafe fn tauto_to_nec<A: DProp>(tauto_a: Tauto<A>) -> Nec<A> {
Rc::new(move |pos_na| {
match para_decide() {
Left(para_na) => pos_to_para_para(pos_na)(para_na),
Right(npara_na) => {
let para_a = para_not_rev_double(pow_not(npara_na));
para_a(tauto_a(True))
}
}
})
}
pub fn npos_to_para<A: DProp>(npos: Not<Pos<A>>) -> Para<A> {
match para_decide() {
Left(para_a) => para_a,
Right(npara_a) => imply::absurd()(pos_not(npos)(npara_a)),
}
}
pub unsafe fn para_to_npos<A: Prop>(para_a: Para<A>) -> Not<Pos<A>> {
Rc::new(move |pos_a| pos_to_para_para(pos_a)(para_a))
}
pub fn not_not_to_pos<A: DProp>(nna: Not<Not<A>>) -> Pos<A> {
Pos::new(hooo::not_not_to_para_para(nna))
}
pub unsafe fn pos_to_not_not<A: DProp>(pos: Pos<A>) -> Not<Not<A>> {
hooo::para_para_to_not_not(pos_to_para_para(pos))
}
pub fn eq_nnecn_pos<A: DProp>() -> Eq<Not<Nec<Not<A>>>, Pos<A>> {
fn f<A: DProp>(_: True) -> Eq<Not<Para<A>>, Not<Para<Not<Not<A>>>>> {
(
Rc::new(move |x| para_rev_not(para_not_triple(pow_not(x)))),
Rc::new(move |x| para_rev_not(para_not_rev_triple(pow_not(x))))
)
}
fn g<A: DProp>(_: True) -> Eq<Not<Para<A>>, Not<Para<Not<Not<A>>>>> {
(
Rc::new(move |x| para_rev_not(para_not_triple(pow_not(x)))),
Rc::new(move |x| para_rev_not(para_not_rev_double(pow_not(x))))
)
}
(
Rc::new(move |nnec_na| {
match Pos::<A>::decide() {
Left(pos_a) => pos_a,
Right(npos_a) => {
let x = pos_not(npos_a);
let x = para_in_arg(x, f);
let x = para_rev_not(x);
let x = imply::in_left(x, |y| unsafe {pos_to_para_para(y)});
imply::absurd()(nnec_na(x))
}
}
}),
Rc::new(move |x| {
let x = unsafe {pos_to_para_para(x)};
let x = not::double(x);
let x = imply::in_left(x, |y| para_rev_not(y));
let x = imply::in_left(x, |y| para_in_arg(y, tauto_eq_symmetry(g)));
let x: Not<Not<Para<Para<Not<Not<A>>>>>> = imply::in_left(x, pow_not);
nnpara_para_to_nnpos(x)
})
)
}
pub fn eq_nposn_nec<A: Prop>() -> Eq<Not<Pos<Not<A>>>, Nec<A>> {
eq::refl()
}
pub fn eq_nnec_posn<A: DProp>() -> Eq<Not<Nec<A>>, Pos<Not<A>>> {
fn g<A: DProp>(_: True) -> Eq<Not<Not<Para<Not<A>>>>, Para<Not<A>>> {
fn f<A: DProp>(_: True) -> Eq<Not<Not<Not<A>>>, Not<A>> {
(Rc::new(move |x| not::rev_triple(x)), Rc::new(move |x| not::double(x)))
}
(
Rc::new(move |x| {
let x = imply::in_left(x, |y| para_rev_not(y));
para_in_arg(pow_not(x), f)
}),
Rc::new(move |x| {
let x = para_in_arg(x, tauto_eq_symmetry(f));
let x: Not<Para<Not<Not<A>>>> = para_rev_not(x);
imply::in_left(x, pow_not)
})
)
}
(
Rc::new(move |nnec_a: Not<Not<Pos<Not<A>>>>| {
let x = unsafe {nnpos_to_nnpara_para(nnec_a)};
let x = imply::in_left(x, |y| para_rev_not(y));
let x = pow_not(x);
Pos::new(para_in_arg(x, g))
}),
Rc::new(move |pos_na| {
let x = unsafe {pos_to_para_para(pos_na)};
let x: Para<Not<Not<Para<Not<A>>>>> = para_in_arg(x, tauto_eq_symmetry(g));
let x = para_rev_not(x);
let x: Not<Not<Para<Para<Not<A>>>>> = imply::in_left(x, pow_not);
imply::in_left(x, |y| imply::in_left(y, Pos::new))
})
)
}
pub fn eq_posn_nnec<A: DProp>() -> Eq<Not<Pos<A>>, Nec<Not<A>>> {
fn f<A: DProp>(_: True) -> Eq<Not<Para<A>>, Not<Para<Not<Not<A>>>>> {
fn g<A: Prop>(_: True) -> Eq<Not<Not<Not<A>>>, Not<A>> {
(Rc::new(move |x| not::rev_triple(x)), Rc::new(move |x| not::double(x)))
}
(
Rc::new(move |x| {
let x = pow_not(x);
let x = para_in_arg(x, tauto_eq_symmetry(g));
para_rev_not(x)
}),
Rc::new(move |x| {
let x = pow_not(x);
let x = para_in_arg(x, g);
para_rev_not(x)
})
)
}
(
Rc::new(move |x| {
let x = pos_not(x);
let x = para_in_arg(x, f);
imply::in_left(para_rev_not(x), |y| unsafe {pos_to_para_para(y)})
}),
Rc::new(move |x| {
let x = pos_not(x);
let x = para_in_arg(x, tauto_eq_symmetry(f));
imply::in_left(para_rev_not(x), |y| unsafe {pos_to_para_para(y)})
})
)
}
pub unsafe fn nnpos_to_nnpara_para<A: Prop>(x: Not<Not<Pos<A>>>) -> Not<Not<Para<Para<A>>>> {
imply::in_left(x, |y| imply::in_left(y, |x| pos_to_para_para(x)))
}
pub fn nnpara_para_to_nnpos<A: Prop>(x: Not<Not<Para<Para<A>>>>) -> Not<Not<Pos<A>>> {
imply::in_left(x, |y| imply::in_left(y, |x| Pos::new(x)))
}
pub fn to_pos_tauto_eq<A: Prop>(
y: Tauto<Imply<Para<Para<A>>, Pos<A>>>
) -> Tauto<Eq<Para<Para<A>>, Pos<A>>> {
fn f<A: Prop>(_: True) -> Imply<Pos<A>, Para<Para<A>>> {
Rc::new(move |pos_a| unsafe {pos_to_para_para(pos_a)})
}
hooo_rev_and((y, f::<A>))
}
pub fn pos_not<A: DProp>(x: Not<Pos<A>>) -> Para<Not<Para<A>>> {
pow_not(imply::in_left(x, |y| Pos::new(y)))
}