Merge branch feature-omit-sequence into master
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)
Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.

BFF.agda
BFFPlug.agda
Bidir.agda
Precond.agda

index 6943f0d..9fc0afe 100644 (file)
--- a/BFF.agda
+++ b/BFF.agda
@@ -14,7 +14,7 @@ open import Function using (id ; _∘_ ; flip)
 open import Relation.Binary using (Setoid ; DecSetoid ; module DecSetoid)
 
 open import FinMap
-open import Generic using (mapMV ; ≡-to-Π)
+open import Generic using (sequenceV ; ≡-to-Π)
 import CheckInsert
 open import GetTypes using (VecVec-to-PartialVecVec)
 
@@ -36,7 +36,7 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier
   denumerate = flip lookupV
 
-  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
+  bff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G j))
   bff G i s v = let s′ = enumerate s
                     t′ = Get.get G s′
                     g  = fromFunc (denumerate s)
@@ -44,7 +44,10 @@ module PartialVecBFF (A : DecSetoid ℓ₀ ℓ₀) where
                     t  = enumeratel (Get.|gl₁| G i)
                     h  = assoc (Get.get G t) v
                     h′ = (flip union (reshape g′ (Get.|gl₁| G i))) <$> h
-                in h′ >>= flip mapMV t ∘ flip lookupM
+                in (flip mapV t ∘ flip lookupM) <$> h′
+
+  sbff : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G j) → Maybe (Vec Carrier (Get.|gl₁| G j))
+  sbff G j s v = bff G j s v >>= sequenceV
 
 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
   open GetTypes.VecVec public using (Get)
@@ -53,5 +56,8 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where
 
   open PartialVecBFF A public using (assoc ; enumerate ; denumerate)
 
-  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
+  bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec (Maybe Carrier) m)
   bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G)
+
+  sbff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m)
+  sbff G = PartialVecBFF.sbff A (VecVec-to-PartialVecVec G)
index 9f45db1..12ee980 100644 (file)
@@ -13,8 +13,10 @@ open import Relation.Nullary using (yes ; no)
 open import Function using (flip ; id ; _∘_)
 open import Function.Equality using (_⟶_ ; _⟨$⟩_)
 open import Function.LeftInverse using (_RightInverseOf_)
+import Category.Monad
+open Category.Monad.RawMonad {ℓ₀} Data.Maybe.monad using (_>>=_)
 
-open import Generic using (≡-to-Π)
+open import Generic using (sequenceV ; ≡-to-Π)
 import BFF
 import GetTypes
 import Examples
@@ -24,9 +26,9 @@ open GetTypes.PartialVecVec public using (Get)
 open BFF.PartialVecBFF A public
 
 bffsameshape : (G : Get) → {i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))
-bffsameshape G {i} = bff G i
+bffsameshape G {i} = sbff G i
 
-bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec Carrier (Get.|gl₁| G j))
+bffplug : (G : Get) → (Get.|I| G → ℕ → Maybe (Get.|I| G)) → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (∃ λ j → Vec (Maybe Carrier) (Get.|gl₁| G j))
 bffplug G sput {i} {m} s v with sput i m
 ...                        | nothing = nothing
 ...                        | just j with Get.|gl₂| G j ≟ m
@@ -38,16 +40,16 @@ bffplug G sput {i}     s v | just j | yes refl with bff G j s v
 _SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set
 f SimpleRightInvOf g = ≡-to-Π f RightInverseOf ≡-to-Π g
 
-bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec Carrier (Get.|gl₁| G (nelteg ⟨$⟩ m)))
+bffinv : (G : Get) → (nelteg : PropEq ℕ ⟶ Get.I G) → nelteg RightInverseOf Get.gl₂ G → {i : Get.|I| G} → {m : ℕ} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (Get.|gl₁| G (nelteg ⟨$⟩ m)))
 bffinv G nelteg inv {m = m} s v = bff G (nelteg ⟨$⟩ m) s (subst (Vec Carrier) (sym (inv m)) v)
 
 module InvExamples where
   open Examples using (reverse' ; drop' ; sieve' ; tail' ; take')
   
   reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m)
-  reverse-put = bffinv reverse' (≡-to-Π id) (λ _ → refl)
+  reverse-put s v = bffinv reverse' (≡-to-Π id) (λ _ → refl) s v >>= sequenceV
 
