diff options
| -rw-r--r-- | Bidir.agda | 35 | ||||
| -rw-r--r-- | FinMap.agda | 6 | ||||
| -rw-r--r-- | Generic.agda | 4 | ||||
| -rw-r--r-- | Precond.agda | 26 |
4 files changed, 38 insertions, 33 deletions
@@ -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 _) @@ -191,19 +191,19 @@ lemma-mapM-successful (x ∷ xs) p | just y | just ys | [ p′ ] | w , lemma-get-mapMV : {A B : Set} {f : A → Maybe B} {n : ℕ} {v : Vec A n} {r : Vec B n} → mapMV f v ≡ just r → (get : Get) → Get.get get <$> mapMV f v ≡ mapMV f (Get.get get v) -lemma-get-mapMV {f = f} {v = v} p G = let w , pw = lemma-mapM-successful v p in begin +lemma-get-mapMV {f = f} {v = v} p G = 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)) @@ -211,13 +211,16 @@ lemma-get-mapMV {f = f} {v = v} p G = 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 _)) +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) → {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) diff --git a/FinMap.agda b/FinMap.agda index ea4f49b..052ed6f 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -94,7 +94,7 @@ 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-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)) @@ -113,8 +113,8 @@ lemma-disjoint-union {n} {m} f t = trans (lemma-tabulate-∘ (lemma-inner t)) (s ≡⟨ 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 ⟩ + lookupM x (tabulate (Maybe.just ∘ f)) + ≡⟨ lookup∘tabulate (Maybe.just ∘ 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 81292ff..748a49a 100644 --- a/Generic.agda +++ b/Generic.agda @@ -36,7 +36,7 @@ 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-purity : {A B : Set} {n : ℕ} → (f : A → B) → (v : Vec A n) → mapMV (just ∘ f) v ≡ just (map f 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 mapMV-purity f (x ∷V xs) rewrite mapMV-purity f xs = refl @@ -80,7 +80,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 2be3f3a..afb77d8 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.PropositionalEquality using (refl ; cong ; inspect ; [_] ; sym ; decSetoid) open Relation.Binary.PropositionalEquality.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) @@ -29,7 +29,8 @@ open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; ins 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.VecVec using (Get ; module Get) open BFF.VecBFF (decSetoid deq) using (assoc ; enumerate ; denumerate ; bff) @@ -54,7 +55,7 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (begin 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 +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 (map just g))) ≡⟨ lemma-tabulate-∘ inner ⟩ union h (delete-many is (map just g)) @@ -71,24 +72,25 @@ lemma-union-delete-fromFunc {n = n} {is = i ∷ is} {h = h} {g = g} ((x , px) Da inner f | no f≢i = cong (flip (maybe′ just) (lookup f h)) (lemma-lookupM-delete (delete-many is (map just 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) = let w , pw = lemma-union-delete-fromFunc (lemma-assoc-domain (get s′) v h p) in _ , (begin +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) 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′) ∎) + ≡⟨ cong (sequenceV ∘ flip map s′ ∘ flip lookupM) (proj₂ wp) ⟩ + sequenceV (map (flip lookupM (map just (proj₁ wp))) s′) + ≡⟨ cong sequenceV (map-cong (λ f → lemma-lookup-map-just f (proj₁ wp)) s′) ⟩ + sequenceV (map (Maybe.just ∘ flip lookup (proj₁ wp)) s′) + ≡⟨ cong sequenceV (map-∘ just (flip lookup (proj₁ wp)) s′) ⟩ + sequenceV (map Maybe.just (map (flip lookup (proj₁ wp)) s′)) + ≡⟨ lemma-just-sequence (map (flip lookup (proj₁ wp)) s′) ⟩ + just (map (flip lookup (proj₁ wp)) s′) ∎) 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) data All-different {A : Set} : List A → Set where different-[] : All-different [] |