define mapMV via sequenceV
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)
This makes a few proofs easier and eliminates the need for sequence-map
entirely.

Bidir.agda
Generic.agda
Precond.agda

index 96ba6cf..2231447 100644 (file)
@@ -26,7 +26,7 @@ import Relation.Binary.EqReasoning as EqR
 
 import GetTypes
 open GetTypes.PartialVecVec using (Get ; module Get)
-open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; sequence-map ; VecISetoid)
+open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid)
 open import FinMap
 import CheckInsert
 open CheckInsert A
@@ -189,7 +189,7 @@ lemma-mapM-successful         (x ∷ xs) p  | just y | just ys | [ p′ ] = map-
 lemma-get-mapMV : {A B : Set} {f : A → Maybe B} → (G : Get) → {i : Get.|I| G} {v : Vec A (Get.|gl₁| G i)} {r : Vec B (Get.|gl₁| G i)} → mapMV f v ≡ just r → Get.get G <$> mapMV f v ≡ mapMV f (Get.get G v)
 lemma-get-mapMV {f = f} G {v = v} p = begin
   get <$> mapMV f v
-    ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩
+    ≡⟨ refl ⟩
   get <$> sequenceV (map f v)
     ≡⟨ cong (_<$>_ get ∘ sequenceV) (proj₂ wp) ⟩
   get <$> sequenceV (map just (proj₁ wp))
@@ -203,7 +203,7 @@ lemma-get-mapMV {f = f} G {v = v} p = begin
   sequenceV (get (map f v))
     ≡⟨ cong sequenceV (free-theorem f v) ⟩
   sequenceV (map f (get v))
-    ≡⟨ sequence-map f (get v) ⟩
+    ≡⟨ refl ⟩
   mapMV f (get v) ∎
   where open ≡-Reasoning
         open Get G
@@ -229,7 +229,7 @@ theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid
   get <$> h′↦r (h↦h′ h)
     ≡⟨ lemma-get-mapMV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
   mapMV (flip lookupM (h↦h′ h)) (get t)
-    ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get t)) ⟩
+    ≡⟨ refl ⟩
   sequenceV (map (flip lookupM (h↦h′ h)) (get t))
     ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph)) ⟩
   sequenceV (map (flip lookupM h) (get t))
index c458483..9f1172d 100644 (file)
@@ -8,6 +8,7 @@ open import Data.Nat using (ℕ ; zero ; suc)
 open import Data.Product using (__ ; _,_)
 open import Data.Vec using (Vec ; toList ; fromList ; map) renaming ([] to []V ; _∷_ to _∷V_)
 open import Data.Vec.Equality using () renaming (module Equality to VecEq)
+open import Data.Vec.Properties using (map-cong)
 open import Function using (_∘_ ; id ; flip)
 open import Function.Equality using (_⟶_)
 open import Level using () renaming (zero to ℓ₀)
@@ -30,13 +31,15 @@ length-replicate : {A : Set} {a : A} → (n : ℕ) → length (replicate n a) 
 length-replicate zero    = refl
 length-replicate (suc n) = cong suc (length-replicate n)
 
+sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
+sequenceV []V       = just []V
+sequenceV (x ∷V xs) = x >>= (λ y → (_∷V_ y) <$> sequenceV xs)
+
 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))
+mapMV f = sequenceV ∘ map f
 
 mapMV-cong : {A B : Set} {f g : A → Maybe B} → f ≗ g → {n : ℕ} → mapMV {n = n} f ≗ mapMV g
-mapMV-cong f≗g []V       = refl
-mapMV-cong f≗g (x ∷V xs) = cong₂ _>>=_ (f≗g x) (cong (flip (_<$>_ ∘ _∷V_)) (mapMV-cong f≗g xs))
+mapMV-cong f≗g v = cong sequenceV (map-cong f≗g v)
 
 mapMV-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (Maybe.just ∘ f) v ≡ just (map f v)
 mapMV-purity f []V       = refl
@@ -50,15 +53,6 @@ maybeEq-to-≡ : {A : Set} {a b : Maybe A} → MaybeEq (EqSetoid A) ∋ a ≈ b
 maybeEq-to-≡ (just refl) = refl
 maybeEq-to-≡ nothing     = refl
 
-sequenceV : {A : Set} {n : ℕ} → Vec (Maybe A) n → Maybe (Vec A n)
-sequenceV = mapMV id
-
-sequence-map : {A B : Set} {n : ℕ} → (f : A → Maybe B) → sequenceV {n = n} ∘ map f ≗ mapMV f
-sequence-map f []V = refl
-sequence-map f (x ∷V xs) with f x
-sequence-map f (x ∷V xs) | just y = cong (_<$>_ (_∷V_ y)) (sequence-map f xs)
-sequence-map f (x ∷V xs) | nothing = refl
-
 subst-cong : {A : Set} → (T : A → Set) → {g : A → A} → {a b : A} → (f : {c : A} → T c → T (g c)) → (p : a ≡ b) →
              f ∘ subst T p ≗ subst T (cong g p) ∘ f
 subst-cong T f refl _ = refl
index bc619dc..3e4c219 100644 (file)
@@ -25,7 +25,7 @@ open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ;
 open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎)
 open import Relation.Nullary using (yes ; no)
 
-open import Generic using (mapMV ; sequenceV ; sequence-map)
+open import Generic using (mapMV ; sequenceV)
 open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id)
 import CheckInsert
 open CheckInsert (decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other)
@@ -73,7 +73,7 @@ assoc-enough G {i} s v (h , p) = _ , (begin
   bff G i s v
     ≡⟨ cong (flip _>>=_ (flip mapMV t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (Get.|gl₁| G i)))) p ⟩
   mapMV (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t
-    ≡⟨ sym (sequence-map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t) ⟩
+    ≡⟨ refl ⟩
   sequenceV (map (flip lookupM (union h (reshape g′ (Get.|gl₁| G i)))) t)
     ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
   sequenceV (map (flip lookupM (union h g′)) t)