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

[Sergei Meshveliani]

(First I have replied from another email program, but this reply is hold
for some unclear reason of not being a member of something.
Is this due to the reply-to address  andreas.abel at gu.se  ?
Sorry for possible duplication.
)


On Wed, 2014-10-29 at 23:12 +0100, Andreas Abel wrote:
> 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?
> 

My project suffers of expensive type check.
And `case' is said to save the type-check cost. And I am trying to set
`case' instead of `with' everywhere where this is possible. This is
easier to understand how to do this, when dealing with simple examples.
So far, I do not understand this. 
So, I try `with', then rewrite to `case'.
`case' fails in 2/3 of examples. Then try introducing a local function.
Then, may be, return to `with'. 

Also if I see a couple of simple usage examples of  case_return_of_,
this will probably help me to reduce the usage of `with'. 

Regards,

------
Sergei


> 
> 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)
> > -}
> >
> 
>