-  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec Carrier (k + m))
+  drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier (k + n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (k + m))
   drop-put k = bffinv (drop' k) (≡-to-Π id) (λ _ → refl)
 
   double : ℕ → ℕ
@@ -59,10 +61,10 @@ module InvExamples where
   sieve-inv-len (suc zero)    = refl
   sieve-inv-len (suc (suc x)) = cong (suc ∘ suc) (sieve-inv-len x)
 
-  sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (double m))
+  sieve-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec (Maybe Carrier) (double m))
   sieve-put = bffinv sieve' (≡-to-Π double) sieve-inv-len
 
-  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec Carrier (suc m))
+  tail-put : {n m : ℕ} → Vec Carrier (suc n) → Vec Carrier m → Maybe (Vec (Maybe Carrier) (suc m))
   tail-put = bffinv tail' (≡-to-Π id) (λ _ → refl)
 
   take-put : (k : ℕ) → {n : ℕ}  → Vec Carrier (k + n) → Vec Carrier k → Maybe (Vec Carrier (k + n))
index 4d6524e..c9227e9 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 ; VecISetoid)
+open import Generic using (mapMV ; mapMV-cong ; mapMV-purity ; sequenceV ; VecISetoid ; just-injective)
 open import FinMap
 import CheckInsert
 open CheckInsert A
@@ -123,7 +123,7 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin
   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 s
+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)) ⟩
@@ -141,17 +141,17 @@ theorem-1 G {i} s = begin
     ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩
   (h′↦r ∘ just) (fromFunc (denumerate s))
     ≡⟨ refl ⟩
-  mapMV (flip lookupM (fromFunc (denumerate s))) (enumerate s)
-    ≡⟨ mapMV-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s) ⟩
-  mapMV (Maybe.just ∘ denumerate s) (enumerate s)
-    ≡⟨ mapMV-purity (denumerate s) (enumerate s) ⟩
-  just (map (denumerate s) (enumerate s))
-    ≡⟨ cong just (lemma-map-denumerate-enumerate s) ⟩
-  just s ∎
+  just (map (flip lookupM (fromFunc (denumerate s))) (enumerate s))
+    ≡⟨ cong just (map-cong (lemma-lookupM-fromFunc (denumerate s)) (enumerate s)) ⟩
+  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) ⟩
+  just (map just s) ∎
     where open ≡-Reasoning
           open Get G
           h↦h′ = _<$>_ (flip union (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G i)))
-          h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM)
+          h′↦r = _<$>_ (flip map (enumerate s) ∘ flip lookupM)
 
 
 lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a
@@ -211,32 +211,41 @@ sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong
 sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 sequence-cong {S}                                       (VecEq._∷-cong_ nothing xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _))
 
-theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
-theorem-2 G j s v u p with (lemma->>=-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
+theorem-2 : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec (Maybe Carrier) (Get.|gl₁| G j)) → bff G j s v ≡ just u → VecISetoid (MaybeSetoid A.setoid) at _ ∋ Get.get G u ≈ map just v
+theorem-2 G j s v u p with (lemma-<$>-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) (Get.|gl₁| G j))) <$> (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v)) p)
 theorem-2 G j s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v) ph′)
-theorem-2 G j s v u p | h′ , ph′ | h , ph = drop-just (begin
-  get <$> (just u)
-    ≡⟨ cong (_<$>_ get) (sym p) ⟩
-  get <$> (bff G j s v)
-    ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩
-  get <$> h′↦r (h↦h′ h)
+theorem-2 G j s v u p | h′ , ph′ | h , ph = begin⟨ VecISetoid (MaybeSetoid A.setoid) at _ ⟩
+  get u
+    ≡⟨ just-injective (trans (cong (_<$>_ get) (sym p))
+                             (cong (_<$>_ get ∘ _<$>_ h′↦r ∘ _<$>_ h↦h′) ph)) ⟩
+  get (h′↦r (h↦h′ h))
     ≡⟨ refl ⟩
-  get <$> sequenceV (map (flip lookupM (h↦h′ h)) t)
-    ≡⟨ lemma-get-sequenceV G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩
-  sequenceV (get (map (flip lookupM (h↦h′ h)) t))
-    ≡⟨ cong sequenceV (free-theorem (flip lookupM (h↦h′ h)) t) ⟩
-  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))
-    ≈⟨ sequence-cong (lemma-2 (get t) v h ph) ⟩
-  sequenceV (map just v)
-    ≡⟨ lemma-just-sequence v ⟩
-  just v ∎)
-    where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
+  get (map (flip lookupM (h↦h′ h)) t)
+    ≡⟨ free-theorem (flip lookupM (h↦h′ h)) t ⟩
+  map (flip lookupM (h↦h′ h)) (get t)
+    ≡⟨ lemma-union-not-used h g′ (get t) (lemma-assoc-domain (get t) v h ph) ⟩
+  map (flip lookupM h) (get t)
+    ≈⟨ lemma-2 (get t) v h ph ⟩
+  map just v ∎
+    where open SetoidReasoning
           open Get G
           s′   = enumerate s
           g    = fromFunc (denumerate s)
           g′   = delete-many (get s′) g
           t    = enumeratel (Get.|gl₁| G j)
           h↦h′ = flip union (reshape g′ (Get.|gl₁| G j))
