diff options
| -rw-r--r-- | Bidir.agda | 16 | ||||
| -rw-r--r-- | CheckInsert.agda | 5 | ||||
| -rw-r--r-- | FinMap.agda | 27 |
3 files changed, 23 insertions, 25 deletions
@@ -51,14 +51,14 @@ module SetoidReasoning where _≡⟨_⟩_ : {X : Setoid ℓ₀ ℓ₀} → (x : Setoid.Carrier X) → {y z : Setoid.Carrier X} → x ≡ y → EqR._IsRelatedTo_ X y z → EqR._IsRelatedTo_ X x z _≡⟨_⟩_ {X} = EqR._≡⟨_⟩_ X -lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f (toList is)) +lemma-1 : {m n : ℕ} → (f : Fin n → Carrier) → (is : Vec (Fin n) m) → assoc is (map f is) ≡ just (restrict f is) lemma-1 f [] = refl lemma-1 f (i ∷ is′) = begin (assoc is′ (map f is′) >>= checkInsert i (f i)) ≡⟨ cong (λ m → m >>= checkInsert i (f i)) (lemma-1 f is′) ⟩ - checkInsert i (f i) (restrict f (toList is′)) - ≡⟨ lemma-checkInsert-restrict f i (toList is′) ⟩ - just (restrict f (toList (i ∷ is′))) ∎ + checkInsert i (f i) (restrict f is′) + ≡⟨ lemma-checkInsert-restrict f i is′ ⟩ + just (restrict f (i ∷ is′)) ∎ where open ≡-Reasoning lemma-lookupM-checkInserted : {n : ℕ} → (i : Fin n) → (x : Carrier) → (h h' : FinMapMaybe n Carrier) → checkInsert i x h ≡ just h' → MaybeSetoid A.setoid ∋ lookupM i h' ≈ just x @@ -134,11 +134,11 @@ theorem-1 G {i} s = begin ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′ ∘ assoc (Shaped.content ViewShapeT (get t))) (Shaped.fmap-content ViewShapeT f (get t)) ⟩ h′↦r <$> (h↦h′ <$> (assoc (Shaped.content ViewShapeT (get t)) (map f (Shaped.content ViewShapeT (get t))))) ≡⟨ cong (_<$>_ h′↦r ∘ _<$>_ h↦h′) (lemma-1 f (Shaped.content ViewShapeT (get t))) ⟩ - (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (toList (Shaped.content ViewShapeT (get t)))) + (Maybe.just ∘ h′↦r ∘ h↦h′) (restrict f (Shaped.content ViewShapeT (get t))) ≡⟨ cong just (begin - h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i)))) - ≡⟨ cong (h′↦r ∘ union (restrict f (toList (Shaped.content ViewShapeT (get t))))) (lemma-reshape-id g′) ⟩ - h′↦r (union (restrict f (toList (Shaped.content ViewShapeT (get t)))) g′) + h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) (reshape g′ (Shaped.arity SourceShapeT (|gl₁| i)))) + ≡⟨ cong (h′↦r ∘ union (restrict f (Shaped.content ViewShapeT (get t)))) (lemma-reshape-id g′) ⟩ + h′↦r (union (restrict f (Shaped.content ViewShapeT (get t))) g′) ≡⟨ cong h′↦r (lemma-disjoint-union f (Shaped.content ViewShapeT (get t))) ⟩ h′↦r (fromFunc f) ≡⟨ refl ⟩ diff --git a/CheckInsert.agda b/CheckInsert.agda index 52dffc4..62ec6c8 100644 --- a/CheckInsert.agda +++ b/CheckInsert.agda @@ -7,8 +7,7 @@ open import Data.Nat using (ℕ) open import Data.Fin using (Fin) open import Data.Fin.Props using (_≟_) open import Data.Maybe using (Maybe ; nothing ; just) renaming (setoid to MaybeSetoid ; Eq to MaybeEq) -open import Data.List using (List ; [] ; _∷_) -open import Data.Vec using () renaming (_∷_ to _∷V_) +open import Data.Vec using (Vec) renaming (_∷_ to _∷V_) open import Data.Vec.Equality using () renaming (module Equality to VecEq) open import Relation.Nullary using (Dec ; yes ; no ; ¬_) open import Relation.Nullary.Negation using (contradiction) @@ -57,7 +56,7 @@ lemma-checkInsert-wrong i x m x' d refl | .(just x') with deq x x' lemma-checkInsert-wrong i x m x' d refl | .(just x') | yes q = contradiction q d lemma-checkInsert-wrong i x m x' d refl | .(just x') | no ¬q = refl -lemma-checkInsert-restrict : {n : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : List (Fin n)) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷ is)) +lemma-checkInsert-restrict : {n m : ℕ} → (f : Fin n → Carrier) → (i : Fin n) → (is : Vec (Fin n) m) → checkInsert i (f i) (restrict f is) ≡ just (restrict f (i ∷V is)) lemma-checkInsert-restrict f i is with checkInsert i (f i) (restrict f is) | insertionresult i (f i) (restrict f is) lemma-checkInsert-restrict f i is | ._ | same x fi≈x p = cong just (lemma-insert-same _ i (f i) (trans p (cong just (sym (lemma-lookupM-restrict i f is x p))))) lemma-checkInsert-restrict f i is | ._ | new _ = refl diff --git a/FinMap.agda b/FinMap.agda index f9572b8..ccd522e 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -5,11 +5,10 @@ open import Data.Nat using (ℕ ; zero ; suc) open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) renaming (setoid to MaybeEq) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Props using (_≟_) -open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; toList) renaming (lookup to lookupVec ; map to mapV) +open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip) renaming (lookup to lookupVec ; map to mapV) open import Data.Vec.Equality using () open Data.Vec.Equality.Equality using (_∷-cong_) open import Data.Vec.Properties using (lookup∘tabulate) -open import Data.List using (List ; [] ; _∷_ ; map ; zip) open import Data.Product using (_×_ ; _,_) open import Function using (id ; _∘_ ; flip ; const) open import Relation.Nullary using (yes ; no) @@ -33,7 +32,7 @@ insert f a m = m [ f ]≔ (just a) empty : {A : Set} {n : ℕ} → FinMapMaybe n A empty = replicate nothing -fromAscList : {A : Set} {n : ℕ} → List (Fin n × A) → FinMapMaybe n A +fromAscList : {A : Set} {n m : ℕ} → Vec (Fin n × A) m → FinMapMaybe n A fromAscList [] = empty fromAscList ((f , a) ∷ xs) = insert f a (fromAscList xs) @@ -48,8 +47,8 @@ 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)) -restrict : {A : Set} {n : ℕ} → (Fin n → A) → List (Fin n) → FinMapMaybe n A -restrict f is = fromAscList (zip is (map f is)) +restrict : {A : Set} {n m : ℕ} → (Fin n → A) → Vec (Fin n) m → FinMapMaybe n A +restrict f is = fromAscList (zip is (mapV f is)) delete : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → FinMapMaybe n A delete i m = m [ i ]≔ nothing @@ -76,7 +75,7 @@ lemma-lookupM-insert-other zero (suc j) a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) zero a (x ∷ xs) p = refl lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc) -lemma-lookupM-restrict : {A : Set} {n : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : List (Fin n)) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a +lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → (a : A) → lookupM i (restrict f is) ≡ just a → f i ≡ a lemma-lookupM-restrict i f [] a p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ()) lemma-lookupM-restrict i f (i' ∷ is) a p with i ≟ i' lemma-lookupM-restrict i f (.i ∷ is) a p | yes refl = just-injective (begin @@ -110,9 +109,9 @@ lemma-reshape-id : {n : ℕ} {A : Set} → (m : FinMapMaybe n A) → reshape m n 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 : ℕ} {A : Set} → (f : Fin n → A) → (t : Vec (Fin n) m) → union (restrict f t) (delete-many t (fromFunc f)) ≡ fromFunc f lemma-disjoint-union {n} {m} f t = lemma-tabulate-∘ (lemma-inner t) - 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) + 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 t)) ≡ just (f x) lemma-inner [] x = begin maybe′ just (lookupM x (fromFunc f)) (lookupM x empty) ≡⟨ cong (maybe′ just (lookupM x (fromFunc f))) (lemma-lookupM-empty x) ⟩ @@ -120,12 +119,12 @@ lemma-disjoint-union {n} {m} f t = lemma-tabulate-∘ (lemma-inner t) ≡⟨ 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))) + 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 ts)) lemma-inner (t ∷ ts) x | no ¬p = begin - maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList (t ∷ ts)))) - ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (lemma-lookupM-insert-other x t (f t) (restrict f (toList ts)) ¬p) ⟩ - maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (toList ts))) - ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f (toList ts)))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩ - maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f (toList ts))) + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f (t ∷ ts))) + ≡⟨ cong (maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f)))) (lemma-lookupM-insert-other x t (f t) (restrict f ts) ¬p) ⟩ + maybe′ just (lookupM x (delete-many (t ∷ ts) (fromFunc f))) (lookupM x (restrict f ts)) + ≡⟨ cong (flip (maybe′ just) (lookupM x (restrict f ts))) (lemma-lookupM-delete (delete-many ts (fromFunc f)) ¬p) ⟩ + maybe′ just (lookupM x (delete-many ts (fromFunc f))) (lookupM x (restrict f ts)) ≡⟨ lemma-inner ts x ⟩ just (f x) ∎ |