[Agda] struggling `with'

Sergei Meshveliani mechvel at botik.ru
Sun Jan 4 11:11:01 CET 2015


I see. Thank you.

------
Sergei


On Sat, 2015-01-03 at 12:05 -0600, Christopher Jenkins wrote:
> Sergei,
> 
> 
> It might be helpful if you posted full code examples using lpaste.net.
> It has a nice syntax highlighting and is easier to extract to a file
> than copy / paste from email.
> 
>         And I need to find out what is `inspect'.
> 
> 
> "inspect" can be found living in Relation.Binary.Propositional
> equality, and is a nifty little trick to remember that a with term w
> was originally equal to f x. Here's an example:
> 
> http://lpaste.net/117700
> 
> 
> When proving 
> filter-All :  ∀ {A : Set} → (p : A → Bool) → (xs : List A) → 
>              All (λ x → p x ≡ true) (filter p xs)
> After doing analysis on xs and moving to a cons case, we find we need to analyze p x in order to continue.
> 
> filter-All p (x ∷ xs) = {!!}
> --Goal: All (λ x₁ → p x₁ ≡ true) (if p x then x ∷ filter p xs else filter p xs)
> However after we get to the true case and are ready to construct an element of All with _∷_, Agda seems to have forgotten why we were 
> here in first place!
> 
> filter-All p (x ∷ xs) with p x
> filter-All p (x ∷ xs) | true = {!!} ∷ (filter-All p xs)
> -- Goal: p x ≡ true
> We can use inspect to remind Agda.
> 
> filter-All p (x ∷ xs) with p x | inspect p x
> filter-All p (x ∷ xs) | true | Reveal_is_.[ eq ] = eq ∷ (filter-All p xs)
> 
> On Sat, Jan 3, 2015 at 7:19 AM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         On Fri, 2015-01-02 at 20:47 +0100, Andrea Vezzosi wrote:
>         > Only one match wasn't enough, but inspect and rewrite help
>         to keep the
>         > code short anyway :)
>         >
>         
>         This looks good!
>         Thank you very much.
>         And I need to find out what is `inspect'.
>         
>         ------
>         Sergei
>         
>         
>         >   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'
>         > >
>         > >
>         -------------------------------------------------------------------------------
>         > >
>         > >
>         > >
>         > >
>         >
>         
>         
>         _______________________________________________
>         Agda mailing list
>         Agda at lists.chalmers.se
>         https://lists.chalmers.se/mailman/listinfo/agda
>         
> 
> 
> 
> -- 
> Christopher Jenkins
> Computer Science 2013
> Trinity University




More information about the Agda mailing list