diff options
| -rw-r--r-- | BFF.agda | 14 | ||||
| -rw-r--r-- | BFFPlug.agda | 66 | ||||
| -rw-r--r-- | Bidir.agda | 65 | ||||
| -rw-r--r-- | Everything.agda | 1 | ||||
| -rw-r--r-- | FinMap.agda | 9 | ||||
| -rw-r--r-- | Precond.agda | 39 |
6 files changed, 140 insertions, 54 deletions
@@ -30,14 +30,18 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where enumerate : {n : ℕ} → Vec Carrier n → Vec (Fin n) n enumerate _ = tabulate id + enumeratel : (n : ℕ) → Vec (Fin n) n + enumeratel _ = tabulate id + denumerate : {n : ℕ} → Vec Carrier n → Fin n → Carrier denumerate = flip lookupV - bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) - bff G s v = let s′ = enumerate s + bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m) + bff G m s v = let s′ = enumerate s t′ = Get.get G s′ g = fromFunc (denumerate s) g′ = delete-many t′ g - h = assoc t′ v - h′ = (flip union g′) <$> h - in h′ >>= flip mapMV s′ ∘ flip lookupM + t = enumeratel m + h = assoc (Get.get G t) v + h′ = (flip union (reshape g′ m)) <$> h + in h′ >>= flip mapMV t ∘ flip lookupM diff --git a/BFFPlug.agda b/BFFPlug.agda new file mode 100644 index 0000000..1d5570c --- /dev/null +++ b/BFFPlug.agda @@ -0,0 +1,66 @@ +open import Level using () renaming (zero to ℓ₀) +open import Relation.Binary using (DecSetoid) + +module BFFPlug (A : DecSetoid ℓ₀ ℓ₀) where + +open import Data.Nat using (ℕ ; _≟_ ; _+_ ; _∸_ ; zero ; suc ; ⌈_/2⌉) +open import Data.Nat.Properties using (m+n∸n≡m) +open import Data.Maybe using (Maybe ; just ; nothing) +open import Data.Vec using (Vec) +open import Data.Product using (∃ ; _,_) +open import Relation.Binary using (module DecSetoid) +open import Relation.Binary.PropositionalEquality using (refl ; cong ; subst ; sym ; module ≡-Reasoning) renaming (setoid to PropEq) +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 BFF +import GetTypes +import Examples + +open DecSetoid A using (Carrier) +open GetTypes.VecVec public using (Get) +open BFF.VecBFF A public + +bffsameshape : (G : Get) → {n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n) +bffsameshape G {n} = bff G n + +bffplug : (G : Get) → (ℕ → ℕ → Maybe ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (∃ λ l → Vec Carrier l) +bffplug G sput {n} {m} s v with sput n m +... | nothing = nothing +... | just l with Get.getlen G l ≟ m +... | no getlenl≢m = nothing +bffplug G sput {n} s v | just l | yes refl with bff G l s v +... | nothing = nothing +... | just s′ = just (l , s′) + +as-Π : {A B : Set} → (f : A → B) → PropEq A ⟶ PropEq B +as-Π f = record { _⟨$⟩_ = f; cong = cong f } + +_SimpleRightInvOf_ : (ℕ → ℕ) → (ℕ → ℕ) → Set +f SimpleRightInvOf g = as-Π f RightInverseOf as-Π g + +bffinv : (G : Get) → (nelteg : ℕ → ℕ) → nelteg SimpleRightInvOf Get.getlen G → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (nelteg m)) +bffinv G nelteg inv {n} {m} s v = bff G (nelteg m) s (subst (Vec Carrier) (sym (inv m)) v) + +module InvExamples where + open Examples using (reverse' ; drop' ; sieve') + + reverse-put : {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier m) + reverse-put = bffinv reverse' id (λ _ → refl) + + drop-put : (k : ℕ) → {n m : ℕ} → Vec Carrier n → Vec Carrier m → Maybe (Vec Carrier (m + k)) + drop-put k = bffinv (drop' k) (flip _+_ k) (flip m+n∸n≡m k) + + double : ℕ → ℕ + double zero = zero + double (suc n) = suc (suc (double n)) + + sieve-inv-len : double SimpleRightInvOf ⌈_/2⌉ + sieve-inv-len zero = refl + 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 = bffinv sieve' double sieve-inv-len @@ -31,7 +31,7 @@ open import FinMap import CheckInsert open CheckInsert A import BFF -open BFF.VecBFF A using (assoc ; enumerate ; denumerate ; bff) +open BFF.VecBFF A using (assoc ; enumerate ; enumeratel ; denumerate ; bff) open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) @@ -125,18 +125,20 @@ lemma-map-denumerate-enumerate (a ∷ as) = cong (_∷_ a) (begin as ∎) where open ≡-Reasoning -theorem-1 : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → bff G s (Get.get G s) ≡ just s -theorem-1 G s = begin - bff G s (get s) - ≡⟨ cong (bff G s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ - bff G s (get (map (denumerate s) (enumerate s))) - ≡⟨ cong (bff G s) (free-theorem (denumerate s) (enumerate s)) ⟩ - bff G s (map (denumerate s) (get (enumerate s))) +theorem-1 : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → bff G m s (Get.get G s) ≡ just s +theorem-1 G {m} s = begin + bff G m s (get s) + ≡⟨ cong (bff G m s ∘ get) (sym (lemma-map-denumerate-enumerate s)) ⟩ + bff G m s (get (map (denumerate s) (enumerate s))) + ≡⟨ cong (bff G m s) (free-theorem (denumerate s) (enumerate s)) ⟩ + bff G m s (map (denumerate s) (get (enumerate s))) ≡⟨ refl ⟩ (h′↦r ∘ h↦h′) (assoc (get (enumerate s)) (map (denumerate s) (get (enumerate s)))) ≡⟨ cong (h′↦r ∘ h↦h′) (lemma-1 (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ h↦h′ ∘ just) (restrict (denumerate s) (toList (get (enumerate s)))) ≡⟨ refl ⟩ + (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) m)) + ≡⟨ cong (h′↦r ∘ Maybe.just ∘ union (restrict (denumerate s) (toList (get (enumerate s))))) (lemma-reshape-id (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) ⟩ (h′↦r ∘ just) (union (restrict (denumerate s) (toList (get (enumerate s)))) (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) ≡⟨ cong (h′↦r ∘ just) (lemma-disjoint-union (denumerate s) (get (enumerate s))) ⟩ (h′↦r ∘ just) (fromFunc (denumerate s)) @@ -150,7 +152,7 @@ theorem-1 G s = begin just s ∎ where open ≡-Reasoning open Get G - h↦h′ = _<$>_ (flip union (delete-many (get (enumerate s)) (fromFunc (denumerate s)))) + h↦h′ = _<$>_ (flip union (reshape (delete-many (get (enumerate s)) (fromFunc (denumerate s))) m)) h′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupM) @@ -158,14 +160,14 @@ lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma lemma-<$>-just (just x) f<$>ma≡just-b = x , refl lemma-<$>-just nothing () -lemma-union-not-used : {m n : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMapMaybe n A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map (flip lookupM (union h h')) is ≡ map (flip lookupM h) is -lemma-union-not-used h h' [] p = refl -lemma-union-not-used h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin - lookupM i (union h h') - ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j h') (lookupM j h)) i ⟩ - maybe′ just (lookupM i h') (lookupM i h) - ≡⟨ cong (maybe′ just (lookupM i h')) px ⟩ - maybe′ just (lookupM i h') (just x) +lemma-union-not-used : {m n n' : ℕ} {A : Set} (h : FinMapMaybe n A) → (h' : FinMapMaybe n' A) → (is : Vec (Fin n) m) → (toList is) in-domain-of h → map (flip lookupM (union h (reshape h' n))) is ≡ map (flip lookupM h) is +lemma-union-not-used h h' [] p = refl +lemma-union-not-used {n = n} h h' (i ∷ is') (Data.List.All._∷_ (x , px) p') = cong₂ _∷_ (begin + lookupM i (union h (reshape h' n)) + ≡⟨ lookup∘tabulate (λ j → maybe′ just (lookupM j (reshape h' n)) (lookupM j h)) i ⟩ + maybe′ just (lookupM i (reshape h' n)) (lookupM i h) + ≡⟨ cong (maybe′ just (lookupM i (reshape h' n))) px ⟩ + maybe′ just (lookupM i (reshape h' n)) (just x) ≡⟨ sym px ⟩ lookupM i h ∎) (lemma-union-not-used h h' is' p') @@ -220,22 +222,22 @@ 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) → {m : ℕ} → (v : Vec Carrier (Get.getlen G m)) → (s u : Vec Carrier m) → bff G s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v -theorem-2 G v s u p with (lemma->>=-just ((flip union (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s)))) <$> (assoc (Get.get G (enumerate s)) v)) p) -theorem-2 G v s u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumerate s)) v) ph′) -theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ +theorem-2 : (G : Get) → {m : ℕ} → (n : ℕ) → (s : Vec Carrier m) → (v : Vec Carrier (Get.getlen G n)) → (u : Vec Carrier n) → bff G n s v ≡ just u → VecISetoid A.setoid at _ ∋ Get.get G u ≈ v +theorem-2 G n s v u p with (lemma->>=-just ((flip union (reshape (delete-many (Get.get G (enumerate s)) (fromFunc (denumerate s))) n)) <$> (assoc (Get.get G (enumeratel n)) v)) p) +theorem-2 G n s v u p | h′ , ph′ with (lemma-<$>-just (assoc (Get.get G (enumeratel n)) v) ph′) +theorem-2 G n s v u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ get <$> (just u) ≡⟨ cong (_<$>_ get) (sym p) ⟩ - get <$> (bff G s v) + get <$> (bff G n s v) ≡⟨ cong (_<$>_ get ∘ flip _>>=_ h′↦r ∘ _<$>_ h↦h′) ph ⟩ - get <$> mapMV (flip lookupM (h↦h′ h)) s′ + get <$> mapMV (flip lookupM (h↦h′ h)) t ≡⟨ lemma-get-mapMV (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) G ⟩ - mapMV (flip lookupM (h↦h′ h)) (get s′) - ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get s′)) ⟩ - sequenceV (map (flip lookupM (h↦h′ h)) (get s′)) - ≡⟨ cong sequenceV (lemma-union-not-used h g′ (get s′) (lemma-assoc-domain (get s′) v h ph)) ⟩ - sequenceV (map (flip lookupM h) (get s′)) - ≈⟨ sequence-cong (lemma-2 (get s′) v h ph) ⟩ + mapMV (flip lookupM (h↦h′ h)) (get t) + ≡⟨ sym (sequence-map (flip lookupM (h↦h′ h)) (get 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 ∎) @@ -244,5 +246,6 @@ theorem-2 G v s u p | h′ , ph′ | h , ph = drop-just (begin⟨ MaybeSetoid (V s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g - h↦h′ = flip union g′ - h′↦r = flip mapMV s′ ∘ flip lookupM + t = enumeratel n + h↦h′ = flip union (reshape g′ n) + h′↦r = flip mapMV (enumeratel n) ∘ flip lookupM diff --git a/Everything.agda b/Everything.agda index e1734a9..e37c76e 100644 --- a/Everything.agda +++ b/Everything.agda @@ -11,3 +11,4 @@ import Bidir import LiftGet import Precond import Examples +import BFFPlug diff --git a/FinMap.agda b/FinMap.agda index c46e637..240bbe1 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -40,6 +40,11 @@ fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) fromFunc : {A : Set} {n : ℕ} → (Fin n → A) → FinMapMaybe n A fromFunc = mapV just ∘ tabulate +reshape : {n : ℕ} {A : Set} → FinMapMaybe n A → (l : ℕ) → FinMapMaybe l A +reshape m zero = [] +reshape [] (suc l) = nothing ∷ (reshape [] l) +reshape (x ∷ xs) (suc l) = x ∷ (reshape xs l) + union : {A : Set} {n : ℕ} → FinMapMaybe n A → FinMapMaybe n A → FinMapMaybe n A union m1 m2 = tabulate (λ f → maybe′ just (lookupM f m2) (lookupM f m1)) @@ -108,6 +113,10 @@ lemma-lookupM-delete {i = zero} {j = suc j} (_ ∷ _) p = refl lemma-lookupM-delete {i = suc i} {j = zero} (x ∷ xs) p = refl lemma-lookupM-delete {i = suc i} {j = suc j} (x ∷ xs) p = lemma-lookupM-delete xs (p ∘ cong suc) +lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n ≡ m +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)) 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) diff --git a/Precond.agda b/Precond.agda index 354e5f1..9dd077e 100644 --- a/Precond.agda +++ b/Precond.agda @@ -25,7 +25,7 @@ open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨ open import Relation.Nullary using (yes ; no) open import Generic using (mapMV ; sequenceV ; sequence-map) -open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; lemma-lookupM-empty ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc) +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 @@ -33,7 +33,7 @@ import Bidir open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) import GetTypes open GetTypes.VecVec using (Get ; module Get) -open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) +open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff ; enumeratel) 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 @@ -67,26 +67,29 @@ 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) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (Get.getlen G m)) → ∃ (λ h → assoc (Get.get G (enumerate s)) v ≡ just h) → ∃ λ u → bff G s v ≡ just u -assoc-enough G s v (h , p) = _ , (begin - bff G s v - ≡⟨ cong (flip _>>=_ (flip mapMV s′ ∘ flip lookupM) ∘ _<$>_ (flip union g′)) p ⟩ - mapMV (flip lookupM (union h g′)) s′ - ≡⟨ sym (sequence-map (flip lookupM (union h g′)) s′) ⟩ - sequenceV (map (flip lookupM (union h g′)) s′) - ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) (proj₂ wp) ⟩ - sequenceV (map (flip lookupM (fromFunc (proj₁ wp))) s′) - ≡⟨ cong sequenceV (map-cong (lemma-lookupM-fromFunc (proj₁ wp)) s′) ⟩ - sequenceV (map (Maybe.just ∘ proj₁ wp) s′) - ≡⟨ cong sequenceV (map-∘ just (proj₁ wp) s′) ⟩ - sequenceV (map Maybe.just (map (proj₁ wp) s′)) - ≡⟨ lemma-just-sequence (map (proj₁ wp) s′) ⟩ - just (map (proj₁ wp) s′) ∎) +assoc-enough : (G : Get) → {m : ℕ} → (s : Vec Carrier m) → (v : Vec Carrier (Get.getlen G m)) → ∃ (λ h → assoc (Get.get G (enumeratel m)) v ≡ just h) → ∃ λ u → bff G m s v ≡ just u +assoc-enough G {m} s v (h , p) = _ , (begin + bff G m s v + ≡⟨ cong (flip _>>=_ (flip mapMV t ∘ flip lookupM) ∘ _<$>_ (flip union (reshape g′ m))) p ⟩ + mapMV (flip lookupM (union h (reshape g′ m))) t + ≡⟨ sym (sequence-map (flip lookupM (union h (reshape g′ m))) t) ⟩ + sequenceV (map (flip lookupM (union h (reshape g′ m))) 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) ∎) where open Get G s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g - wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) + t = enumeratel m + wp = lemma-union-delete-fromFunc (lemma-assoc-domain (get t) v h p) data All-different {A : Set} : List A → Set where different-[] : All-different [] |