[Agda] struggling `with'

[Sergei Meshveliani]

On Fri, 2015-01-02 at 16:51 +0100, Andrea Vezzosi wrote:
> It's really hard to see what's going on without being able to load the
> code, and with a lot of it omitted.
> 
> We need at least the definition of "ins" and the original type of
> "foo", then we might be able to figure out a better type for the two
> alternatives, so that the splitting on (k ≟ k') only needs to be done
> once.
> 

Here follows the full code. It occurs small.

I am grateful to anyone who shows how to write 
                                         ins-kv∘ins-ku-eq 
in a nicer way.

------
Sergei



--**********************************************************************
module AssocList where 
open import Level    using (Level) 
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 
     (Rel; _⇒_; Reflexive; Symmetric; Transitive; IsEquivalence;
      module IsEquivalence; Setoid; module Setoid; module DecSetoid; 
      DecSetoid 
     )
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
import Relation.Binary.EqReasoning as EqR
open import Data.Empty   using (⊥; ⊥-elim)
open import Data.Product using (_×_;  _,_)
open import Relation.Binary.Product.Pointwise using (_×-setoid_)
open import Data.List using (List; []; _∷_)
open import Relation.Binary.List.Pointwise as Pointwise using ()
                                   renaming ([] to []pn; _∷_ to _∷pn_)

-----------------------------------------------------------------------
module _ {α α= β β= : Level} (keyDSetoid : DecSetoid α α=)
                             (valSetoid  : Setoid β β=)
  where
  open DecSetoid keyDSetoid using (_≈_; _≟_; setoid) renaming 
                                (Carrier to K; isEquivalence to kEquiv)
  open IsEquivalence kEquiv using () 
                renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)

  open Setoid valSetoid using () renaming (Carrier to V; _≈_ to _=v_;
                                               isEquivalence to vEquiv)
  open IsEquivalence vEquiv using () 
           renaming (refl to =v-refl; sym to =v-sym; trans to =v-trans;
                                             reflexive to =v-reflexive)

  pairSetoid = setoid ×-setoid valSetoid                  -- for  K × V
  open Setoid pairSetoid using () renaming (Carrier to KV; _≈_ to _=p_;
                                              isEquivalence to pEquiv) 
  open IsEquivalence pEquiv using () 
          renaming (refl to =p-refl; sym to =p-sym; trans to =p-trans; 
                                             reflexive to =p-reflexive)

  point-p-setoid = Pointwise.setoid pairSetoid  
  open Setoid point-p-setoid using () 
                      renaming (_≈_ to _=pn_; isEquivalence to pnEquiv)
  -- "pn" stands for "pointwise for List KV"

  open IsEquivalence pnEquiv using () 
               renaming (refl to =pn-refl; reflexive to =pn-reflexive; 
                                                 sym to =pn-sym)   
  open module EqR-pn = EqR point-p-setoid
      renaming (begin_ to begin-pn_; _∎ to _end-pn; _≈⟨_⟩_ to _=pn[_]_)


  -------------------------------------------------------------------
  Pairs : Set _
  Pairs = List KV

  CombineKVV : Set _  -- (α ⊔ β)
  CombineKVV = K → V → V → V

  ----------------------------------------------------------------------
  insertWithKey : CombineKVV →  KV → Pairs → Pairs
               -- \key newV oldV |→ resV

  insertWithKey _    p         []                =  p ∷ []
  insertWithKey comb (k , new) ((k' , old) ∷ ps) =
        case k ≟ k'
        of \
        { (yes _) → (k' , comb k new old) ∷ ps
        ; (no _)  → (k' , old) ∷ (insertWithKey comb (k , new) ps) }

  ----------------------------------------------------------------------
  ins-kv∘ins-ku-eq :
             (comb : CombineKVV) → ∀ k u v ps →
             (∀ {w} → comb k v (comb k u w) =v comb k (comb k v u) w) →
             let ins = insertWithKey comb 
             in
             ins (k , v) (ins (k , u) ps)  =pn  ins (k , comb k v u) ps

  -- Example:  it fits  comb _ u v = f u v   with any Associative f.

  ins-kv∘ins-ku-eq _    k _ _ []   _  with k ≟ k
  ...                                     | yes _  =  =pn-refl
  ...                                     | no k≉k =  ⊥-elim $ k≉k ≈refl

  ins-kv∘ins-ku-eq comb k u v ((k' , w) ∷ ps) sym-assoc-comb =  
                                                        prove (k ≟ k')
    where
    ins  = insertWithKey comb 
    kv   = (k , v)
    ku   = (k , u)
    k'w  = (k' , w) 
    ckuw = comb k u w
    ckvu = comb k v u

    -------------------------------------------------------------------
    case≈ : k ≈ k' →
            ins kv (ins ku (k'w ∷ ps)) =pn ins (k , ckvu) (k'w ∷ ps)

    case≈ k≈k' =  
      begin-pn
        ins kv (ins ku (k'w ∷ ps))   =pn[ =pn-reflexive $ 
                                          PE.cong (ins kv) e1
                                        ]
        ins kv ((k' , ckuw) ∷ ps)    =pn[ =pn-reflexive e2 ]
        (k' , comb k v ckuw) ∷ ps    =pn[ e0 ∷pn =pn-refl ]
        (k' , comb k ckvu w) ∷ ps    =pn[ =pn-reflexive $ PE.sym e3 ]
        ins (k , ckvu) (k'w ∷ ps)
      end-pn
      where
      e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)
      e0 = (≈refl , sym-assoc-comb)

      e1 :  ins ku ((k' , w) ∷ ps) ≡ (k' , ckuw) ∷ ps   
      e1 with k ≟ k' 
      ... | yes _   = PE.refl
      ... | no k≉k' = ⊥-elim $ k≉k' k≈k'

      e2 :  ins kv ((k' , ckuw) ∷ ps) ≡ (k' , comb k v ckuw) ∷ ps 
      e2 with k ≟ k' 
      ... | yes _   = PE.refl
      ... | no k≉k' = ⊥-elim $ k≉k' k≈k'

      e3 :  ins (k , ckvu) (k'w ∷ ps) ≡ (k' , comb k ckvu w) ∷ ps    
      e3 with k ≟ k' 
      ... | yes _   = PE.refl
      ... | no k≉k' = ⊥-elim $ k≉k' k≈k'

    -------------------------------------------------------------------
    case≉ : ¬ k ≈ k' → 
            ins kv (ins ku (k'w ∷ ps))  =pn  ins (k , ckvu) (k'w ∷ ps)
  
    case≉ k≉k' = 
      begin-pn  
        ins kv (ins ku (k'w ∷ ps))      =pn[ =pn-reflexive $
                                              PE.cong (ins kv) e1 ]
         ins kv (k'w ∷ (ins ku ps))     =pn[ =pn-reflexive e2 ]
         k'w ∷ (ins kv $ ins ku ps)     =pn[ =p-refl ∷pn e0 ]
         k'w ∷ (ins (k , ckvu) ps)      =pn[ =pn-reflexive e3 ]
         ins (k , ckvu) (k'w ∷ ps)
      end-pn
      where
      e0 : (ins kv (ins ku ps)) =pn (ins (k , ckvu) ps)
      e0 = ins-kv∘ins-ku-eq comb k u v ps sym-assoc-comb

      e1 : ins ku (k'w ∷ ps) ≡ k'w ∷ (ins ku ps)
      e1 with k ≟ k'
      ... | no _     = PE.refl 
      ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'

      e2 : ins kv (k'w ∷ ins ku ps) ≡ k'w ∷ (ins kv $ ins ku ps)
      e2 with k ≟ k'
      ... | no _     = PE.refl
      ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'

      e3 :  k'w ∷ (ins (k , ckvu) ps) ≡ ins (k , ckvu) (k'w ∷ ps)
      e3 with k ≟ k'
      ... | no _     = PE.refl
      ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'

    -----------------------------------------------------------------
    prove : Dec (k ≈ k') → ins kv (ins ku (k'w ∷ ps)) =pn 
                           ins (k , comb k v u) (k'w ∷ ps)
    prove (no k≉k')  = case≉ k≉k'
    prove (yes k≈k') = case≈ k≈k'

-------------------------------------------------------------------------------