[Agda] struggling `with'

Andrea Vezzosi sanzhiyan at gmail.com
Fri Jan 2 20:47:40 CET 2015


Only one match wasn't enough, but inspect and rewrite help to keep the
code short anyway :)

  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
    where
    ins  = insertWithKey comb
    kv   = (k , v)
    ku   = (k , u)
    k'w  = (k' , w)
    ckuw = comb k u w
    ckvu = comb k v u

    prove : ins kv (ins ku (k'w ∷ ps)) =pn ins (k , comb k v u) (k'w ∷ ps)
    prove with k ≟ k' | PE.inspect (_≟_ k) k'
    prove     | yes p | PE.[ eq ] rewrite eq = e0 ∷pn =pn-refl
      where
      e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)
      e0 = (≈refl , sym-assoc-comb)

    prove     | no ¬p | PE.[ eq ] rewrite eq = =p-refl ∷pn e0
      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

Cheers,
Andrea

On Fri, Jan 2, 2015 at 8:15 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
>
> 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'
>
> -------------------------------------------------------------------------------
>
>
>
>


More information about the Agda mailing list