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  _∈_

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