-          h′↦r = flip mapMV t ∘ flip lookupM
+          h′↦r = flip map t ∘ flip lookupM
+
+theorem-2′ : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → (u : Vec Carrier (Get.|gl₁| G j)) → bff G j s v ≡ just (map just u) → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v
+theorem-2′ G j s v u p = drop-just (begin
+  get <$> just u
+    ≡⟨ cong (_<$>_ get) (sym (lemma-just-sequence u)) ⟩
+  get <$> sequenceV (map just u)
+    ≡⟨ lemma-get-sequenceV G (lemma-just-sequence u) ⟩
+  sequenceV (get (map just u))
+    ≈⟨ sequence-cong (theorem-2 G j s v (map just u) p) ⟩
+  sequenceV (map just v)
+    ≡⟨ lemma-just-sequence v ⟩
+  just v ∎)
+  where open EqR (MaybeSetoid (VecISetoid A.setoid at _))
+        open Get G
index 3a48757..ead2e18 100644 (file)
@@ -25,13 +25,12 @@ 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)
 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)
 import BFF
 import Bidir
-open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence)
+open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain)
 import GetTypes
 open GetTypes.PartialVecVec using (Get ; module Get)
 open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff ; enumeratel)
@@ -63,23 +62,26 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} (Data.List.A
           maybe′ just (lookupM i (delete-many is (fromFunc g))) (lookup i h) ∎
         inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (fromFunc g)) f≢i)
 
-assoc-enough : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G i s v ≡ just u
-assoc-enough G {i} s v (h , p) = _ , (begin
+assoc-enough : (G : Get) → {i : Get.|I| G} → (j : Get.|I| G) → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G j)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G j))) v ≡ just h) → ∃ λ u → bff G j s v ≡ just u
+assoc-enough G {i} j s v (h , p) = _ , cong (_<$>_ (flip map t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ (|gl₁| j)))) p
+  where open Get G
+        g′ = delete-many (get (enumerate s)) (fromFunc (denumerate s))
+        t  = enumeratel (|gl₁| j)
+
+assoc-enough′ : (G : Get) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → (v : Vec Carrier (Get.|gl₂| G i)) → ∃ (λ h → assoc (Get.get G (enumeratel (Get.|gl₁| G i))) v ≡ just h) → ∃ λ u → bff G i s v ≡ just (map just u)
+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
-    ≡⟨ 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)
-    ≡⟨ cong (sequenceV ∘ flip map t ∘ flip lookupM) (proj₂ wp) ⟩
-  sequenceV (map (flip lookupM (fromFunc (proj₁ wp))) t)
-    ≡⟨ cong sequenceV (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t) ⟩
-  sequenceV (map (Maybe.just ∘ proj₁ wp) t)
-    ≡⟨ cong sequenceV (map-∘ just (proj₁ wp) t) ⟩
-  sequenceV (map Maybe.just (map (proj₁ wp) t))
-    ≡⟨ lemma-just-sequence (map (proj₁ wp) t) ⟩
-  just (map (proj₁ wp) t) ∎)
+    ≡⟨ proj₂ (assoc-enough G i s v (h , p)) ⟩
+  just (map (flip lookupM (union h (reshape g′ (|gl₁| i)))) t)
+    ≡⟨ cong just (begin _
+        ≡⟨ cong (flip map t ∘ flip lookupM ∘ union h) (lemma-reshape-id g′) ⟩
+      map (flip lookupM (union h g′)) t
+        ≡⟨ cong (flip map t ∘ flip lookupM) (proj₂ wp) ⟩
+      map (flip lookupM (fromFunc (proj₁ wp))) t
+        ≡⟨ map-cong (lemma-lookupM-fromFunc (proj₁ wp)) t ⟩
+      map (Maybe.just ∘ proj₁ wp) t
+        ≡⟨ map-∘ just (proj₁ wp) t ⟩
+      map Maybe.just (map (proj₁ wp) t) ∎) ⟩ _ ∎)
   where open Get G
         s′ = enumerate s
         g  = fromFunc (denumerate s)