module Tautology where open import Data.Bool -- Natural numbers ADT data Nat : Set where zero : Nat suc : Nat -> Nat -- n-ary boolean function type _AryBoolOp : Nat -> Set zero AryBoolOp = Bool (suc n) AryBoolOp = Bool -> (n AryBoolOp) -- Tautology predicate (with dependent function type) taut : (n : Nat) -> n AryBoolOp -> Bool taut zero f = f taut (suc n) f = taut n (f true) ∧ taut n (f false) {- Some examples -} foo : Bool -> Bool foo _ = true foo2 : Bool -> Bool -> Bool foo2 true false = false foo2 _ _ = true test = taut (suc zero) foo test2 = taut (suc (suc zero)) foo2