author Helmut Grohne Mon, 27 Jan 2014 08:31:56 +0000 (09:31 +0100) committer Helmut Grohne Mon, 27 Jan 2014 08:31:56 +0000 (09:31 +0100)
 Bidir.agda patch | blob | history Generic.agda patch | blob | history Precond.agda patch | blob | history

index eef8bff..05ee066 100644 (file)
@@ -22,7 +22,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨

import FreeTheorems
open FreeTheorems.VecVec using (get-type ; free-theorem)
-open import Generic using (just-injective ; map-just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
+open import Generic using (just-injective ; mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map)
open import FinMap
import CheckInsert
open CheckInsert Carrier deq
@@ -150,14 +150,6 @@ lemma->>=-just : {A B : Set} (ma : Maybe A) {f : A → Maybe B} {b : B} → (ma
lemma->>=-just (just a) p = a , refl
lemma->>=-just nothing  ()

-lemma-mapMV-just : {A B : Set} {n : ℕ} {f : A → Maybe B} {s : Vec A n} {v : Vec B n} → mapMV f s ≡ just v → All (λ x → ∃ λ y → f x ≡ just y) (toList s)
-lemma-mapMV-just         {s = []}     p = Data.List.All.[]
-lemma-mapMV-just {f = f} {s = x ∷ xs} p with f x | inspect f x
-lemma-mapMV-just         {s = x ∷ xs} () | nothing | _
-lemma-mapMV-just {f = f} {s = x ∷ xs} p  | just y  | [ py ] with mapMV f xs | inspect (mapMV f) xs
-lemma-mapMV-just         {s = x ∷ xs} () | just y  | [ py ] | nothing | _
-lemma-mapMV-just         {s = x ∷ xs} p  | just y  | [ py ] | just ys | [ pys ] = (y , py) Data.List.All.∷ (lemma-mapMV-just pys)
-
lemma-just-sequence : {A : Set} {n : ℕ} → (v : Vec A n) → sequenceV (map just v) ≡ just v
lemma-just-sequence [] = refl
lemma-just-sequence (x ∷ xs) rewrite lemma-just-sequence xs = refl
index 2ef374c..4e55c21 100644 (file)
@@ -15,10 +15,6 @@ open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ;
open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<\$>_)

-∷-injective : {A : Set} {n : ℕ} {x y : A} {xs ys : Vec A n} →
-              (x ∷V xs) ≡ (y ∷V ys) → x ≡ y × xs ≡ ys
-∷-injective refl = refl , refl
-
just-injective : {A : Set} → {x y : A} → Maybe.just x ≡ Maybe.just y → x ≡ y
just-injective refl = refl

@@ -26,12 +22,6 @@ length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a)
length-replicate zero    = refl
length-replicate (suc n) = cong suc (length-replicate n)

-map-just-injective : {A : Set} {n : ℕ} {xs ys : Vec A n} →
-                     map Maybe.just xs ≡ map Maybe.just ys → xs ≡ ys
-map-just-injective {xs = []V}      {ys = []V}       p  = refl
-map-just-injective {xs = x ∷V xs′} {ys = y ∷V ys′}  p with ∷-injective p
-map-just-injective {xs = x ∷V xs′} {ys = .x ∷V ys′} p | refl , p′ = cong (_∷V_ x) (map-just-injective p′)
-
mapMV : {A B : Set} {n : ℕ} → (A → Maybe B) → Vec A n → Maybe (Vec B n)
mapMV f []V = just []V
mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <\$> (mapMV f xs))
index 90027b4..6aba291 100644 (file)
@@ -18,7 +18,7 @@ import Data.List.All
open import Data.List.Any using (here ; there)
open Data.List.Any.Membership-≡ using (_∉_)
open import Data.Maybe using (just)
-open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂)
+open import Data.Product using (∃ ; _,_ ; proj₂)
open import Function using (flip ; _∘_ ; id)
open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym)
open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
@@ -37,9 +37,6 @@ lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup
lemma-lookup-map-just zero    (x ∷ xs) = refl
lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs

-fromMaybe : {A : Set} → A → Maybe A → A
-fromMaybe a ma = maybe′ id a ma
-
lemma-maybe-just : {A : Set} → (a : A) → (ma : Maybe A) → maybe′ Maybe.just (just a) ma ≡ Maybe.just (maybe′ id a ma)
lemma-maybe-just a (just x) = refl
lemma-maybe-just a nothing = refl
@@ -52,16 +49,13 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin
≡⟨ cong (flip (maybe′ just) (lookup f h)) (lemma-lookup-map-just f g) ⟩
maybe′ just (just (lookup f g)) (lookup f h)
≡⟨ lemma-maybe-just (lookup f g) (lookup f h) ⟩
-      just (fromMaybe (lookup f g) (lookup f h)) ∎) ⟩
-  tabulate (λ f → just (fromMaybe (lookup f g) (lookup f h)))
-    ≡⟨ tabulate-∘ just (λ f → fromMaybe (lookup f g) (lookup f h)) ⟩
-  map just (tabulate (λ f → fromMaybe (lookup f g) (lookup f h))) ∎)
-lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List.All.∷ ps) = _ , (begin
+      just (maybe′ id (lookup f g) (lookup f h)) ∎) ⟩
+  tabulate (λ f → just (maybe′ id (lookup f g) (lookup f h)))
+    ≡⟨ tabulate-∘ just (λ f → maybe′ id (lookup f g) (lookup f h)) ⟩
+  map just (tabulate (λ f → maybe′ id (lookup f g) (lookup f h))) ∎)
+lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Data.List.All.∷ ps) = _ , (begin
union h (delete i (delete-many is (map just g)))
-    ≡⟨ lemma-tabulate-∘ (λ f → (begin
-      maybe′ just (lookupM f (delete i (delete-many is (map just g)))) (lookup f h)
-        ≡⟨ inner f ⟩
-      maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) ∎)) ⟩
+    ≡⟨ lemma-tabulate-∘ inner ⟩
union h (delete-many is (map just g))
≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩
map just _ ∎)
@@ -69,9 +63,9 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (p Data.List
inner f with f ≟ i
inner .i | yes refl = begin
maybe′ just (lookupM i (delete i (delete-many is (map just g)))) (lookup i h)
-            ≡⟨ cong (maybe′ just _) (proj₂ p) ⟩
-          just (proj₁ p)
-            ≡⟨ cong (maybe′ just _) (sym (proj₂ p)) ⟩
+            ≡⟨ cong (maybe′ just _) px ⟩
+          just x
+            ≡⟨ cong (maybe′ just _) (sym px) ⟩
maybe′ just (lookupM i (delete-many is (map just g))) (lookup i h) ∎
inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just g)) f≢i)