use allFin rather than tabulate id
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Mar 2014 08:16:45 +0000 (09:16 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Mar 2014 08:16:45 +0000 (09:16 +0100)
BFF.agda
Bidir.agda
Precond.agda

index 9fc0afe..2ce24db 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -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
index c9227e9..56d7817 100644 (file)
@@ -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
index ead2e18..a76fddc 100644 (file)
@@ -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)