[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