##これなんですが
#property-3はどうやって証明すればよいでしょう?
#あとproperty-1,2,3はいずれもAをℕに限定してしまっていますが、Aに対して証明しようとしたらどうやればいいんでしょうか?
#やろうとしているのは
#ある要素がリストに含まれる型
#ある要素がリストに含まれない型
#これらを定義したつもりですが
#ある要素がリストに含まれるなら、その要素はリストに含まれないということはない(property-1)
#ある要素がリストに含まれないなら、その要素はリストに含まれないことはない（property-2)
#これで、同じindicesを持つ_∈_と_∉_の両方が存在することはないという理解
#例えば 3 ∈ 3 ∷ [] 型の値は構成できるけど 3 ∉ 3 ∷ [] 型の値は構成できないとか
#ですが、これだけだと(ℕとList ℕに対して)双方の型がカバーする範囲が互いに排他的だということを言っていると思いますが、全空間をカバーするかは分からないので、それを証明したいと思いました.
#なので任意のℕとList ℕにたいして、どちらかであるという型の証明をしたい。
#s/型の証明/命題を証明/
#特に元ネタがあるわけでもなく、自分でスクラッチしているので_∈_や_∉_のデータ構成子が足りない可能性もありますし、命題が間違っている可能性もあるし、本当に証明できるのかも自信ないです。念の為。
#s/その要素はリストに含まれないことはない（property-2)/その要素はリストに含まれることはない（property-2)/
#すんません。いけました。
##自己解決した.
haskell-ja > Archives > 2015/08/01