diff options
| -rw-r--r-- | Bidir.agda | 8 | ||||
| -rw-r--r-- | Generic.agda | 20 | ||||
| -rw-r--r-- | Precond.agda | 4 |
3 files changed, 13 insertions, 19 deletions
@@ -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)) diff --git a/Generic.agda b/Generic.agda index c458483..9f1172d 100644 --- a/Generic.agda +++ b/Generic.agda @@ -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 diff --git a/Precond.agda b/Precond.agda index bc619dc..3e4c219 100644 --- a/Precond.agda +++ b/Precond.agda @@ -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) |