From eb6be3f9358e441fcee9256da5aae8915453f0a5 Mon Sep 17 00:00:00 2001 From: Helmut Grohne Date: Thu, 9 Feb 2012 11:58:54 +0100 Subject: [PATCH] introduce denumerate It is some kind of counter part to enumerate. That is: map (denumerate s) (enumerate s) \== s It can be employed in bff and I believe it to simplify reasoning on bff. --- Bidir.agda | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/Bidir.agda b/Bidir.agda index 15a389c..0c9f0e5 100644 --- a/Bidir.agda +++ b/Bidir.agda @@ -4,7 +4,9 @@ open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Maybe using (Maybe ; nothing ; just ; maybe′) open import Data.List using (List ; [] ; _∷_ ; map ; length) -open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec) +open import Data.List.Properties using () renaming (map-compose to map-∘) +open import Data.Vec using (toList ; fromList ; tabulate) renaming (lookup to lookupVec ; _∷_ to _∷V_) +open import Data.Vec.Properties using (tabulate-∘) open import Function using (id ; _∘_ ; flip) open import Relation.Nullary using (Dec ; yes ; no) open import Relation.Nullary.Negation using (contradiction) @@ -96,9 +98,12 @@ lemma-2 eq (i ∷ is) (x ∷ xs) h p | just h' | Reveal_is_.[_] ir = begin enumerate : {A : Set} → (l : List A) → List (Fin (length l)) enumerate l = toList (tabulate id) +denumerate : {A : Set} (l : List A) → Fin (length l) → A +denumerate l = flip lookupVec (fromList l) + bff : ({A : Set} → List A → List A) → ({B : Set} → EqInst B → List B → List B → Maybe (List B)) bff get eq s v = let s′ = enumerate s - g = fromFunc (λ f → lookupVec f (fromList s)) + g = fromFunc (denumerate s) h = assoc eq (get s′) v h′ = fmap (flip union g) h in fmap (flip map s′ ∘ flip lookup) h′ @@ -106,5 +111,24 @@ bff get eq s v = let s′ = enumerate s postulate free-theorem-list-list : {β γ : Set} → (get : {α : Set} → List α → List α) → (f : β → γ) → (l : List β) → get (map f l) ≡ map f (get l) +toList-map-commutes : {A B : Set} {n : ℕ} → (f : A → B) → (v : Data.Vec.Vec A n) → (toList (Data.Vec.map f v)) ≡ map f (toList v) +toList-map-commutes f Data.Vec.[] = refl +toList-map-commutes f (x ∷V xs) = cong (_∷_ (f x)) (toList-map-commutes f xs) + +lemma-map-denumerate-enumerate : {A : Set} → (as : List A) → map (denumerate as) (enumerate as) ≡ as +lemma-map-denumerate-enumerate [] = refl +lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin + map (flip lookupVec (a ∷V (fromList as))) (toList (tabulate Fin.suc)) + ≡⟨ cong (map (flip lookupVec (a ∷V (fromList as))) ∘ toList) (tabulate-∘ Fin.suc id) ⟩ + map (flip lookupVec (a ∷V (fromList as))) (toList (Data.Vec.map Fin.suc (tabulate id))) + ≡⟨ cong (map (flip lookupVec (a ∷V fromList as))) (toList-map-commutes Data.Fin.suc (tabulate id)) ⟩ + map (flip lookupVec (a ∷V fromList as)) (map Fin.suc (enumerate as)) + ≡⟨ sym (map-∘ (enumerate as)) ⟩ + map (flip lookupVec (a ∷V (fromList as)) ∘ Fin.suc) (enumerate as) + ≡⟨ refl ⟩ + map (denumerate as) (enumerate as) + ≡⟨ lemma-map-denumerate-enumerate as ⟩ + as ∎) + theorem-1 : (get : {α : Set} → List α → List α) → {τ : Set} → (eq : EqInst τ) → (s : List τ) → bff get eq s (get s) ≡ just s theorem-1 get eq s = {!!} -- 2.20.1