diff options
Diffstat (limited to 'Data')
| -rw-r--r-- | Data/Circuit/Merge.agda | 27 | ||||
| -rw-r--r-- | Data/Fin/Preimage.agda | 6 |
2 files changed, 22 insertions, 11 deletions
diff --git a/Data/Circuit/Merge.agda b/Data/Circuit/Merge.agda index b399cb4..82c0d92 100644 --- a/Data/Circuit/Merge.agda +++ b/Data/Circuit/Merge.agda @@ -20,7 +20,8 @@ open import Data.Subset.Functional open import Data.Vector as V using (Vector; head; tail; removeAt) open import Data.Fin.Permutation using - ( Permutation′ + ( Permutation + ; Permutation′ ; _⟨$⟩ˡ_ ; _⟨$⟩ʳ_ ; inverseˡ ; inverseʳ ; id @@ -101,7 +102,7 @@ merge-cong₁ = merge-with-cong U merge-cong₂ : {A : ℕ} (v : Vector Value A) {S₁ S₂ : Subset A} → S₁ ≗ S₂ → merge v S₁ ≡ merge v S₂ merge-cong₂ = merge-with-cong₂ U -merge-⊥ : {A : ℕ} (v : Vector Value A) → merge-with U v ⊥ ≡ U +merge-⊥ : {A : ℕ} (v : Vector Value A) → merge v ⊥ ≡ U merge-⊥ = merge-with-⊥ U merge-[] : (v : Vector Value 0) (S : Subset 0) → merge v S ≡ U @@ -172,13 +173,15 @@ open module FStruct {A B : Set} = FunctionStructures {_} {_} {_} {_} {A} _≡_ { open IsInverse using () renaming (inverseˡ to invˡ; inverseʳ to invʳ) merge-preimage-ρ - : {A : ℕ} - → (ρ : Permutation′ A) + : {A B : ℕ} + → (ρ : Permutation A B) → (v : Vector Value A) - (S : Subset A) + (S : Subset B) → merge v (preimage (ρ ⟨$⟩ʳ_) S) ≡ merge (v ∘ (ρ ⟨$⟩ˡ_)) S -merge-preimage-ρ {zero} ρ v S = merge-[]₂ -merge-preimage-ρ {suc A} ρ v S = begin +merge-preimage-ρ {zero} {zero} ρ v S = merge-[]₂ +merge-preimage-ρ {zero} {suc B} ρ v S with () ← ρ ⟨$⟩ˡ zero +merge-preimage-ρ {suc A} {zero} ρ v S with () ← ρ ⟨$⟩ʳ zero +merge-preimage-ρ {suc A} {suc B} ρ v S = begin merge v (preimage ρʳ S) ≡⟨ merge-removeAt (head ρˡ) v (preimage ρʳ S) ⟩ join (head (v ∘ ρˡ) when S (ρʳ (ρˡ zero))) @@ -190,19 +193,21 @@ merge-preimage-ρ {suc A} ρ v S = begin merge-with vρˡ0? (tail (v ∘ ρˡ)) S- ≡⟨ merge-suc (v ∘ ρˡ) S ⟨ merge (v ∘ ρˡ) S ∎ where - ρˡ ρʳ : Fin (suc A) → Fin (suc A) + ρˡ : Fin (suc B) → Fin (suc A) ρˡ = ρ ⟨$⟩ˡ_ + ρʳ : Fin (suc A) → Fin (suc B) ρʳ = ρ ⟨$⟩ʳ_ - ρ- : Permutation′ A + ρ- : Permutation A B ρ- = remove (head ρˡ) ρ - ρˡ- ρʳ- : Fin A → Fin A + ρˡ- : Fin B → Fin A ρˡ- = ρ- ⟨$⟩ˡ_ + ρʳ- : Fin A → Fin B ρʳ- = ρ- ⟨$⟩ʳ_ v- : Vector Value A v- = removeAt v (head ρˡ) [preimageρʳS]- : Subset A [preimageρʳS]- = removeAt (preimage ρʳ S) (head ρˡ) - S- : Subset A + S- : Subset B S- = tail S vρˡ0? : Value vρˡ0? = head (v ∘ ρˡ) when head S diff --git a/Data/Fin/Preimage.agda b/Data/Fin/Preimage.agda index f6e4373..4f7ea43 100644 --- a/Data/Fin/Preimage.agda +++ b/Data/Fin/Preimage.agda @@ -40,3 +40,9 @@ preimage-∘ (z : Fin C) → preimage (g ∘ f) ⁅ z ⁆ ≗ preimage f (preimage g ⁅ z ⁆) preimage-∘ f g S x = ≡.refl + +preimage-⊥ + : {n m : ℕ} + (f : Fin n → Fin m) + → preimage f ⊥ ≗ ⊥ +preimage-⊥ f x = ≡.refl |