toggle_binary.agda

{-# OPTIONS --safe #-}

open import Data.Bool renaming (Bool to 𝔹)
import Data.Bool as 𝔹
import Data.Bool.Properties as 𝔹ₚ
open import Data.Nat
open import Data.Vec hiding (concat; map)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary.Construct.Closure.ReflexiveTransitive
open import Relation.Binary.Construct.Closure.ReflexiveTransitive.Properties
open import Relation.Nullary

pattern 0𝔹 = false
pattern 1𝔹 = true

BinSeq : ℕ -> Set
BinSeq n = Vec 𝔹 n

data _step-to_ : ∀ {n} → BinSeq n → BinSeq n → Set where
  toggle_and_ : ∀ b {n} (bs : BinSeq n) → (b ∷ bs) step-to (not b ∷ bs)
  toggle_after_0𝔹s-1𝔹-and_ : ∀ b n {m} (bs : BinSeq m) → (replicate {n = n} 0𝔹 ++ 1𝔹 ∷ b ∷ bs) step-to (replicate {n = n} 0𝔹 ++ 1𝔹 ∷ not b ∷ bs)

_steps-to_ : ∀ {n} → BinSeq n → BinSeq n → Set
_steps-to_ = Star _step-to_

module steps-to-Reasoning {n} = StarReasoning (_step-to_ {n})
open steps-to-Reasoning

step-0𝔹-extension : ∀ {n} {bs₀ bs₁ : BinSeq n} → bs₀ step-to bs₁ → (0𝔹 ∷ bs₀) steps-to (0𝔹 ∷ bs₁)
step-0𝔹-extension (toggle b and bs) =
  begin
    0𝔹 ∷ b ∷ bs
    ⟶⟨ toggle 0𝔹 and (b ∷ bs) ⟩
    1𝔹 ∷ b ∷ bs
    ⟶⟨ toggle b after 0 0𝔹s-1𝔹-and bs ⟩
    1𝔹 ∷ not b ∷ bs
    ⟶⟨ toggle 1𝔹 and (not b ∷ bs) ⟩
    0𝔹 ∷ not b ∷ bs
  ∎
step-0𝔹-extension (toggle b after n 0𝔹s-1𝔹-and bs) =
  return (toggle b after (suc n) 0𝔹s-1𝔹-and bs)

steps-0𝔹-extension : ∀ {n} {bs₀ bs₁ : BinSeq n} → bs₀ steps-to bs₁ → (0𝔹 ∷ bs₀) steps-to (0𝔹 ∷ bs₁)
steps-0𝔹-extension {bs₀ = bs₀} {bs₁ = bs₁} r = kleisliStar (0𝔹 ∷_) step-0𝔹-extension r

steps-extension : ∀ b {n} {bs₀ bs₁ : BinSeq n} → bs₀ steps-to bs₁ → (b ∷ bs₀) steps-to (b ∷ bs₁)
steps-extension 0𝔹 = steps-0𝔹-extension
steps-extension 1𝔹 substeps =
  begin
    1𝔹 ∷ _
    ⟶⟨ toggle 1𝔹 and _ ⟩
    0𝔹 ∷ _
    ⟶⋆⟨ steps-0𝔹-extension substeps ⟩
    0𝔹 ∷ _
    ⟶⟨ toggle 0𝔹 and _ ⟩
    1𝔹 ∷ _
  ∎

steps-theorem : ∀ {n} (bs₀ bs₁ : BinSeq n) → bs₀ steps-to bs₁
steps-theorem {n = zero} [] [] = ε
steps-theorem {n = suc n} (b₀ ∷ bs₀) (b₁ ∷ bs₁)
    with  b₁ | b₁ 𝔹.≟ b₀
...    | .b₀ | yes refl = steps-extension b₀ (steps-theorem bs₀ bs₁)
...    |  b₁ | no b₁≢b₀ with sym (𝔹ₚ.¬-not b₁≢b₀)
...                       | refl = toggle b₀ and bs₀ ◅ steps-extension (not b₀) (steps-theorem bs₀ bs₁)