私は(So (not (y == y)))
がUninhabited
のインスタンスであることを証明する方法を知りました。私はそれについてどうやって行くのか分かりません。それはIdrisで証明可能か、またはyのために奇妙なEq
の実装の可能性のために証明できませんか?Idrisでは、自身の型のブール不等式が無人であることを証明する方法は?
3
A
答えて
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)
が無人であることを示すのは簡単です。
関連する問題
- 1. Idris - 2つの数値の等価性を証明する
- 2. Ssreflectで単純な不等式を証明する
- 3. OpenSSLが証明書の検証エラーで自分自身をkill
- 4. 自己署名証明書で無人機を使用する方法はありますか?
- 5. Idrisは、2つの値が等しくないことを自動的に証明する方法を教えてください。
- 6. 私が++であることを証明する方法
- 7. Haskellの型レベルプログラミングで型不等式を使用する
- 8. Netlogo if自分自身と他の人との声明
- 9. 等式推論を使用してこのハスケルコードを証明する方法
- 10. Goで不明な型の値をインスタンス化する方法は?
- 11. 角度サービスがシングルトンであることを証明する方法は?
- 12. あなた自身のブロードキャストUDPパケットを無視する方法
- 13. これは右図のための方程式である場合、ブール式は
- 14. なぜこのIdrisスニペット型チェックは明示的な型なしではありませんか?
- 15. 任意のブール式を結合型または論理和型に変換する方法は、どこで見つけることができますか?
- 16. モデルなしでIdrisに何かを証明する方法はありますか?
- 17. クラスは自動的に自分自身の友人ですか?
- 18. 固有アイソメトリーが等長であることを保証する方法?
- 19. PHPで自分自身の自動インクリメントを作る方法は?
- 20. には、すべてのブラウザが自己署名証明書を無視する方法がありますか?
- 21. 証明書が個人証明書またはルート証明書であるかどうかを確認するためのプログラム的方法
- 22. このサーバの証明書はS3とPaperclipで無効です
- 23. Scalaは、明確に定義された型を無視することがあるのはなぜですか?
- 24. これを証明する方法は?
- 25. オブジェクトは自分自身を置き換えることは法的ですか?
- 26. Idrisには同等のハッカーや追跡がありますか?
- 27. IdrisはAgdaの `_`式と同等のものを持っていますか?
- 28. PG :: DatatypeMismatch:ERROR:コラム "スコア" は整数型であるが、式はここではtext型
- 29. request-promiseで自己署名証明書の問題を無視する方法
- 30. クライアントが自分自身を変えることができるイオンタイマーを作る方法は?
:https://stackoverflow.com/questions/44213584/in-idris-can-i-prove-free-theorems-eg-the-only-total-function-私はあなたがそのようなことを証明することはできないと言います。少なくとも一般的には、すべての型に対して '(==)'を実装していないためです。 – Shersh