# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1572221113 -32400
# Node ID 797dd1369472e9cd0f67b0bfa7ad4eb53a7d143d
# Parent  6d50a933bcb3d9c3a78849dda0d5fd0bb549957e
try solver

diff -r 6d50a933bcb3 -r 797dd1369472 agda/puzzle.agda
--- a/agda/puzzle.agda	Mon Oct 28 01:58:25 2019 +0900
+++ b/agda/puzzle.agda	Mon Oct 28 09:05:13 2019 +0900
@@ -44,10 +44,10 @@
     problem2 g with lem Cat | lem Dog
     problem2 g | case1 c | d = ⊥-elim ( fact1 p (case1 c ) g )
     problem2 g | case2 ¬c | case1 d = ⊥-elim ( fact1 p (case2 d ) g )
-    problem2 g | case2 ¬c | case2 ¬d with fact3 p | lem Rabbit
-    ... | _  | case1  r = r
-    ... | f3 | case2 ¬r = f3 lemma2 where
-        lemma2 : Cat ∨ Goat → ⊥
+    problem2 g | case2 ¬c | case2 ¬d with lem Rabbit
+    ... | case1  r = r
+    ... | case2 ¬r = fact3 p lemma2 where
+        lemma2 : ¬ ( Cat ∨ Goat )
         lemma2 (case1 c) = ¬c c
         lemma2 (case2 g) with fact2 p ¬c
         lemma2 (case2 g) | case1 d = ¬d d
@@ -115,3 +115,80 @@
   problem3 false false true false = refl
   problem3 false true false false = refl
   problem3 false true true false = refl
+
+module pet-research2 ( Cat Dog Goat Rabbit : Set ) where
+
+  open import Data.Bool hiding ( _∨_ )
+  open import Relation.Binary
+  open import Relation.Binary.PropositionalEquality 
+
+  ¬_ : Bool → Bool
+  ¬ p = p xor true
+
+  infixr 5 _∨_ 
+  _∨_ :  Bool → Bool → Bool
+  a ∨ b = ¬ ( (¬ a) ∧ (¬ b ) )
+
+  _=>_ :  Bool → Bool → Bool
+  a => b = (¬ a ) ∨ b 
+
+  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
+
+  problem1' :  ( Cat : Bool ) → (Cat ∧ (Cat xor true ))  ≡ false 
+  problem1' = solve 1 (λ c → ((c :* (c :+ con true )) ) := con false ) {!!}
+
+  open import Data.Nat
+  :¬_ : {n : ℕ} → Polynomial n → Polynomial n
+  :¬ p = p :+ con true
+
+  _:∨_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+  a :∨ b = :¬ ( ( :¬ a ) :* ( :¬ b ))
+
+  _:=>_ : {n : ℕ} → Polynomial n → Polynomial n → Polynomial n
+  a :=> b = ( :¬ a ) :∨ b 
+
+  _:∧_ = _:*_
+
+  infixr 6 _:∧_
+  infixr 5 _:∨_ 
+
+  problem0 :  ( Cat Dog Goat Rabbit : Bool ) →
+    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+    => (Cat ∨ Dog ∨ Goat ∨ Rabbit) ≡ true
+  problem0 = solve 4 ( λ Cat Dog Goat Rabbit → (
+    ( ((Cat :∨ Dog ) :=> (:¬ Goat)) :∧ ( ((:¬ Cat ) :=>  ( Dog :∨ Rabbit )) :∧ (( :¬ ( Cat :∨ Goat ) ) :=>  Rabbit)  ))
+    :=> ( Cat :∨ (Dog :∨ ( Goat :∨ Rabbit))) ) := con true ) {!!}
+
+  problem1 :  ( Cat Dog Goat Rabbit : Bool ) →
+    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+    => ( Goat => ( ¬ Dog )) ≡ true
+  problem1 c false false r = {!!}
+  problem1 c true false r = {!!}
+  problem1 c false true r = {!!}
+  problem1 false true true r = refl
+  problem1 true true true r = refl
+
+  problem2 :  ( Cat Dog Goat Rabbit : Bool ) →
+    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+    => ( Goat => Rabbit ) ≡ true
+  problem2 c d false false = {!!}
+  problem2 c d false true = {!!}
+  problem2 c d true true = {!!}
+  problem2 true d true false = refl
+  problem2 false false true false = refl
+  problem2 false true true false = refl
+
+  problem3 :  ( Cat Dog Goat Rabbit : Bool ) →
+    ((( Cat ∨ Dog ) => (¬ Goat) ) ∧ ( (¬ Cat ) =>  ( Dog ∨ Rabbit ) ) ∧ ( ( ¬ ( Cat ∨ Goat ) ) =>  Rabbit ) )
+    => ( (¬ Rabbit ) => Cat ) ≡ true
+  problem3 false d g true = {!!}
+  problem3 true d g true = {!!}
+  problem3 true d g false = {!!}
+  problem3 false false false false = refl
+  problem3 false false true false = refl
+  problem3 false true false false = refl
+  problem3 false true true false = refl