[Agda] `with' -> `case' example

[Andreas Abel]

I do not think you can write it with "case", as you need the fact that k 
\equiv k' in order to reduce delBy.

What's wrong with the "with" version?

--Andreas

On 29.10.2014 16:25, Sergei Meshveliani wrote:
> open import Function using (_∘_; case_of_)
> open import Relation.Nullary using (¬_; Dec; yes; no)
> open import Relation.Unary   using (Decidable)
> open import Relation.Binary  using (module Setoid; module DecSetoid;
>                                                            DecSetoid)
>                               renaming (Decidable to Decidable₂)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≗_)
> open import Data.Product using (_×_; proj₁; _,_)
> open import Data.List    using (List; []; _∷_; map)
>
>
> ----------------------------------------------------------------------
> delBy : ∀ {α p} {A : Set α} {P : A → Set p} →
>                              (P? : Decidable P) → List A → List A
> delBy _  []       = []
> delBy P? (x ∷ xs) = case P? x of \ { (yes _) → xs
>                                     ; (no _)  → x ∷ (delBy P? xs) }
>
> ----------------------------------------------------------------------
> module AssocList-pack {α α= β} (Key : DecSetoid α α=) (Val : Set β)
>    where
>    open DecSetoid Key using (_≈_; _≟_) renaming (Carrier to K)
>    KV = K × Val
>
>    del : K → List K → List K
>    del x =  delBy (_≟_ x)
>
>    getKeys : List KV → List K
>    getKeys = map proj₁
>
>    delByKey : K → List KV → List KV
>    delByKey k =  delBy ((_≟_ k) ∘ proj₁)
>
>    keys-commute-delByKey :
>                          {k : K} → getKeys ∘ delByKey k ≗ del k ∘ getKeys
>    keys-commute-delByKey {k} []              =  PE.refl
>    keys-commute-delByKey {k} ((k' , v) ∷ ps) =
>      case
>          k ≟ k'
>      of \
>      { (yes _) → PE.refl
>      ; (no _)  → PE.cong (_∷_ k') (keys-commute-delByKey {k} ps) }
>
> {-
>      with k ≟ k'
>    ...
>        | yes _ = PE.refl
>    ... | no _  = PE.cong (_∷_ k') (keys-commute-delByKey {k} ps)
> -}
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/