How to prove that a Boolean inequality of type with itself is uninhabited in Idris?
The interface Eq
does not require the implementation to follow the normal laws of equality. But we can define an extended interface LawfulEq
that does:
%default total
is_reflexive : (t -> t -> Bool) -> Type
is_reflexive {t} rel = (x : t) -> rel x x = True
is_symmetric : (t -> t -> Bool) -> Type
is_symmetric {t} rel = (x : t) -> (y : t) -> rel x y = rel y x
is_transitive : (t -> t -> Bool) -> Type
is_transitive {t} rel = (x : t) -> (y : t) -> (z : t) -> rel x y = True -> rel x z = rel y z
interface Eq t => LawfulEq t where
eq_is_reflexive : is_reflexive {t} (==)
eq_is_symmetric : is_symmetric {t} (==)
eq_is_transitive : is_transitive {t} (==)
The result asked in the question can be proven for type Bool
:
so_false_is_void : So False -> Void
so_false_is_void Oh impossible
so_not_y_eq_y_is_void : (y : Bool) -> So (not (y == y)) -> Void
so_not_y_eq_y_is_void False = so_false_is_void
so_not_y_eq_y_is_void True = so_false_is_void
The result can be proven wrong for the following type Weird
:
data Weird = W
Eq Weird where
W == W = False
weird_so_not_y_eq_y : (y : Weird) -> So (not (y == y))
weird_so_not_y_eq_y W = Oh
It can be shown that Weird (==)
it is not reflexive, so implementation is LawfulEq Weird
not possible:
weird_eq_not_reflexive : is_reflexive {t=Weird} (==) -> Void
weird_eq_not_reflexive is_reflexive_eq =
let w_eq_w_is_true = is_reflexive_eq W in
trueNotFalse $ trans (sym w_eq_w_is_true) (the (W == W = False) Refl)
source to share
Shersh is right: you can't. The implementations are (==)
not guaranteed to be reflexive, so this may not be true.
You can restrict the type y
to prove an implementation-specific property (==)
, but I suspect you want to use decEq
both (=)
instead of So
and (==)
. It is easy to show that we are Not (y = y)
uninhabited.
source to share