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