# [Agda] " | condition " in report

Sergei Meshveliani mechvel at botik.ru
Thu Dec 19 19:22:21 CET 2013

```Please,
what is wrong in the below program?

------------------------------------------------------------------------
open import Relation.Nullary using (yes; no)
open import Relation.Binary using
(module Setoid; module DecSetoid; module DecTotalOrder)
open import Relation.Binary.PropositionalEquality as PE
using (_≡_; _≢_)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
_∎ to _≡end)
open import Data.Empty      using (⊥-elim)
open import Data.Sum        using (_⊎_; inj₁; inj₂)
open import Data.Product    using (_×_; _,_; proj₁)
open import Data.Nat as Nat using (ℕ)
open import Data.List       using (List; []; _∷_; map)
open import Data.List.Any using (Any; module Any; module Membership)

open Any
natDecSetoid = DecTotalOrder.Eq.decSetoid Nat.decTotalOrder
_≟_          = DecSetoid._≟_    natDecSetoid
natSetoid    = DecSetoid.setoid natDecSetoid

open module Mem-ℕ = Membership natSetoid using (_∈_)

------------------------------------------------------------------------
getKeys : List (ℕ × ℕ) → List ℕ
getKeys = map proj₁

insert : ℕ → ℕ → List (ℕ × ℕ) → List (ℕ × ℕ)
insert k v []               =  (k , v) ∷ []
insert k v ((k' , v') ∷ ps)  with  k ≟ k'
...                                | yes _ = (k' , v) ∷ ps
...                                | no _  = (k' , v') ∷ (insert k v ps)

lemma : (k v : ℕ) → (ps : List (ℕ × ℕ)) → let keys = getKeys ps
ps'  = insert k v ps
in
k ∈ keys → getKeys ps' ≡ keys

lemma _ _ []               ()
lemma k _ ((k' , _) ∷ ps)  (here k=k')  with  k ≟ k'
...                                     | yes _   =  PE.refl
...                                     | no k≉k' =  ⊥-elim (k≉k' k=k')

lemma k v ((k' , v') ∷ ps) (there k∈ks)  with  k ≟ k'
... |
yes k=k' =  PE.refl
... | no k≢k'  =  goal
where
ps'     = (k' , v') ∷ ps
ins-ps' = insert k v ps'
ks      = getKeys ps
ins-ps  = insert k v ps

keys-ins-ps'=k':keys-ins-ps :
getKeys ins-ps' ≡ k' ∷ (getKeys ins-ps)
keys-ins-ps'=k':keys-ins-ps  with  k ≟ k'
...                         | no _     =  PE.refl
...                         | yes k=k' =  ⊥-elim (k≢k' k=k')

goal : getKeys ins-ps' ≡ k' ∷ ks
-- (map proj₁ (insert k v ((k' , v') ∷ ps)) ≡ k' ∷ ks)
goal =
≡begin
getKeys ins-ps'         ≡[ keys-ins-ps'=k':keys-ins-ps  ]
k' ∷ (getKeys ins-ps)   ≡[ PE.cong (_∷_ k')
(lemma k v ps k∈ks) ]
k' ∷ ks
≡end
---------------------------------------------------------------------------

Development Agda of November ~20 2013 MAlonzo

finds that everything is correct -- except that the last branch of
... | no k≢k'  =

must have the goal type different to  getKeys ins-ps' ≡ k' ∷ ks
It reports
"
map (λ r → proj₁ r) (insert k v ((k' , v') ∷ ps) | k Nat.≟ k') !=
k' ∷ map (λ r → proj₁ r) (insert k v ps) of type List ℕ
when checking that the expression goal has type
map (λ r → proj₁ r) (insert k v ((k' , v') ∷ ps) | no k≢k') ≡
k' ∷ map (λ r → proj₁ r) ps
"

Normalizing the last type expression in the report gives
{-
map proj₁ (insert k v ((k' , v') ∷ ps) | no k≢k') ≡
k' ∷ map proj₁ ps
-->
getKeys (insert k v ps' | no k≢k')  ≡  k' ∷ getKeys ps
-->
getKeys (ins-ps' | no k≢k')  ≡  k' ∷ ks
-}

It differs from the  `goal'  type only in adding   "| no k≢k' ".

1) I do not see what is wrong in my program.
2) How to fix?

Thank you in advance for explanation,

------
Sergei

```