$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2007/10/27

### copy of Braun Tree

module Braun where

open import Logic.Base
open import Logic.Identity
open import Data.Nat
open import Data.Nat.Properties
open import Data.Bool


Parity = Bool

parity : Parity -> Nat
parity false = 0
parity true  = 1

data Braun (A : Set) : Nat -> Set where
nul : Braun A 0
bin : {n : Nat} -> A -> (p : Parity) ->
Braun A (parity p + n) -> Braun A n ->
Braun A (1 + parity p + (n + n))


half : Nat -> Nat
half (suc (suc n)) = suc (half n)
half _             = zero


data isEven : Nat -> Set where
evenPfBase : isEven zero
evenPfInd  : {n : Nat} -> isEven n -> isEven (suc (suc n))

data isOdd : Nat -> Set where
oddPf : {n : Nat} -> isEven n -> isOdd (suc n)


mutual

even-or-odd : (n : Nat) -> (isEven n) \/ (isOdd n)
even-or-odd zero = \/-IL evenPfBase
even-or-odd (suc zero) = \/-IR (oddPf evenPfBase)
even-or-odd (suc (suc m)) = even-or-odd-ind (even-or-odd m)
-- Why didn't "with" work?
-- even-or-odd (suc (suc m)) with (even-or-odd m)
-- ... | \/-IL evenpf = \/-IL (evenPfInd evenpf)
-- ... | \/-IR (oddPf evenpf) = \/-IR (oddPf (evenPfInd evenpf))

even-or-odd-ind : {m : Nat} -> (isEven m) \/ (isOdd m) ->
(isEven (suc (suc m))) \/ (isOdd (suc (suc m)))
even-or-odd-ind (\/-IL evenpf) = \/-IL (evenPfInd evenpf)
even-or-odd-ind (\/-IR (oddPf evenpf)) = \/-IR (oddPf (evenPfInd evenpf))


halfevensuc : {n : Nat} -> isEven n -> half (suc n) ≡ half n
halfevensuc evenPfBase = refl
halfevensuc (evenPfInd indHyp) = cong suc (halfevensuc indHyp)

halfoddsuc : {n : Nat} -> isOdd n -> half (suc n) ≡ suc (half n)
halfoddsuc (oddPf evenpf) = cong suc (sym (halfevensuc evenpf))


suc²2half : (n : Nat) ->
suc (suc (half n + half n)) ≡ half (suc (suc n)) + half (suc (suc n))
suc²2half n = cong suc (sym (+suc (half n) (half n)))


doubleEven : {n : Nat} -> isEven n -> (half n + half n) ≡ n
doubleEven evenPfBase = refl
doubleEven {suc (suc n)} (evenPfInd evenpf) =
trans (sym (suc²2half n)) (cong suc (cong suc (doubleEven evenpf)))

doubleOdd : {n : Nat} -> isOdd n -> suc (half n + half n) ≡ n
doubleOdd {suc n} (oddPf evenpf) =
cong suc (trans
(subst (\x -> x + x ≡ half n + half n) (halfevensuc evenpf) refl)
(doubleEven evenpf))


-- [Braun.copy] does NOT termination check; why?
copy : {A : Set} -> A -> (n : Nat) -> Braun A n
copy _ zero = nul
copy {A} a (suc n) with even-or-odd n
... | \/-IL evenpf =
subst (\x -> Braun A x)
(cong suc (sym (doubleEven evenpf)))
(bin a false (copy a (half n)) (copy a (half n)))
... | \/-IR oddpf =
subst (\x -> Braun A x)
(cong suc (sym (doubleOdd oddpf)))
(bin a true (copy a (suc (half n))) (copy a (half n)))


--

Labels: ,