define fromFunc more conveniently
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 13:52:33 +0000 (14:52 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 13:52:33 +0000 (14:52 +0100)
FinMap.agda
Precond.agda

index fa13144..b2db8f4 100644 (file)
@@ -38,7 +38,7 @@ fromAscList []             = empty
 fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs)
 
 fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A
-fromFunc = mapV just ∘ tabulate
+fromFunc = tabulate ∘ _∘_ just
 
 reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A
 reshape m        zero    = []
@@ -103,10 +103,6 @@ lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip look
 lemma-lookupM-fromFunc f zero = refl
 lemma-lookupM-fromFunc f (suc i) = lemma-lookupM-fromFunc (f ∘ suc) i
 
-lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (Maybe.just ∘ f)
-lemma-fromFunc-tabulate {zero}  f = refl
-lemma-fromFunc-tabulate {suc _} f = cong (_∷_ (just (f zero))) (lemma-fromFunc-tabulate (f ∘ suc))
-
 lemma-lookupM-delete : {n : ℕ} {A : Set} {i j : Fin n} → (f : FinMapMaybe n A) → i ≢ j → lookupM i (delete j f) ≡ lookupM i f
 lemma-lookupM-delete {i = zero}  {j = zero}  (_ ∷ _)  p = contradiction refl p
 lemma-lookupM-delete {i = zero}  {j = suc j} (_ ∷ _)  p = refl
@@ -118,7 +114,7 @@ lemma-reshape-id []       = refl
 lemma-reshape-id (x ∷ xs) = cong (_∷_ x) (lemma-reshape-id xs)
 
 lemma-disjoint-union : {n m : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f (toList t)) (delete-many t (fromFunc f)) ≡ fromFunc f
-lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (sym (lemma-fromFunc-tabulate f))
+lemma-disjoint-union {n} {m} f t = lemma-tabulate-∘ (lemma-inner t)
     where lemma-inner : {m : ℕ} → (t : Vec (Fin n) m) → (x : Fin n) → maybe′ just (lookupM x (delete-many t (fromFunc f))) (lookupM x (restrict f (toList t))) ≡ just (f x)
           lemma-inner [] x = begin
             maybe′ just (lookupM x (fromFunc f)) (lookupM x empty)
index 3e4c219..3a48757 100644 (file)
@@ -41,23 +41,18 @@ lemma-maybe-just a (just x) = refl
 lemma-maybe-just a nothing = refl
 
 lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (fromFunc g)) ≡ fromFunc v
-lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
-  union h (fromFunc g)
-    ≡⟨ lemma-tabulate-∘ (λ f → begin
+lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∘ (λ f → begin
       maybe′ just (lookupM f (fromFunc g)) (lookupM f h)
         ≡⟨ cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩
       maybe′ just (just (g f)) (lookupM f h)
         ≡⟨ lemma-maybe-just (g f) (lookupM f h) ⟩
-      just (maybe′ id (g f) (lookupM f h)) ∎) ⟩
-  tabulate (λ f → just (maybe′ id (g f) (lookup f h)))
-    ≡⟨ tabulate-∘ just (λ f → maybe′ id (g f) (lookup f h)) ⟩
-  map just (tabulate (λ f → maybe′ id (g f) (lookup f h))) ∎)
+      just (maybe′ id (g f) (lookupM f h)) ∎))
 lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.All._∷_ (x , px) ps) = _ , (begin
   union h (delete i (delete-many is (fromFunc g)))
     ≡⟨ lemma-tabulate-∘ inner ⟩
   union h (delete-many is (fromFunc g))
     ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
-  map just _ ∎)
+  _ ∎)
   where inner : (f : Fin n) → maybe′ just (lookupM f (delete i (delete-many is (fromFunc g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (fromFunc g))) (lookup f h)
         inner f with f ≟ i
         inner .i | yes refl = begin