From f879394a8e467a674dd1ef0b28d3f6003c5d03ac Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Wed, 15 Dec 2021 16:22:55 +0000 Subject: Finish initial definition of bitvectors. --- src/Helium/Data/BitVec/Properties.agda | 418 --------------------------------- 1 file changed, 418 deletions(-) delete mode 100644 src/Helium/Data/BitVec/Properties.agda (limited to 'src/Helium/Data/BitVec') diff --git a/src/Helium/Data/BitVec/Properties.agda b/src/Helium/Data/BitVec/Properties.agda deleted file mode 100644 index 8094f97..0000000 --- a/src/Helium/Data/BitVec/Properties.agda +++ /dev/null @@ -1,418 +0,0 @@ -{-# OPTIONS --safe --without-K #-} - -module Helium.Data.BitVec.Properties where - -import Algebra.Definitions as Algebra -open import Data.Bool as B using () renaming (Bool to Bit; false to 0#; true to 1#) -open import Data.Empty -open import Data.Fin as F hiding (_+_; _<_; _≥_) -open import Data.Fin.Properties as FP -import Data.Bool.Properties as B -open import Data.Nat as N hiding (_+_; _*_) -import Data.Nat.Properties as NP -open import Data.Product -open import Data.Vec using ([]; _∷_) -open import Data.Vec.Properties using (∷-injective; ∷-injectiveʳ) -open import Function -open import Helium.Data.BitVec -open import Relation.Binary.PropositionalEquality as ≡ - -private - variable - l m n : ℕ - -module A n = Algebra (_≡_ {A = BitVec n}) - renaming ( _DistributesOverʳ_ to ₍_₎_DistributesOverʳ_ - ; _DistributesOverˡ_ to ₍_₎_DistributesOverˡ_ - ; _DistributesOver_ to ₍_₎_DistributesOver_ - ; _IdempotentOn_ to ₍_₎_IdempotentOn_ - ; _Absorbs_ to ₍_₎_Absorbs_ - ) - - ---- Bitwise operations - --- bitwise - -bitwise-injective : ∀ f → Injective _≡_ _≡_ f → Injective _≡_ _≡_ (bitwise {n} f) -bitwise-injective f inj {[]} {[]} eq = refl -bitwise-injective f inj {x ∷ xs} {y ∷ ys} eq = uncurry (cong₂ _∷_) (dmap inj (bitwise-injective f inj) (∷-injective eq)) - -bitwise-idem : ∀ f → Algebra.IdempotentFun _≡_ f → A.IdempotentFun n (bitwise f) -bitwise-idem f idem [] = refl -bitwise-idem f idem (x ∷ xs) = cong₂ _∷_ (idem x) (bitwise-idem f idem xs) - -bitwise-involutive : ∀ f → Algebra.Involutive _≡_ f → A.Involutive n (bitwise f) -bitwise-involutive f inv [] = refl -bitwise-involutive f inv (x ∷ xs) = cong₂ _∷_ (inv x) (bitwise-involutive f inv xs) - --- bitwise₂ - -bitwise₂-assoc : ∀ ∙ → Algebra.Associative _≡_ ∙ → A.Associative n (bitwise₂ ∙) -bitwise₂-assoc ∙ assoc [] [] [] = refl -bitwise₂-assoc ∙ assoc (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (assoc x y z) (bitwise₂-assoc ∙ assoc xs ys zs) - -bitwise₂-comm : ∀ ∙ → Algebra.Commutative _≡_ ∙ → A.Commutative n (bitwise₂ ∙) -bitwise₂-comm ∙ comm [] [] = refl -bitwise₂-comm ∙ comm (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (comm x y) (bitwise₂-comm ∙ comm xs ys) - -bitwise₂-identityˡ : ∀ b ∙ → Algebra.LeftIdentity _≡_ b ∙ → A.LeftIdentity n (replicate b) (bitwise₂ ∙) -bitwise₂-identityˡ b ∙ id [] = refl -bitwise₂-identityˡ b ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-identityˡ b ∙ id xs) - -bitwise₂-identityʳ : ∀ b ∙ → Algebra.RightIdentity _≡_ b ∙ → A.RightIdentity n (replicate b) (bitwise₂ ∙) -bitwise₂-identityʳ b ∙ id [] = refl -bitwise₂-identityʳ b ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-identityʳ b ∙ id xs) - -bitwise₂-identity : ∀ b ∙ → Algebra.Identity _≡_ b ∙ → A.Identity n (replicate b) (bitwise₂ ∙) -bitwise₂-identity b ∙ = dmap (bitwise₂-identityˡ b ∙) (bitwise₂-identityʳ b ∙) - -bitwise₂-zeroˡ : ∀ b ∙ → Algebra.LeftZero _≡_ b ∙ → A.LeftZero n (replicate b) (bitwise₂ ∙) -bitwise₂-zeroˡ b ∙ z [] = refl -bitwise₂-zeroˡ b ∙ z (x ∷ xs) = cong₂ _∷_ (z x) (bitwise₂-zeroˡ b ∙ z xs) - -bitwise₂-zeroʳ : ∀ b ∙ → Algebra.RightZero _≡_ b ∙ → A.RightZero n (replicate b) (bitwise₂ ∙) -bitwise₂-zeroʳ b ∙ z [] = refl -bitwise₂-zeroʳ b ∙ z (x ∷ xs) = cong₂ _∷_ (z x) (bitwise₂-zeroʳ b ∙ z xs) - -bitwise₂-zero : ∀ b ∙ → Algebra.Zero _≡_ b ∙ → A.Zero n (replicate b) (bitwise₂ ∙) -bitwise₂-zero b ∙ = dmap (bitwise₂-zeroˡ b ∙) (bitwise₂-zeroʳ b ∙) - -bitwise₂-inverseˡ : ∀ b f ∙ → Algebra.LeftInverse _≡_ b f ∙ → A.LeftInverse n (replicate b) (bitwise f) (bitwise₂ ∙) -bitwise₂-inverseˡ b f ∙ id [] = refl -bitwise₂-inverseˡ b f ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-inverseˡ b f ∙ id xs) - -bitwise₂-inverseʳ : ∀ b f ∙ → Algebra.RightInverse _≡_ b f ∙ → A.RightInverse n (replicate b) (bitwise f) (bitwise₂ ∙) -bitwise₂-inverseʳ b f ∙ id [] = refl -bitwise₂-inverseʳ b f ∙ id (x ∷ xs) = cong₂ _∷_ (id x) (bitwise₂-inverseʳ b f ∙ id xs) - -bitwise₂-inverse : ∀ b f ∙ → Algebra.Inverse _≡_ b f ∙ → A.Inverse n (replicate b) (bitwise f) (bitwise₂ ∙) -bitwise₂-inverse b f ∙ = dmap (bitwise₂-inverseˡ b f ∙) (bitwise₂-inverseʳ b f ∙) - -bitwise₂-conicalˡ : ∀ b ∙ → Algebra.LeftConical _≡_ b ∙ → A.LeftConical n (replicate b) (bitwise₂ ∙) -bitwise₂-conicalˡ b ∙ conical [] [] eq = refl -bitwise₂-conicalˡ b ∙ conical (x ∷ xs) (y ∷ ys) eq = uncurry (cong₂ _∷_) (dmap (conical x y) (bitwise₂-conicalˡ b ∙ conical xs ys) (∷-injective eq)) - -bitwise₂-conicalʳ : ∀ b ∙ → Algebra.RightConical _≡_ b ∙ → A.RightConical n (replicate b) (bitwise₂ ∙) -bitwise₂-conicalʳ b ∙ conical [] [] eq = refl -bitwise₂-conicalʳ b ∙ conical (x ∷ xs) (y ∷ ys) eq = uncurry (cong₂ _∷_) (dmap (conical x y) (bitwise₂-conicalʳ b ∙ conical xs ys) (∷-injective eq)) - -bitwise₂-conical : ∀ b ∙ → Algebra.Conical _≡_ b ∙ → A.Conical n (replicate b) (bitwise₂ ∙) -bitwise₂-conical b ∙ = dmap (bitwise₂-conicalˡ b ∙) (bitwise₂-conicalʳ b ∙) - -bitwise₂-distribˡ : ∀ * ∙ → Algebra._DistributesOverˡ_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOverˡ (bitwise₂ ∙) -bitwise₂-distribˡ * ∙ distrib [] [] [] = refl -bitwise₂-distribˡ * ∙ distrib (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (distrib x y z) (bitwise₂-distribˡ * ∙ distrib xs ys zs) - -bitwise₂-distribʳ : ∀ * ∙ → Algebra._DistributesOverʳ_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOverʳ (bitwise₂ ∙) -bitwise₂-distribʳ * ∙ distrib [] [] [] = refl -bitwise₂-distribʳ * ∙ distrib (x ∷ xs) (y ∷ ys) (z ∷ zs) = cong₂ _∷_ (distrib x y z) (bitwise₂-distribʳ * ∙ distrib xs ys zs) - -bitwise₂-distrib : ∀ * ∙ → Algebra._DistributesOver_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) DistributesOver (bitwise₂ ∙) -bitwise₂-distrib * ∙ = dmap (bitwise₂-distribˡ * ∙) (bitwise₂-distribʳ * ∙) - -bitwise₂-idemOn : ∀ ∙ b → Algebra._IdempotentOn_ _≡_ ∙ b → A.₍ n ₎ (bitwise₂ ∙) IdempotentOn (replicate b) -bitwise₂-idemOn {zero} ∙ b idem = refl -bitwise₂-idemOn {suc n} ∙ b idem = cong₂ _∷_ idem (bitwise₂-idemOn ∙ b idem) - -bitwise₂-idem : ∀ ∙ → Algebra.Idempotent _≡_ ∙ → A.Idempotent n (bitwise₂ ∙) -bitwise₂-idem ∙ idem [] = refl -bitwise₂-idem ∙ idem (x ∷ xs) = cong₂ _∷_ (idem x) (bitwise₂-idem ∙ idem xs) - -bitwise₂-absorbs : ∀ * ∙ → Algebra._Absorbs_ _≡_ * ∙ → A.₍ n ₎ (bitwise₂ *) Absorbs (bitwise₂ ∙) -bitwise₂-absorbs * ∙ absorbs [] [] = refl -bitwise₂-absorbs * ∙ absorbs (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (absorbs x y) (bitwise₂-absorbs * ∙ absorbs xs ys) - -bitwise₂-absorptive : ∀ * ∙ → Algebra.Absorptive _≡_ * ∙ → A.Absorptive n (bitwise₂ *) (bitwise₂ ∙) -bitwise₂-absorptive * ∙ = dmap (bitwise₂-absorbs * ∙) (bitwise₂-absorbs ∙ *) - -bitwise₂-cancelˡ : ∀ ∙ → Algebra.LeftCancellative _≡_ ∙ → A.LeftCancellative n (bitwise₂ ∙) -bitwise₂-cancelˡ ∙ cancel [] {[]} {[]} eq = refl -bitwise₂-cancelˡ ∙ cancel (x ∷ xs) {y ∷ ys} {z ∷ zs} eq = uncurry (cong₂ _∷_) (dmap (cancel x) (bitwise₂-cancelˡ ∙ cancel xs) (∷-injective eq)) - -bitwise₂-cancelʳ : ∀ ∙ → Algebra.RightCancellative _≡_ ∙ → A.RightCancellative n (bitwise₂ ∙) -bitwise₂-cancelʳ ∙ cancel [] [] eq = refl -bitwise₂-cancelʳ ∙ cancel {x ∷ xs} (y ∷ ys) (z ∷ zs) eq = uncurry (cong₂ _∷_) (dmap (cancel y z) (bitwise₂-cancelʳ ∙ cancel ys zs) (∷-injective eq)) - -bitwise₂-cancel : ∀ ∙ → Algebra.Cancellative _≡_ ∙ → A.Cancellative n (bitwise₂ ∙) -bitwise₂-cancel ∙ = dmap (bitwise₂-cancelˡ ∙) (bitwise₂-cancelʳ ∙) - -bitwise₂-interchangable : ∀ * ∙ → Algebra.Interchangable _≡_ * ∙ → A.Interchangable n (bitwise₂ *) (bitwise₂ ∙) -bitwise₂-interchangable * ∙ inter [] [] [] [] = refl -bitwise₂-interchangable * ∙ inter (x ∷ xs) (y ∷ ys) (z ∷ zs) (w ∷ ws) = cong₂ _∷_ (inter x y z w) (bitwise₂-interchangable * ∙ inter xs ys zs ws) - --- not - -not-involutive : A.Involutive n not -not-involutive = bitwise-involutive B.not B.not-involutive - -not-injective : Injective _≡_ _≡_ (not {n}) -not-injective = bitwise-injective B.not B.not-injective - -not-0 : not {n} zeroes ≡ ones -not-0 {zero} = refl -not-0 {suc n} = cong (1# ∷_) not-0 - -not-1 : not {n} ones ≡ zeroes -not-1 {zero} = refl -not-1 {suc n} = cong (0# ∷_) not-1 - --- ∧ - -∧-assoc : A.Associative n _∧_ -∧-assoc = bitwise₂-assoc B._∧_ B.∧-assoc - -∧-comm : A.Commutative n _∧_ -∧-comm = bitwise₂-comm B._∧_ B.∧-comm - -∧-identityˡ : A.LeftIdentity n ones _∧_ -∧-identityˡ = bitwise₂-identityˡ 1# B._∧_ B.∧-identityˡ - -∧-identityʳ : A.RightIdentity n ones _∧_ -∧-identityʳ = bitwise₂-identityʳ 1# B._∧_ B.∧-identityʳ - -∧-identity : A.Identity n ones _∧_ -∧-identity = ∧-identityˡ , ∧-identityʳ - -∧-zeroˡ : A.LeftZero n zeroes _∧_ -∧-zeroˡ = bitwise₂-zeroˡ 0# B._∧_ B.∧-zeroˡ - -∧-zeroʳ : A.RightZero n zeroes _∧_ -∧-zeroʳ = bitwise₂-zeroʳ 0# B._∧_ B.∧-zeroʳ - -∧-zero : A.Zero n zeroes _∧_ -∧-zero = ∧-zeroˡ , ∧-zeroʳ - -∧-inverseˡ : A.LeftInverse n zeroes not _∧_ -∧-inverseˡ = bitwise₂-inverseˡ 0# B.not B._∧_ B.∧-inverseˡ - -∧-inverseʳ : A.RightInverse n zeroes not _∧_ -∧-inverseʳ = bitwise₂-inverseʳ 0# B.not B._∧_ B.∧-inverseʳ - -∧-inverse : A.Inverse n zeroes not _∧_ -∧-inverse = ∧-inverseˡ , ∧-inverseʳ - -∧-conicalˡ : A.LeftConical n ones _∧_ -∧-conicalˡ = bitwise₂-conicalˡ 1# B._∧_ λ { 1# 1# eq → refl } - -∧-conicalʳ : A.RightConical n ones _∧_ -∧-conicalʳ = bitwise₂-conicalʳ 1# B._∧_ λ { 1# 1# eq → refl } - -∧-conical : A.Conical n ones _∧_ -∧-conical = ∧-conicalˡ , ∧-conicalʳ - -∧-idem : A.Idempotent n _∧_ -∧-idem = bitwise₂-idem B._∧_ B.∧-idem - --- ∨ - -∨-assoc : A.Associative n _∨_ -∨-assoc = bitwise₂-assoc B._∨_ B.∨-assoc - -∨-comm : A.Commutative n _∨_ -∨-comm = bitwise₂-comm B._∨_ B.∨-comm - -∨-identityˡ : A.LeftIdentity n zeroes _∨_ -∨-identityˡ = bitwise₂-identityˡ 0# B._∨_ B.∨-identityˡ - -∨-identityʳ : A.RightIdentity n zeroes _∨_ -∨-identityʳ = bitwise₂-identityʳ 0# B._∨_ B.∨-identityʳ - -∨-identity : A.Identity n zeroes _∨_ -∨-identity = ∨-identityˡ , ∨-identityʳ - -∨-zeroˡ : A.LeftZero n ones _∨_ -∨-zeroˡ = bitwise₂-zeroˡ 1# B._∨_ B.∨-zeroˡ - -∨-zeroʳ : A.RightZero n ones _∨_ -∨-zeroʳ = bitwise₂-zeroʳ 1# B._∨_ B.∨-zeroʳ - -∨-zero : A.Zero n ones _∨_ -∨-zero = ∨-zeroˡ , ∨-zeroʳ - -∨-inverseˡ : A.LeftInverse n ones not _∨_ -∨-inverseˡ = bitwise₂-inverseˡ 1# B.not B._∨_ B.∨-inverseˡ - -∨-inverseʳ : A.RightInverse n ones not _∨_ -∨-inverseʳ = bitwise₂-inverseʳ 1# B.not B._∨_ B.∨-inverseʳ - -∨-inverse : A.Inverse n ones not _∨_ -∨-inverse = ∨-inverseˡ , ∨-inverseʳ - -∨-conicalˡ : A.LeftConical n zeroes _∨_ -∨-conicalˡ = bitwise₂-conicalˡ 0# B._∨_ λ { 0# 0# eq → refl } - -∨-conicalʳ : A.RightConical n zeroes _∨_ -∨-conicalʳ = bitwise₂-conicalʳ 0# B._∨_ λ { 0# 0# eq → refl } - -∨-conical : A.Conical n zeroes _∨_ -∨-conical = ∨-conicalˡ , ∨-conicalʳ - -∨-idem : A.Idempotent n _∨_ -∨-idem = bitwise₂-idem B._∨_ B.∨-idem - --- ∧ and ∨ - -∧-distribˡ-∨ : A.₍ n ₎ _∧_ DistributesOverˡ _∨_ -∧-distribˡ-∨ = bitwise₂-distribˡ B._∧_ B._∨_ B.∧-distribˡ-∨ - -∧-distribʳ-∨ : A.₍ n ₎ _∧_ DistributesOverʳ _∨_ -∧-distribʳ-∨ = bitwise₂-distribʳ B._∧_ B._∨_ B.∧-distribʳ-∨ - -∧-distrib-∨ : A.₍ n ₎ _∧_ DistributesOver _∨_ -∧-distrib-∨ = ∧-distribˡ-∨ , ∧-distribʳ-∨ - -∨-distribˡ-∧ : A.₍ n ₎ _∨_ DistributesOverˡ _∧_ -∨-distribˡ-∧ = bitwise₂-distribˡ B._∨_ B._∧_ B.∨-distribˡ-∧ - -∨-distribʳ-∧ : A.₍ n ₎ _∨_ DistributesOverʳ _∧_ -∨-distribʳ-∧ = bitwise₂-distribʳ B._∨_ B._∧_ B.∨-distribʳ-∧ - -∨-distrib-∧ : A.₍ n ₎ _∨_ DistributesOver _∧_ -∨-distrib-∧ = ∨-distribˡ-∧ , ∨-distribʳ-∧ - -∧-abs-∨ : A.₍ n ₎ _∧_ Absorbs _∨_ -∧-abs-∨ = bitwise₂-absorbs B._∧_ B._∨_ B.∧-abs-∨ - -∨-abs-∧ : A.₍ n ₎ _∨_ Absorbs _∧_ -∨-abs-∧ = bitwise₂-absorbs B._∨_ B._∧_ B.∨-abs-∧ - -∧-∨-absorptive : A.Absorptive n _∧_ _∨_ -∧-∨-absorptive = ∧-abs-∨ , ∨-abs-∧ - --- xor - -private - bxor-comm : ∀ x y → x B.xor y ≡ y B.xor x - bxor-comm 0# 0# = refl - bxor-comm 0# 1# = refl - bxor-comm 1# 0# = refl - bxor-comm 1# 1# = refl - - bxor-identityʳ : ∀ x → x B.xor 0# ≡ x - bxor-identityʳ 0# = refl - bxor-identityʳ 1# = refl - - bxor-annihilate : ∀ x → x B.xor x ≡ 0# - bxor-annihilate 0# = refl - bxor-annihilate 1# = refl - - bxor-distribˡ-not : ∀ x y → B.not (x B.xor y) ≡ B.not x B.xor y - bxor-distribˡ-not 0# y = refl - bxor-distribˡ-not 1# y = B.not-involutive y - - bxor-distribʳ-not : ∀ x y → B.not (x B.xor y) ≡ x B.xor B.not y - bxor-distribʳ-not 0# y = refl - bxor-distribʳ-not 1# y = refl - -xor-assoc : A.Associative n _xor_ -xor-assoc = bitwise₂-assoc B._xor_ (λ - { 0# y z → refl - ; 1# y z → sym (bxor-distribˡ-not y z) - }) - -xor-comm : A.Commutative n _xor_ -xor-comm = bitwise₂-comm B._xor_ bxor-comm - -xor-identityˡ : A.LeftIdentity n zeroes _xor_ -xor-identityˡ = bitwise₂-identityˡ 0# B._xor_ λ _ → refl - -xor-identityʳ : A.RightIdentity n zeroes _xor_ -xor-identityʳ = bitwise₂-identityʳ 0# B._xor_ bxor-identityʳ - -xor-identity : A.Identity n zeroes _xor_ -xor-identity = xor-identityˡ , xor-identityʳ - -xor-inverseˡ : A.LeftInverse n ones not _xor_ -xor-inverseˡ = bitwise₂-inverseˡ 1# B.not B._xor_ (λ { 0# → refl ; 1# → refl }) - -xor-inverseʳ : A.RightInverse n ones not _xor_ -xor-inverseʳ = bitwise₂-inverseʳ 1# B.not B._xor_ (λ { 0# → refl ; 1# → refl }) - -xor-inverse : A.Inverse n ones not _xor_ -xor-inverse = xor-inverseˡ , xor-inverseʳ - -xor-annihilate : ∀ (xs : BitVec n) → xs xor xs ≡ zeroes -xor-annihilate [] = refl -xor-annihilate (x ∷ xs) = cong₂ _∷_ (bxor-annihilate x) (xor-annihilate xs) - -xor-cancelˡ : A.LeftCancellative n _xor_ -xor-cancelˡ = bitwise₂-cancelˡ B._xor_ (λ { 0# eq → eq ; 1# eq → B.not-injective eq }) - -xor-cancelʳ : A.RightCancellative n _xor_ -xor-cancelʳ = bitwise₂-cancelʳ B._xor_ (λ - { 0# 0# eq → refl - ; 0# 1# eq → ⊥-elim (B.not-¬ refl eq) - ; 1# 0# eq → ⊥-elim (B.not-¬ refl (sym eq)) - ; 1# 1# eq → refl - }) - -xor-cancel : A.Cancellative n _xor_ -xor-cancel = xor-cancelˡ , xor-cancelʳ - --- not and xor - -xor-distribˡ-not : ∀ (xs ys : BitVec n) → not (xs xor ys) ≡ not xs xor ys -xor-distribˡ-not [] [] = refl -xor-distribˡ-not (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (bxor-distribˡ-not x y) (xor-distribˡ-not xs ys) - -xor-distribʳ-not : ∀ (xs ys : BitVec n) → not (xs xor ys) ≡ xs xor not ys -xor-distribʳ-not [] [] = refl -xor-distribʳ-not (x ∷ xs) (y ∷ ys) = cong₂ _∷_ (bxor-distribʳ-not x y) (xor-distribʳ-not xs ys) - --- ∧ and xor - -∧-distribˡ-xor : A.₍ n ₎ _∧_ DistributesOverˡ _xor_ -∧-distribˡ-xor = bitwise₂-distribˡ B._∧_ B._xor_ (λ { 0# y z → refl ; 1# y z → refl }) - -∧-distribʳ-xor : A.₍ n ₎ _∧_ DistributesOverʳ _xor_ -∧-distribʳ-xor = bitwise₂-distribʳ B._∧_ B._xor_ (λ - { x 0# z → refl - ; x 1# 0# → sym (bxor-identityʳ x) - ; x 1# 1# → sym (bxor-annihilate x) - }) - -∧-distrib-xor : A.₍ n ₎ _∧_ DistributesOver _xor_ -∧-distrib-xor = ∧-distribˡ-xor , ∧-distribʳ-xor - --- ∨ and xor - -∨-squash-xor : ∀ (xs ys : BitVec n) → xs ∨ (xs xor ys) ≡ xs ∨ ys -∨-squash-xor [] [] = refl -∨-squash-xor (x ∷ xs) (y ∷ ys) = - flip (cong₂ _∷_) (∨-squash-xor xs ys) (case x return (λ x → x B.∨ x B.xor y ≡ x B.∨ y) of λ - { 0# → refl - ; 1# → refl - }) - - --- Conversions - --- bitToFin and finToBit - -bitToFin-finToBit : ∀ x → bitToFin (finToBit x) ≡ x -bitToFin-finToBit zero = refl -bitToFin-finToBit (suc zero) = refl - -finToBit-bitToFin : ∀ x → finToBit (bitToFin x) ≡ x -finToBit-bitToFin 0# = refl -finToBit-bitToFin 1# = refl - --- toFin and fromFin - -fromFin-toFin : ∀ xs → fromFin {n} (toFin {n} xs) ≡ xs -fromFin-toFin [] = refl -fromFin-toFin {suc n} (x ∷ xs) with quotRem {2} (2 ^ n) (combine (bitToFin x) (toFin xs)) | remQuot-combine (bitToFin x) (toFin xs) -... | .(toFin xs) , .(bitToFin x) | refl = cong₂ _∷_ (finToBit-bitToFin x) (fromFin-toFin xs) - -toFin-fromFin : ∀ x → toFin {n} (fromFin x) ≡ x -toFin-fromFin {zero} zero = refl -toFin-fromFin {suc n} x = begin - combine (bitToFin (finToBit (proj₁ rq))) (toFin (fromFin {n} (proj₂ rq))) ≡⟨ eq₁ ⟩ - combine (proj₁ rq) (proj₂ rq) ≡⟨ combine-remQuot (2 ^ n) x ⟩ - x ∎ - where - open ≡-Reasoning - rq = remQuot {2} (2 ^ n) x - eq₁ = cong₂ combine (bitToFin-finToBit (proj₁ rq)) (toFin-fromFin {n} (proj₂ rq)) - -- cgit v1.2.3