diff --git a/src/Maps.lagda b/src/Maps.lagda index 4e292d41..7d4eebd1 100644 --- a/src/Maps.lagda +++ b/src/Maps.lagda @@ -86,6 +86,8 @@ y = id "y" z = id "z" \end{code} +## Extensionality + ## Total Maps Our main job in this chapter will be to build a definition of @@ -219,8 +221,8 @@ back $$v$$: update-eq′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) → (ρ , x ↦ v) x ≡ v update-eq′ ρ x v with x ≟ x - ... | yes x=x = refl - ... | no x≠x = ⊥-elim (x≠x refl) + ... | yes x≡x = refl + ... | no x≢x = ⊥-elim (x≢x refl) \end{code} @@ -237,6 +239,14 @@ the same result that $$m$$ would have given: ... | no _ = refl \end{code} +For the following lemmas, since maps are represented by functions, to +show two maps equal we will need to postulate extensionality. + +\begin{code} + postulate + extensionality : ∀ {A : Set} {ρ ρ′ : TotalMap A} → (∀ x → ρ x ≡ ρ′ x) → ρ ≡ ρ′ +\end{code} + #### Exercise: 2 stars, optional (update-shadow) If we update a map $$ρ$$ at a key $$x$$ with a value $$v$$ and then update again with the same key $$x$$ and another value $$w$$, the @@ -246,18 +256,20 @@ the second update on $$ρ$$: \begin{code} postulate - update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) (y : Id) - → (ρ , x ↦ v , x ↦ w) y ≡ (ρ , x ↦ w) y + update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) + → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w) \end{code} @@ -268,16 +280,18 @@ result is equal to $$ρ$$: \begin{code} postulate - update-same : ∀ {A} (ρ : TotalMap A) (x y : Id) → (ρ , x ↦ ρ x) y ≡ ρ y + update-same : ∀ {A} (ρ : TotalMap A) (x : Id) → (ρ , x ↦ ρ x) ≡ ρ \end{code} @@ -288,19 +302,22 @@ updates. \begin{code} postulate - update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id) - → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z + update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) + → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v) \end{code}