dependent-type - 如何证明一个类型与自身的 bool 不等式在 Idris 中是无人居住的？

Question

我想知道如何证明 (So (not (y == y))) 是 Uninhabited 的实例，但我不确定如何证明去吧。它在 Idris 中是可证明的，还是由于 y 的奇怪 Eq 实现的可能性而无法证明？

Answer 1

Eq 接口(interface)不需要实现来遵循正常的相等法则。但是，我们可以定义一个扩展的 LawfulEq 接口(interface)，它可以:

%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} (==)

问题中要求的结果可以为 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

下面的怪异类型可以证明结果不正确:

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

Weird (==) 可以证明不是自反的，因此 LawfulEq Weird 的实现是不可能的:

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)