module BinProof where
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality

data Bin : Set where
  I O : Bin

xor2 : Bin → Bin → Bin
xor2 I I = O
xor2 I O = I
xor2 O I = I
xor2 O O = O

xor3 : Bin → Bin → Bin → Bin
xor3 a b c = xor2 a (xor2 b c)

both : (P : Bin → Set) → Set
both P = P I × P O

bin : {R : Bin → Set} → both R → (x : Bin) → R x
bin (i , o) I = i
bin (i , o) O = o

argTy : ℕ → Set
argTy zero = Bin
argTy (suc n) = Bin → argTy n

compPfTy : (n : ℕ) → (f g : argTy n) → Set
compPfTy zero f g = f ≡ g
compPfTy (suc n) f g = both (λ x → compPfTy n (f x) (g x))

pf : {n : ℕ} → (f : argTy n) → compPfTy n f f
pf {zero} f = refl
pf {suc y} f = pf (f I) , pf (f O)

allPfTy : (n : ℕ) → (f g : argTy n) → Set
allPfTy zero f g = f ≡ g
allPfTy (suc n) f g = (x : Bin) → allPfTy n (f x) (g x)

conv : {n : ℕ} → {f g : argTy n} → compPfTy n f g → allPfTy n f g
conv {zero} pf = pf
conv {suc n} (pI , pO) = bin (conv pI , conv pO)

thm : (x y z : Bin) → xor3 x y z ≡ xor3 z y x
thm = conv (pf xor3)

thm4 : (x y z w : Bin) → xor3 (xor2 x y) z w ≡ xor2 (xor2 w y) (xor2 z x)
thm4 = conv (pf (λ (x y z w : Bin) → xor3 (xor2 x y) z w))

-- would not typecheck
-- thmWrong : (x y : Bin) → xor2 x y ≡ xor2 x x
-- thmWrong = conf (pf xor2)