[Agda] `with' to case_of_ example

[Sergei Meshveliani]

Hi, all,

I attach a small program for deleting a key from a pair list,
and for proving  (Preserves _≈_ ⟶ _≡_)  for this operation.

The `with' version is type-checked and the `case' version is not
(Agda 2.5.1, ghc-7.10.2).

Is this a bug?
Can it be written as case_of_ ? 

(Agda 2.5.1, ghc-7.10.2).

Thanks,

------
Sergei
-------------- next part --------------
open import Level            using (Level)
open import Function         using (case_of_)
open import Relation.Nullary using (yes; no)
open import Relation.Binary  using (DecSetoid; _Preserves_⟶_)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty   using (⊥-elim)
open import Data.Product using (_×_; _,_)
open import Data.List    using (List; []; _∷_)

module _ {α α= β : Level} (decSetoidK : DecSetoid α α=) (V : Set β) 
  where
  open DecSetoid decSetoidK using (_≈_; _≟_; sym; trans)  
                            renaming (Carrier to K)  
  Pair = K × V

  delKey : K → List Pair → List Pair   
  delKey _ []              =  []
  delKey k ((k' , v) ∷ ps) =  case k ≟ k' 
                              of \ 
                              { (yes _) → ps
                              ; (no _)  → (k' , v) ∷ (delKey k ps) }

  cong-delKey :  ∀ {ps} → (\k → delKey k ps) Preserves _≈_ ⟶ _≡_

  cong-delKey {[]}            _             =  PE.refl
  cong-delKey {(k₁ , v) ∷ ps} {k} {k'} k≈k' 
                                       with k ≟ k₁ | k' ≟ k₁
  ... | yes _    | yes _ =  PE.refl
  ... | no _     | no _  =
                      PE.cong ((k₁ , v) ∷_) (cong-delKey {ps = ps} k≈k')

  ... | yes k≈k₁ | no k'≉k₁  =  ⊥-elim (k'≉k₁ (trans (sym k≈k') k≈k₁))
  ... | no k≉k₁  | yes k'≈k₁ =  ⊥-elim (k≉k₁  (trans k≈k' k'≈k₁))


  cong-delKey' :  ∀ {ps} → (\k → delKey k ps) Preserves _≈_ ⟶ _≡_
  cong-delKey' {[]}            _             =  PE.refl
  cong-delKey' {(k₁ , v) ∷ ps} {k} {k'} k≈k' =

    case ((k ≟ k₁) , (k' ≟ k₁))
    of \
    { (yes _ ,    yes _    ) → PE.refl
    ; (no _ ,     no _     ) →
                        PE.cong ((k₁ , v) ∷_) (cong-delKey' {ps = ps} k≈k')
    ; (yes k≈k₁ , no k'≉k₁ ) → ⊥-elim (k'≉k₁ (trans (sym k≈k') k≈k₁))
    ; (no k≉k₁  , yes k'≈k₁) → ⊥-elim (k≉k₁  (trans k≈k' k'≈k₁))
    }