logic.idr

double_negate : a -> (a -> Void) -> Void
double_negate a not_a = not_a a

double_negate_rev : Dec a -> ((a -> Void) -> Void) -> a
double_negate_rev (Yes proof_a) _ = proof_a
double_negate_rev (No contra_a) f = absurd (f contra_a)

counter_position : (a -> b) -> (b -> Void) -> (a -> Void)
counter_position f g = g . f

counter_position_rev : Dec b -> ((b -> Void) -> (a -> Void)) -> a -> b
counter_position_rev (Yes proof_b) _ _ = proof_b
counter_position_rev (No contra_b) c x = absurd $ c contra_b x

truth_allows_any_assumption : b -> (a -> b)
truth_allows_any_assumption = const

contradiction_to_any : a -> (a -> Void) -> b
contradiction_to_any a f = absurd (f a)

function_to_either : Either (Dec a) (Dec b) -> (a -> b) -> Either (a -> Void) b
function_to_either (Left  (Yes proof_a)) f = Right (f proof_a)
function_to_either (Left  (No contra_a)) _ = Left contra_a
function_to_either (Right (Yes proof_b)) _ = Right proof_b
function_to_either (Right (No contra_b)) f = Left (contra_b . f)

either_to_function : Either (a -> Void) b -> a -> b
either_to_function (Right b) a = b
either_to_function (Left  f) a = absurd (f a)

pair_to_negate : a -> (b -> Void) -> (a -> b) -> Void
pair_to_negate a f g = f (g a)

negate_to_pair : Dec a -> ((a -> b) -> Void) -> Pair a (b -> Void)
negate_to_pair (Yes proof_a) f = (proof_a, f . const)
negate_to_pair (No contra_a) f = (absurd $ f (absurd . contra_a), f . const)

reductio_ad_absurdum : Dec b -> (a -> (b -> Void) -> Void) -> a -> b
reductio_ad_absurdum (Yes proof_b) _ _ = proof_b
reductio_ad_absurdum (No contra_b) f a = absurd $ f a contra_b

reductio_ad_absurdum_rev : (a -> b) -> a -> (b -> Void) -> Void
reductio_ad_absurdum_rev f a not_b = not_b $ f a

not_exists : (a : Type) -> (p : a -> Type) -> ((x : a ** p x) -> Void) -> (x : a) -> p x -> Void
not_exists _ _ f x px = f (x ** px)

not_exists_rev : (a : Type) -> (p : a -> Type) -> ((x : a) -> p x -> Void) -> (x : a ** p x) -> Void
not_exists_rev a p not_for_all (x ** px) = not_for_all x px

HasException : (a : Type) -> (a -> Type) -> Type
HasException a p = (x : a ** p x -> Void)

not_for_all : (a : Type) -> (p : a -> Type) -> ((x : a) -> Dec (p x)) -> Dec (HasException a p) -> (((x : a) -> p x) -> Void) -> HasException a p
not_for_all a p dec_all_pa dec_conclusion = reductio_ad_absurdum dec_conclusion $ \not_all_pa => \not_conclusion =>
  not_all_pa $ \x => double_negate_rev (dec_all_pa x) $ not_exists a (\a' => p a' -> Void) not_conclusion x

not_for_all_rev : (a : Type) -> (p : a -> Type) -> HasException a p  -> ((x : a) -> p x) -> Void
not_for_all_rev a p (x ** not_for_x) for_all_pa = not_for_x $ for_all_pa x

de_morganA : (Either a b -> Void) -> Pair (a -> Void) (b -> Void)
de_morganA f = (f . Left, f . Right)

de_morganA_rev : Pair (a -> Void) (b -> Void) -> Either a b -> Void
de_morganA_rev (f, _) (Left a)  = f a
de_morganA_rev (_, f) (Right b) = f b

de_morganB : Either (Dec a) (Dec b) -> (Pair a b -> Void) -> Either (a -> Void) (b -> Void)
de_morganB (Left  (Yes proof_a)) f = Right (\b => f (proof_a, b))
de_morganB (Left  (No contra_a)) f = Left contra_a
de_morganB (Right (Yes proof_b)) f = Left (\a => f (a, proof_b))
de_morganB (Right (No contra_b)) f = Right contra_b

de_morganB_rev : Pair (a -> Void) (b -> Void) -> Either a b -> Void
de_morganB_rev (f, _) (Left a)  = f a
de_morganB_rev (_, f) (Right b) = f b