diff options
Diffstat (limited to 'Precond.agda')
| -rw-r--r-- | Precond.agda | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Precond.agda b/Precond.agda index 8eec6da..293f44d 100644 --- a/Precond.agda +++ b/Precond.agda @@ -15,7 +15,7 @@ import Data.Maybe.Categorical open Category.Monad.RawMonad {Level.zero} Data.Maybe.Categorical.monad using (_>>=_) open Category.Functor.RawFunctor {Level.zero} Data.Maybe.Categorical.functor using (_<$>_) open import Data.Vec using (Vec ; [] ; _∷_ ; map ; lookup ; toList) -open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘ ; lookup-replicate) +open import Data.Vec.Properties using (map-cong ; map-∘ ; tabulate-∘ ; lookup-replicate ; tabulate-cong) import Data.List.All open import Data.List.Any using (here ; there) open import Data.List.Membership.Setoid using (_∉_) @@ -28,7 +28,7 @@ open P.≡-Reasoning using (begin_ ; _≡⟨_⟩_ ; _∎) open import Relation.Nullary using (yes ; no) open import Structures using (IsFunctor ; module Shaped ; Shaped) -open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; delete-many ; lemma-tabulate-∘ ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id) +open import FinMap using (FinMapMaybe ; lookupM ; union ; fromFunc ; empty ; insert ; delete-many ; delete ; lemma-lookupM-delete ; lemma-lookupM-fromFunc ; reshape ; lemma-reshape-id) import CheckInsert open CheckInsert (P.decSetoid deq) using (checkInsert ; lemma-checkInsert-new ; lemma-lookupM-checkInsert-other) import BFF @@ -43,7 +43,7 @@ lemma-maybe-just a (just x) = P.refl lemma-maybe-just a nothing = P.refl lemma-union-delete-fromFunc : {m n : ℕ} {A : Set} {is : Vec (Fin n) m} {h : FinMapMaybe n A} {g : Fin n → A} → 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 = _ , (lemma-tabulate-∘ (λ f → begin +lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (tabulate-cong (λ f → begin maybe′ just (lookupM f (fromFunc g)) (lookupM f h) ≡⟨ P.cong (flip (maybe′ just) (lookupM f h)) (lemma-lookupM-fromFunc g f) ⟩ maybe′ just (just (g f)) (lookupM f h) @@ -51,7 +51,7 @@ lemma-union-delete-fromFunc {is = []} {h = h} {g = g} p = _ , (lemma-tabulate-∠just (maybe′ id (g f) (lookupM 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 ⟩ + ≡⟨ tabulate-cong inner ⟩ union h (delete-many is (fromFunc g)) ≡⟨ proj₂ (lemma-union-delete-fromFunc ps) ⟩ _ ∎) |