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

[mechvel at scico.botik.ru]

Andreas Abel писал 30.10.2014 02:12:
> 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 the Agda developers wrote that `case' is less expensive in type 
checking than `with'.
So that I need to write `case' instead of `with' everywhere where this 
is possible. Then, if I understand how "to case" in a simple example, I 
would probably know how to do this in more complex examples, in which 
the type-check difference really matters.

Currently I act as follows.
(1) Write `with', make it type-check. `with' is most friendly.
(2) Rewrite to `case'. This fails in 2/3 of examples.
     (Also all my attempts with  case_return-of_  have failed, probably, 
I use it wrongly,
      it will be helpful to see a couple of nice examples of its usage).

(3) If it is not type check, then rewrite to introducing an intermediate 
function.
(4) If (2) and (3) go bad, then return to `with'.

Regards,

------
Sergei



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