diff options
| -rw-r--r-- | BFF.agda | 17 | ||||
| -rw-r--r-- | BFFPlug.agda | 66 | ||||
| -rw-r--r-- | Bidir.agda | 114 | ||||
| -rw-r--r-- | Everything.agda | 2 | ||||
| -rw-r--r-- | Examples.agda | 46 | ||||
| -rw-r--r-- | FinMap.agda | 22 | ||||
| -rw-r--r-- | Generic.agda | 18 | ||||
| -rw-r--r-- | Precond.agda | 81 |
8 files changed, 248 insertions, 118 deletions
@@ -30,18 +30,21 @@ module PartialVecBFF (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) → ({i : Get.|I| G} → Vec Carrier (Get.|gl₁| G i) → Vec Carrier (Get.|gl₂| G i) → Maybe (Vec Carrier (Get.|gl₁| G i))) - bff G s v = let s′ = enumerate s + 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 i 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 lookupV + 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 module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open GetTypes.VecVec public using (Get) @@ -50,5 +53,5 @@ module VecBFF (A : DecSetoid ℓ₀ ℓ₀) where open PartialVecBFF A public using (assoc ; enumerate ; denumerate) - bff : (G : Get) → ({n : ℕ} → Vec Carrier n → Vec Carrier (Get.getlen G n) → Maybe (Vec Carrier n)) + bff : (G : Get) → {n : ℕ} → (m : ℕ) → Vec Carrier n → Vec Carrier (Get.getlen G m) → Maybe (Vec Carrier m) bff G = PartialVecBFF.bff A (VecVec-to-PartialVecVec G) 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.PartialVecBFF A using (assoc ; enumerate ; denumerate ; bff) +open BFF.PartialVecBFF A using (assoc ; enumerate ; enumeratel ; denumerate ; bff) open Setoid using () renaming (_≈_ to _∋_≈_) open module A = DecSetoid A using (Carrier) renaming (_≟_ to deq) @@ -101,11 +101,11 @@ lemma-2 (i ∷ is) (x ∷ xs) h p with assoc is xs | inspect (assoc is) xs lemma-2 (i ∷ is) (x ∷ xs) h () | nothing | _ lemma-2 (i ∷ is) (x ∷ xs) h p | just h' | [ ir ] = begin lookupM i h ∷ map (flip lookupM h) is - ≈⟨ lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p) VecEq.∷-cong ISetoid.refl (VecISetoid (MaybeSetoid A.setoid)) ⟩ + ≈⟨ VecEq._∷-cong_ (lemma-lookupM-assoc i is x xs h (trans (cong (flip _>>=_ (checkInsert i x)) ir) p)) (ISetoid.refl (VecISetoid (MaybeSetoid A.setoid))) ⟩ just x ∷ map (flip lookupM h) is ≡⟨ cong (_∷_ (just x)) (lemma-map-lookupM-assoc i x h h' p is (lemma-assoc-domain is xs h' ir)) ⟩ just x ∷ map (flip lookupM h') is - ≈⟨ Setoid.refl (MaybeSetoid A.setoid) VecEq.∷-cong (lemma-2 is xs h' ir) ⟩ + ≈⟨ VecEq._∷-cong_ (Setoid.refl (MaybeSetoid A.setoid)) (lemma-2 is xs h' ir) ⟩ just x ∷ map just xs ∎ where open EqR (VecISetoid (MaybeSetoid A.setoid) at _) @@ -125,26 +125,26 @@ 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 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) → {i : Get.|I| G} → (s : Vec Carrier (Get.|gl₁| G i)) → bff G i s (Get.get G s) ≡ 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)) ⟩ + bff G i s (get (map (denumerate s) (enumerate s))) + ≡⟨ cong (bff G i s) (free-theorem (denumerate s) (enumerate s)) ⟩ + bff G i 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))) (Get.|gl₁| G i))) + ≡⟨ 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)) ≡⟨ refl ⟩ - mapMV (flip lookupVec (fromFunc (denumerate s))) (enumerate s) - ≡⟨ cong (flip mapMV (enumerate s) ∘ flip lookupVec) (lemma-fromFunc-tabulate (denumerate s)) ⟩ - mapMV (flip lookupVec (tabulate (Maybe.just ∘ denumerate s))) (enumerate s) - ≡⟨ mapMV-cong (lookup∘tabulate (Maybe.just ∘ denumerate s)) (enumerate s) ⟩ + 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)) @@ -152,22 +152,22 @@ 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′↦r = flip _>>=_ (flip mapMV (enumerate s) ∘ flip lookupVec) + 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) lemma-<$>-just : {A B : Set} {f : A → B} {b : B} (ma : Maybe A) → f <$> ma ≡ just b → ∃ λ a → ma ≡ just a 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') @@ -178,8 +178,8 @@ lemma->>=-just (just a) p = a , refl lemma->>=-just nothing () 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 +lemma-just-sequence [] = refl +lemma-just-sequence (x ∷ xs) = cong (_<$>_ (_∷_ x)) (lemma-just-sequence xs) lemma-mapM-successful : {A B : Set} {f : A → Maybe B} {n : ℕ} → (v : Vec A n) → {r : Vec B n} → mapMV f v ≡ just r → ∃ λ w → map f v ≡ map just w lemma-mapM-successful [] p = [] , refl @@ -190,19 +190,19 @@ lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] with l lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] | w , pw = y ∷ w , cong (_∷_ (just y)) pw 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 = let w , pw = lemma-mapM-successful v p in begin +lemma-get-mapMV {f = f} G {v = v} p = begin get <$> mapMV f v ≡⟨ cong (_<$>_ get) (sym (sequence-map f v)) ⟩ get <$> (sequenceV (map f v)) - ≡⟨ cong (_<$>_ get ∘ sequenceV) pw ⟩ - get <$> (sequenceV (map just w)) - ≡⟨ cong (_<$>_ get) (lemma-just-sequence w) ⟩ - get <$> just w - ≡⟨ sym (lemma-just-sequence (get w)) ⟩ - sequenceV (map just (get w)) - ≡⟨ cong sequenceV (sym (free-theorem just w)) ⟩ - sequenceV (get (map just w)) - ≡⟨ cong (sequenceV ∘ get) (sym pw) ⟩ + ≡⟨ cong (_<$>_ get ∘ sequenceV) (proj₂ wp) ⟩ + get <$> (sequenceV (map just (proj₁ wp))) + ≡⟨ cong (_<$>_ get) (lemma-just-sequence (proj₁ wp)) ⟩ + get <$> just (proj₁ wp) + ≡⟨ sym (lemma-just-sequence (get (proj₁ wp))) ⟩ + sequenceV (map just (get (proj₁ wp))) + ≡⟨ cong sequenceV (sym (free-theorem just (proj₁ wp))) ⟩ + sequenceV (get (map just (proj₁ wp))) + ≡⟨ cong (sequenceV ∘ get) (sym (proj₂ wp)) ⟩ sequenceV (get (map f v)) ≡⟨ cong sequenceV (free-theorem f v) ⟩ sequenceV (map f (get v)) @@ -210,30 +210,33 @@ lemma-get-mapMV {f = f} G {v = v} p = let w , pw = lemma-mapM-successful v p in mapMV f (get v) ∎ where open ≡-Reasoning open Get G + wp = lemma-mapM-successful v p sequence-cong : {S : Setoid ℓ₀ ℓ₀} {n : ℕ} {m₁ m₂ : Setoid.Carrier (VecISetoid (MaybeSetoid S) at n)} → VecISetoid (MaybeSetoid S) at _ ∋ m₁ ≈ m₂ → MaybeSetoid (VecISetoid S at n) ∋ sequenceV m₁ ≈ sequenceV m₂ sequence-cong {S} VecEq.[]-cong = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | just sxs | just sys | just p = MaybeEq.just (x≈y VecEq.∷-cong p) -sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (just x≈y VecEq.∷-cong xs≈ys) | nothing | nothing | nothing = Setoid.refl (MaybeSetoid (VecISetoid S at _)) -sequence-cong {S} (nothing VecEq.∷-cong xs≈ys) = Setoid.refl (MaybeSetoid (VecISetoid S at _)) - -theorem-2 : (G : Get) → {i : Get.|I| G} → (v : Vec Carrier (Get.|gl₂| G i)) → (s u : Vec Carrier (Get.|gl₁| G i)) → 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 _) ⟩ +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) with sequenceV xs | sequenceV ys | sequence-cong xs≈ys +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | just sys | just p = MaybeEq.just (VecEq._∷-cong_ x≈y p) +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | nothing | just sys | () +sequence-cong {S} {m₁ = just x ∷ xs} {m₂ = just y ∷ ys} (VecEq._∷-cong_ (just x≈y) xs≈ys) | just sxs | nothing | () +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 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⟨ MaybeSetoid (VecISetoid A.setoid at _) ⟩ get <$> (just u) ≡⟨ cong (_<$>_ get) (sym p) ⟩ - get <$> (bff G s v) + get <$> (bff G j 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 G (trans (cong (flip _>>=_ h′↦r ∘ _<$>_ h↦h′) (sym ph)) p) ⟩ - 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 ∎) @@ -242,5 +245,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 (Get.|gl₁| G j) + h↦h′ = flip union (reshape g′ (Get.|gl₁| G j)) + h′↦r = flip mapMV t ∘ flip lookupM diff --git a/Everything.agda b/Everything.agda index 7399254..e37c76e 100644 --- a/Everything.agda +++ b/Everything.agda @@ -10,3 +10,5 @@ import BFF import Bidir import LiftGet import Precond +import Examples +import BFFPlug diff --git a/Examples.agda b/Examples.agda new file mode 100644 index 0000000..5971460 --- /dev/null +++ b/Examples.agda @@ -0,0 +1,46 @@ +module Examples where + +open import Data.Nat using (ℕ ; zero ; suc ; _⊓_ ; _∸_ ; ⌈_/2⌉) +open import Data.Vec using (Vec ; [] ; _∷_ ; reverse ; _++_) + +import GetTypes +import FreeTheorems + +open GetTypes.VecVec using (Get) +open FreeTheorems.VecVec using (assume-get) + +reverse' : Get +reverse' = assume-get reverse + +double' : Get +double' = assume-get f + where g : ℕ → ℕ + g zero = zero + g (suc n) = suc (suc (g n)) + f : {A : Set} {n : ℕ} → Vec A n → Vec A (g n) + f [] = [] + f (x ∷ v) = x ∷ x ∷ f v + +double'' : Get +double'' = assume-get (λ v → v ++ v) + +take' : ℕ → Get +take' n = assume-get (f n) + where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ⊓ n) + f n [] = [] + f zero (x ∷ xs) = [] + f (suc n) (x ∷ xs) = x ∷ f n xs + +drop' : ℕ → Get +drop' n = assume-get (f n) + where f : (n : ℕ) → {A : Set} {m : ℕ} → Vec A m → Vec A (m ∸ n) + f zero xs = xs + f (suc n) [] = [] + f (suc n) (x ∷ xs) = f n xs + +sieve' : Get +sieve' = assume-get f + where f : {A : Set} {n : ℕ} → Vec A n → Vec A ⌈ n /2⌉ + f [] = [] + f (x ∷ []) = x ∷ [] + f (x ∷ _ ∷ xs) = x ∷ f xs diff --git a/FinMap.agda b/FinMap.agda index ea4f49b..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)) @@ -94,17 +99,24 @@ lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → lemma-tabulate-∘ {zero} {_} {f} {g} f≗g = refl lemma-tabulate-∘ {suc n} {_} {f} {g} f≗g = cong₂ _∷_ (f≗g zero) (lemma-tabulate-∘ (f≗g ∘ suc)) -lemma-fromFunc-tabulate : {n : ℕ} {A : Set} → (f : Fin n → A) → fromFunc f ≡ tabulate (just ∘ f) +lemma-lookupM-fromFunc : {n : ℕ} {A : Set} → (f : Fin n → A) → flip lookupM (fromFunc f) ≗ just ∘ f +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 with p refl -... | () +lemma-lookupM-delete {i = zero} {j = zero} (_ ∷ _) p = contradiction refl p 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) @@ -112,9 +124,7 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s maybe′ just (lookupM x (fromFunc f)) (lookupM x empty) ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ lookupM x (fromFunc f) - ≡⟨ cong (lookupM x) (lemma-fromFunc-tabulate f) ⟩ - lookupM x (tabulate (just ∘ f)) - ≡⟨ lookup∘tabulate (just ∘ f) x ⟩ + ≡⟨ lemma-lookupM-fromFunc f x ⟩ just (f x) ∎ lemma-inner (t ∷ ts) x with x ≟ t lemma-inner (.x ∷ ts) x | yes refl = cong (maybe′ just (lookupM x (delete-many (x ∷ ts) (fromFunc f)))) (lemma-lookupM-insert x (f x) (restrict f (toList ts))) diff --git a/Generic.agda b/Generic.agda index a734ec2..c458483 100644 --- a/Generic.agda +++ b/Generic.agda @@ -8,13 +8,13 @@ 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 Function using (_∘_ ; id) +open import Function using (_∘_ ; id ; flip) open import Function.Equality using (_⟶_) open import Level using () renaming (zero to ℓ₀) open import Relation.Binary using (Setoid ; module Setoid) open import Relation.Binary.Core using (_≡_ ; refl) open import Relation.Binary.Indexed using (_at_) renaming (Setoid to ISetoid) -open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans) renaming (setoid to EqSetoid) +open import Relation.Binary.PropositionalEquality using (_≗_ ; cong ; subst ; trans ; cong₂) renaming (setoid to EqSetoid) open Setoid using () renaming (_≈_ to _∋_≈_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.functor using (_<$>_) @@ -35,14 +35,12 @@ mapMV f []V = just []V mapMV f (x ∷V xs) = (f x) >>= (λ y → (_∷V_ y) <$> (mapMV f xs)) 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 = f} {g = g} f≗g (x ∷V xs) with f x | g x | f≗g x -mapMV-cong f≗g (x ∷V xs) | just y | .(just y) | refl = cong (_<$>_ (_∷V_ y)) (mapMV-cong f≗g xs) -mapMV-cong f≗g (x ∷V xs) | nothing | .nothing | refl = refl +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-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (just ∘ f) v ≡ just (map f v) -mapMV-purity f []V = refl -mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl +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 +mapMV-purity f (x ∷V xs) = cong (_<$>_ (_∷V_ (f x))) (mapMV-purity f xs) maybeEq-from-≡ : {A : Set} {a b : Maybe A} → a ≡ b → MaybeEq (EqSetoid A) ∋ a ≈ b maybeEq-from-≡ {a = just x} {b = .(just x)} refl = just refl @@ -84,7 +82,7 @@ toList-subst v refl = refl VecISetoid : Setoid ℓ₀ ℓ₀ → ISetoid ℕ ℓ₀ ℓ₀ VecISetoid S = record { Carrier = Vec (Setoid.Carrier S) - ; _≈_ = λ x → S VecEq.≈ x + ; _≈_ = λ x → VecEq._≈_ S x ; isEquivalence = record { refl = VecEq.refl S _ ; sym = VecEq.sym S diff --git a/Precond.agda b/Precond.agda index ebb5412..bc619dc 100644 --- a/Precond.agda +++ b/Precond.agda @@ -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₂) +open import Data.Product using (∃ ; _,_ ; proj₁ ; proj₂) open import Function using (flip ; _∘_ ; id) open import Relation.Binary using (Setoid) open import Relation.Binary.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) @@ -26,70 +26,71 @@ 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) +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 -open import Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) +import Bidir +open Bidir (decSetoid deq) using (_in-domain-of_ ; lemma-assoc-domain ; lemma-just-sequence) import GetTypes open GetTypes.PartialVecVec using (Get ; module Get) -open BFF.PartialVecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) - -lemma-lookup-map-just : {n : ℕ} (f : Fin n) {A : Set} (v : Vec A n) → lookup f (map Maybe.just v) ≡ Maybe.just (lookup f v) -lemma-lookup-map-just zero (x ∷ xs) = refl -lemma-lookup-map-just (suc f) (x ∷ xs) = lemma-lookup-map-just f xs +open BFF.PartialVecBFF (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 lemma-maybe-just a nothing = refl -lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Vec A n} → (toList is) in-domain-of h → ∃ λ v → union h (delete-many is (map just g)) ≡ map just v +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 (map just g) + union h (fromFunc g) ≡⟨ lemma-tabulate-∘ (λ f → begin - maybe′ just (lookup f (map just g)) (lookup f h) - ≡⟨ 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 (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))) + 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))) ∎) +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 (map just g)) + 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 (map just g)))) (lookup f h) ≡ maybe′ just (lookupM f (delete-many is (map just g))) (lookup f h) + 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 - maybe′ just (lookupM i (delete i (delete-many is (map just g)))) (lookup i h) + maybe′ just (lookupM i (delete i (delete-many is (fromFunc g)))) (lookup i h) ≡⟨ 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) + 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 s v ≡ just u -assoc-enough G s v (h , p) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (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) pw ⟩ - sequenceV (map (flip lookupM (map just w)) s′) - ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f w) s′) ⟩ - sequenceV (map (Maybe.just ∘ flip lookup w) s′) - ≡⟨ cong sequenceV (map-∘ just (flip lookup w) s′) ⟩ - sequenceV (map Maybe.just (map (flip lookup w) s′)) - ≡⟨ lemma-just-sequence (map (flip lookup w) s′) ⟩ - just (map (flip lookup w) s′) ∎) +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 + 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) ⟩ + 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) ∎) where open Get G s′ = enumerate s g = fromFunc (denumerate s) g′ = delete-many (get s′) g + t = enumeratel (Get.|gl₁| G i) + 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 [] |