michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixed problem in Maps

Browse source
This commit is contained in:
wadler 2017-06-20 20:48:54 +01:00
parent f639060d7c
commit 91fb356db0
1 changed files with 15 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Maps.lagda
View file

@ -292,21 +292,22 @@ updates.
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} ρ x v y w z x≢y with x ≟ z | y ≟ z
... | yes refl | yes refl = ⊥-elim (x≢y refl)
... | no x≢z | yes refl = sym (update-eq′ ρ z w)
... | yes refl | no y≢z = update-eq′ ρ z v
... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
\end{code}
And a slightly different version of the same proof.
\begin{code}
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} ρ x v y w z x≢y with x ≟ z | y ≟ z
... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
... | no x≢z | yes y≡z rewrite y≡z = {! sym (update-eq′ ρ z w)!}
... | yes x≡z | no y≢z rewrite x≡z = {! update-eq′ ρ z v!}
... | no x≢z | no y≢z = {! trans (update-neq ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
{-
Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?
Why does "λ y₁" appear in the final hole?
?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z)
?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v
?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡
(((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z)
-}
... | no x≢z | yes y≡z rewrite y≡z = sym (update-eq′ ρ z w)
... | yes x≡z | no y≢z rewrite x≡z = update-eq′ ρ z v
... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
\end{code}
</div>