猫を飼う

Twitter で tableau で解くなんてのを見かけたので、Agda でやってみました。

仮定
　 猫か犬を飼っている人は山羊を飼ってない
　 猫を飼ってない人は、犬かウサギを飼っている
　 猫も山羊も飼っていない人は、ウサギを飼っている

問題
　 山羊を飼っている人は、犬を飼っていない
　 山羊を飼っている人は、ウサギを飼っている
　 ウサギを飼っていない人は、猫を飼っている

record で書くと、

　 record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
　　 field
　　　　fact1 : ( Cat ∨ Dog ) → ¬ Goat
　　　　fact2 : ¬ Cat →　( Dog ∨ Rabbit )
　　　　fact3 : ¬ ( Cat ∨ Goat ) →　Rabbit

こんな感じか。これを仮定したmoduleを作って

　module tmp ( Cat Dog Goat Rabbit : Set ) (p :　PetResearch　Cat Dog Goat Rabbit ) where
　　open PetResearch
　　problem1 : Goat → ¬ Dog
　　problem1 g d = fact1 p (case2 d) g

簡単簡単。だけど、排中律は証明できないから仮定する必要がある。

　postulate
　　 lem : (a : Set) → a ∨ ( ¬ a )

ということは、validな命題論理式でも証明できないものがあるってことね。排中律を仮定すれば全部証明できました。

Bool代数を使う別な方法もやってみました。

　 problem1 :　( Cat Dog Goat Rabbit : Bool ) →
　　((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>　( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>　Rabbit ) )
　　=> ( Goat => ( ¬ Dog )) ≡ true
　problem1 c false false r = refl
　　...

この方法だと、入力をtrue/falseで選択ていく感じ。本来のtableauだと、絞っていく過程で式の簡略化もするはず。
こっちの方が機械的にできる利点がある。

そういえば、Solver あるはずと思ったら、一応ある。

　 open import Data.Bool.Solver using (module xor-∧-Solver)
　 open xor-∧-Solver

　 problem0' :　( Cat : Bool ) → (Cat xor Cat ) ≡ false
　 problem0' = solve 1 (λ c → (c :+ c ) := con false ) refl

とかすると動くっぽいんですが、なぜかエラーが。壊れてるかな。SAT solverと連携させる話は、少し昔に流行ったはずです。

　 http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/automaton/file/tip/agda/puzzle.agda