module BoolTactic where

open import Data.Unit using ()
open import Data.Nat hiding (_≟_)
open import Data.Empty
open import Data.Bool
open import Data.Maybe hiding (All)
open import Data.Vec hiding (_++_; map; _∈_; module _∈_; lookup)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Data.List.All hiding (map; lookup)
open import Data.List

infix 3 _∈_

data _∈_ {A : Set}(x : A) : List A  Set where
  hd :  {xs}  x  x  xs
  tl :  {y xs}  x  xs  x  y  xs

∈-++ˡ :  {A}{x : A} xs {ys}  x  xs  x  (xs ++ ys)
∈-++ˡ [] ()
∈-++ˡ (x  xs) hd     = hd
∈-++ˡ (x  xs) (tl i) = tl (∈-++ˡ xs i)

∈-++ʳ :  {A}{x : A} xs {ys}  x  ys  x  (xs ++ ys)
∈-++ʳ []       p = p
∈-++ʳ (_  xs) p = tl (∈-++ʳ xs p)

∈-map :  {A B}{x xs}(f : A  B)  x  xs  f x  map f xs
∈-map f hd     = hd
∈-map f (tl i) = tl (∈-map f i)

record Enumeration A : Set₁ where
  field
    elems    : List A
    complete :  x  x  elems

enumVec :  {n}  Enumeration (Vec Bool n)
enumVec = record
  { elems    = allVecs _
  ; complete = complete _
  }
  where
    allVecs :  n  List (Vec Bool n)
    allVecs zero    = []  []
    allVecs (suc n) = map (_∷_ true) (allVecs n) ++ map (_∷_ false) (allVecs n)

    complete :  n x  x  allVecs n
    complete zero [] = hd
    complete (suc n) (true  xs)  = ∈-++ˡ (map (_∷_ true) (allVecs n)) (∈-map _ (complete n xs))
    complete (suc n) (false  xs) = ∈-++ʳ (map (_∷_ true) (allVecs n)) (∈-map _ (complete n xs))

_!_ :  {A}{P : A  Set}{xs x}  All P xs  x  xs  P x
[] ! ()
(px  pxs) ! hd   = px
(px  pxs) ! tl i = pxs ! i

test :  {A}{P : A  Set}(xs : List A)  (∀ x  Maybe (P x))  Maybe (All P xs)
test [] f = just []
test (x  xs) f with f x | test xs f
... | just p | just ps = just (p  ps)
... | _      | _       = nothing

testAll :  {A}{P : A  Set}  Enumeration A 
          (∀ x  Maybe (P x))  Maybe (∀ x  P x)
testAll enum f with test (Enumeration.elems enum) f
... | just p  = just  x  p ! Enumeration.complete enum x)
... | nothing = nothing

decide :  {n}(lhs rhs : Vec Bool n  Bool)   bs  Maybe (lhs bs  rhs bs)
decide lhs rhs bs with lhs bs  rhs bs
... | yes p = just p
... | no _  = nothing

Hyp :  {n}(lhs rhs : Vec Bool n  Bool)  Set
Hyp lhs rhs with testAll enumVec (decide lhs rhs)
... | nothing = 
... | just _  = 

Op :   Set
Op zero    = Bool
Op (suc n) = Bool  Op n

Eqn :  {n}  (lhs rhs : Vec Bool n  Bool)  Set
Eqn {zero}  lhs rhs = lhs []  rhs []
Eqn {suc n} lhs rhs =  x  Eqn  xs  lhs (x  xs))  xs  rhs (x  xs))

curryPrf :  {n}{lhs rhs : Vec Bool n  Bool}  (∀ bs  lhs bs  rhs bs)  Eqn lhs rhs
curryPrf {zero}  f = f []
curryPrf {suc n} f = λ x  curryPrf  xs  f (x  xs))

uncurry :  {n}  Op n  Vec Bool n  Bool
uncurry {zero}  b []       = b
uncurry {suc n} f (x  xs) = uncurry (f x) xs

auto :  {n}{lhs rhs : Op n}  Hyp (uncurry lhs) (uncurry rhs) 
             Eqn (uncurry lhs) (uncurry rhs)
auto {lhs = lhs}{rhs} h with testAll enumVec (decide (uncurry lhs) (uncurry rhs))
auto () | nothing
auto _  | just p  = curryPrf p