diff options
Diffstat (limited to 'FinMap.agda')
| -rw-r--r-- | FinMap.agda | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/FinMap.agda b/FinMap.agda index 6342fc5..051014c 100644 --- a/FinMap.agda +++ b/FinMap.agda @@ -2,7 +2,8 @@ module FinMap where open import Level using () renaming (zero to ℓ₀) open import Data.Nat using (ℕ ; zero ; suc) -open import Data.Maybe using (Maybe ; just ; nothing ; maybe′ ; just-injective) +open import Data.Maybe using (Maybe ; just ; nothing ; maybe′) +open import Data.Maybe.Properties using (just-injective) open import Data.Fin using (Fin ; zero ; suc) open import Data.Fin.Properties using (_≟_) open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV) @@ -40,7 +41,7 @@ FinMapMaybe : ℕ → Set → Set FinMapMaybe n A = Vec (Maybe A) n lookupM : {A : Set} {n : ℕ} → Fin n → FinMapMaybe n A → Maybe A -lookupM = lookupVec +lookupM = flip lookupVec insert : {A : Set} {n : ℕ} → Fin n → A → FinMapMaybe n A → FinMapMaybe n A insert f a m = m [ f ]≔ (just a) @@ -129,6 +130,6 @@ lemma-disjoint-union {n} f t = tabulate-cong inner ≡⟨ P.cong (flip (maybe′ just) nothing) (lookup∘tabulate (just ∘ f) x) ⟩ just (f x) ∎ -lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is -lemma-exchange-maps h≈h′ {[]} All.[] = P.refl -lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis) +lemma-exchange-maps : {n m : ℕ} → {A : Set} → (h h′ : FinMapMaybe n A) → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is +lemma-exchange-maps h h' h≈h′ {[]} All.[] = P.refl +lemma-exchange-maps h h' h≈h′ {i ∷ is} (pi All.∷ pis) = P.cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h h' h≈h′ pis) |