2017-07-02 14 views
3

私は(So (not (y == y)))Uninhabitedのインスタンスであることを証明する方法を知りました。私はそれについてどうやって行くのか分かりません。それはIdrisで証明可能か、またはyのために奇妙なEqの実装の可能性のために証明できませんか?Idrisでは、自身の型のブール不等式が無人であることを証明する方法は?

+1

:https://stackoverflow.com/questions/44213584/in-idris-can-i-prove-free-theorems-eg-the-only-total-function-私はあなたがそのようなことを証明することはできないと言います。少なくとも一般的には、すべての型に対して '(==)'を実装していないためです。 – Shersh

答えて

3

Eqインターフェイスは、平等の通常の法則に従う実装を必要としません。しかし、私たちが行う拡張LawfulEqインタフェースを定義することができます

%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 

結果は以下のために真実ではない証明できます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 

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) 
1

Shershが正しくありません。 (==)の実装は反射的であるとは限りませんので、そうでないかもしれません。

あなたが(==)の特定の実装の性質を証明しているように、あなたはyの種類を制限することもできますが、私はあなたがdecEq(=)の代わりに、So(==)を使用したいと思います。 Not (y = y)が無人であることを示すのは簡単です。

関連する問題