diff options
| -rw-r--r-- | BFF.agda | 8 | ||||
| -rw-r--r-- | Bidir.agda | 24 | ||||
| -rw-r--r-- | Precond.agda | 2 |
3 files changed, 9 insertions, 25 deletions
@@ -9,8 +9,8 @@ open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List ; [] ; _∷_ ; map ; length) -open import Data.Vec using (Vec ; toList ; fromList ; tabulate ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) -open import Function using (id ; _∘_ ; flip) +open import Data.Vec using (Vec ; toList ; fromList ; allFin) renaming (lookup to lookupV ; map to mapV ; [] to []V ; _∷_ to _∷V_) +open import Function using (_∘_ ; flip) open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid) open import FinMap @@ -28,10 +28,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where assoc (i ∷V is) (b ∷V bs) = (assoc is bs) >>= (checkInsert i b) enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n - enumerate _ = tabulate id + enumerate {n} _ = allFin n enumeratel : (n : ℕ) → Vec (Fin n) n - enumeratel _ = tabulate id + enumeratel = allFin denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV @@ -13,9 +13,9 @@ open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) open import Data.List using (List) open import Data.List.All using (All) -open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map ; tabulate) renaming (lookup to lookupVec) +open import Data.Vec using (Vec ; [] ; _∷_ ; toList ; map) renaming (lookup to lookupVec) open import Data.Vec.Equality using () renaming (module Equality to VecEq) -open import Data.Vec.Properties using (tabulate-∘ ; lookup∘tabulate ; map-cong ; map-∘) +open import Data.Vec.Properties using (lookup∘tabulate ; map-cong ; map-∘ ; map-lookup-allFin) open import Data.Product using (∃ ; _×_ ; _,_ ; proj₁ ; proj₂) open import Function using (id ; _∘_ ; flip) open import Relation.Binary.Core using (refl ; _≡_) @@ -107,26 +107,10 @@ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin just x ∷ map just xs ∎ where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) -lemma-map-denumerate-enumerate : {m : ℕ} → (as : Vec Carrier m) → map (denumerate as) (enumerate as) ≡ as -lemma-map-denumerate-enumerate [] = refl -lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin - map (flip lookupVec (a ∷ as)) (tabulate Fin.suc) - ≡⟨ cong (map (flip lookupVec (a ∷ as))) (tabulate-∘ Fin.suc id) ⟩ - map (flip lookupVec (a ∷ as)) (map Fin.suc (tabulate id)) - ≡⟨ refl ⟩ - map (flip lookupVec (a ∷ as)) (map Fin.suc (enumerate as)) - ≡⟨ sym (map-∘ _ _ (enumerate as)) ⟩ - map (flip lookupVec (a ∷ as) ∘ Fin.suc) (enumerate as) - ≡⟨ refl ⟩ - map (denumerate as) (enumerate as) - ≡⟨ lemma-map-denumerate-enumerate as ⟩ - as ∎) - where open ≡-Reasoning - theorem-1 : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ just (map just s) theorem-1 G {i} s = begin bff G i s (get s) - ≡⟨ cong (bff G i s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ + ≡⟨ cong (bff G i s ∘ get) (sym (map-lookup-allFin s)) ⟩ bff G i s (get (map (denumerate s) (enumerate s))) ≡⟨ cong (bff G i s) (free-theorem (denumerate s) (enumerate s)) ⟩ bff G i s (map (denumerate s) (get (enumerate s))) @@ -146,7 +130,7 @@ theorem-1 G {i} s = begin just (map (Maybe.just ∘ denumerate s) (enumerate s)) ≡⟨ cong just (map-∘ just (denumerate s) (enumerate s)) ⟩ just (map just (map (denumerate s) (enumerate s))) - ≡⟨ cong (Maybe.just ∘ map just) (lemma-map-denumerate-enumerate s) ⟩ + ≡⟨ cong (Maybe.just ∘ map just) (map-lookup-allFin s) ⟩ just (map just s) ∎ where open ≡-Reasoning open Get G diff --git a/Precond.agda b/Precond.agda index ead2e18..a76fddc 100644 --- a/Precond.agda +++ b/Precond.agda @@ -12,7 +12,7 @@ import Category.Functor open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) open Category.Monad.RawMonad {Level.zero} Data.Maybe.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) -open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList ; tabulate) +open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList) open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘) import Data.List.All open import Data.List.Any using (here ; there) |