<div dir="ltr"><div>Sergei,<br><br></div>It might be helpful if you posted full code examples using <a href="http://lpaste.net">lpaste.net</a>. It has a nice syntax highlighting and is easier to extract to a file than copy / paste from email.<br><br><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">And I need to find out what is `inspect'.<br></blockquote><div><br></div><div>"inspect" can be found living in Relation.Binary.Propositional equality, and is a nifty little trick to remember that a with term <font face="monospace,monospace">w<font face="arial,helvetica,sans-serif"> was originally equal to <span style="font-family:monospace,monospace">f x</span>.</font></font> Here's an example:<br><br><a href="http://lpaste.net/117700">http://lpaste.net/117700</a><br><br></div><div>When proving <br><pre><span class="">filter</span><span class="">-</span><span class="">All</span> <span class="">:</span> <span class=""> ∀ {A : Set} → (p : A → Bool) → (xs : List A) → <br> All (λ x → p x ≡ true) (filter p xs)<br></span></pre><pre><span class=""><font face="arial,helvetica,sans-serif">After doing analysis on <span style="font-family:monospace,monospace">xs</span> and moving to a cons case, we find we need to analyze <span style="font-family:monospace,monospace">p x</span> in order to continue.<br><br><span style="font-family:monospace,monospace">filter-All p (x ∷ xs) = {!!}<br>--Goal: All (λ x₁ → p x₁ ≡ true) (if p x then x ∷ filter p xs else filter p xs)</span><br></font></span></pre><pre><span class=""><font face="arial,helvetica,sans-serif">However after we get to the true case and are ready to construct an element of <span style="font-family:monospace,monospace">All</span> with <span style="font-family:monospace,monospace">_</span></font></span><span style="font-family:monospace,monospace"><span class="">∷_<font face="arial,helvetica,sans-serif">, Agda seems to have forgotten why we were <br>here in first place!<br><br></font></span><span class="">filter-All p (x ∷ xs) with p x<br>filter-All p (x ∷ xs) | true = {!!} ∷ (filter-All p xs)<br>-- Goal: p x ≡ true<br></span></span></pre><pre><span style="font-family:monospace,monospace"><span class=""><font face="arial,helvetica,sans-serif">We can use inspect to remind Agda.<br><br><font face="monospace,monospace">filter-All p (x ∷ xs) with p x | inspect p x<br>filter-All p (x ∷ xs) | true | Reveal_is_.[ eq ] = eq ∷ (filter-All p xs)</font><br></font></span></span></pre><pre><span style="font-family:monospace,monospace"><span class=""><font face="arial,helvetica,sans-serif"></font></span></span></pre></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Jan 3, 2015 at 7:19 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, 2015-01-02 at 20:47 +0100, Andrea Vezzosi wrote:<br>
> Only one match wasn't enough, but inspect and rewrite help to keep the<br>
> code short anyway :)<br>
><br>
<br>
</span>This looks good!<br>
Thank you very much.<br>
And I need to find out what is `inspect'.<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<br>
> ins-kv∘ins-ku-eq _ k _ _ [] _ with k ≟ k<br>
> ... | yes _ = =pn-refl<br>
> ... | no k≉k = ⊥-elim $ k≉k ≈refl<br>
><br>
> ins-kv∘ins-ku-eq comb k u v ((k' , w) ∷ ps) sym-assoc-comb = prove<br>
> where<br>
> ins = insertWithKey comb<br>
> kv = (k , v)<br>
> ku = (k , u)<br>
> k'w = (k' , w)<br>
> ckuw = comb k u w<br>
> ckvu = comb k v u<br>
><br>
> prove : ins kv (ins ku (k'w ∷ ps)) =pn ins (k , comb k v u) (k'w ∷ ps)<br>
> prove with k ≟ k' | PE.inspect (_≟_ k) k'<br>
> prove | yes p | PE.[ eq ] rewrite eq = e0 ∷pn =pn-refl<br>
> where<br>
> e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)<br>
> e0 = (≈refl , sym-assoc-comb)<br>
><br>
> prove | no ¬p | PE.[ eq ] rewrite eq = =p-refl ∷pn e0<br>
> where<br>
> e0 : (ins kv (ins ku ps)) =pn (ins (k , ckvu) ps)<br>
> e0 = ins-kv∘ins-ku-eq comb k u v ps sym-assoc-comb<br>
><br>
> Cheers,<br>
> Andrea<br>
><br>
> On Fri, Jan 2, 2015 at 8:15 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br>
> ><br>
> > On Fri, 2015-01-02 at 16:51 +0100, Andrea Vezzosi wrote:<br>
> >> It's really hard to see what's going on without being able to load the<br>
> >> code, and with a lot of it omitted.<br>
> >><br>
> >> We need at least the definition of "ins" and the original type of<br>
> >> "foo", then we might be able to figure out a better type for the two<br>
> >> alternatives, so that the splitting on (k ≟ k') only needs to be done<br>
> >> once.<br>
> >><br>
> ><br>
> > Here follows the full code. It occurs small.<br>
> ><br>
> > I am grateful to anyone who shows how to write<br>
> > ins-kv∘ins-ku-eq<br>
> > in a nicer way.<br>
> ><br>
> > ------<br>
> > Sergei<br>
> ><br>
> ><br>
> ><br>
> > --**********************************************************************<br>
> > module AssocList where<br>
> > open import Level using (Level)<br>
> > open import Function using (_$_; case_of_)<br>
> > open import Relation.Nullary using (¬_; Dec; yes; no)<br>
> > open import Relation.Unary using (Decidable)<br>
> > open import Relation.Binary using<br>
> > (Rel; _⇒_; Reflexive; Symmetric; Transitive; IsEquivalence;<br>
> > module IsEquivalence; Setoid; module Setoid; module DecSetoid;<br>
> > DecSetoid<br>
> > )<br>
> > open import Relation.Binary.PropositionalEquality as PE using (_≡_)<br>
> > import Relation.Binary.EqReasoning as EqR<br>
> > open import Data.Empty using (⊥; ⊥-elim)<br>
> > open import Data.Product using (_×_; _,_)<br>
> > open import Relation.Binary.Product.Pointwise using (_×-setoid_)<br>
> > open import Data.List using (List; []; _∷_)<br>
> > open import Relation.Binary.List.Pointwise as Pointwise using ()<br>
> > renaming ([] to []pn; _∷_ to _∷pn_)<br>
> ><br>
> > -----------------------------------------------------------------------<br>
> > module _ {α α= β β= : Level} (keyDSetoid : DecSetoid α α=)<br>
> > (valSetoid : Setoid β β=)<br>
> > where<br>
> > open DecSetoid keyDSetoid using (_≈_; _≟_; setoid) renaming<br>
> > (Carrier to K; isEquivalence to kEquiv)<br>
> > open IsEquivalence kEquiv using ()<br>
> > renaming (refl to ≈refl; sym to ≈sym; trans to ≈trans)<br>
> ><br>
> > open Setoid valSetoid using () renaming (Carrier to V; _≈_ to _=v_;<br>
> > isEquivalence to vEquiv)<br>
> > open IsEquivalence vEquiv using ()<br>
> > renaming (refl to =v-refl; sym to =v-sym; trans to =v-trans;<br>
> > reflexive to =v-reflexive)<br>
> ><br>
> > pairSetoid = setoid ×-setoid valSetoid -- for K × V<br>
> > open Setoid pairSetoid using () renaming (Carrier to KV; _≈_ to _=p_;<br>
> > isEquivalence to pEquiv)<br>
> > open IsEquivalence pEquiv using ()<br>
> > renaming (refl to =p-refl; sym to =p-sym; trans to =p-trans;<br>
> > reflexive to =p-reflexive)<br>
> ><br>
> > point-p-setoid = Pointwise.setoid pairSetoid<br>
> > open Setoid point-p-setoid using ()<br>
> > renaming (_≈_ to _=pn_; isEquivalence to pnEquiv)<br>
> > -- "pn" stands for "pointwise for List KV"<br>
> ><br>
> > open IsEquivalence pnEquiv using ()<br>
> > renaming (refl to =pn-refl; reflexive to =pn-reflexive;<br>
> > sym to =pn-sym)<br>
> > open module EqR-pn = EqR point-p-setoid<br>
> > renaming (begin_ to begin-pn_; _∎ to _end-pn; _≈⟨_⟩_ to _=pn[_]_)<br>
> ><br>
> ><br>
> > -------------------------------------------------------------------<br>
> > Pairs : Set _<br>
> > Pairs = List KV<br>
> ><br>
> > CombineKVV : Set _ -- (α ⊔ β)<br>
> > CombineKVV = K → V → V → V<br>
> ><br>
> > ----------------------------------------------------------------------<br>
> > insertWithKey : CombineKVV → KV → Pairs → Pairs<br>
> > -- \key newV oldV |→ resV<br>
> ><br>
> > insertWithKey _ p [] = p ∷ []<br>
> > insertWithKey comb (k , new) ((k' , old) ∷ ps) =<br>
> > case k ≟ k'<br>
> > of \<br>
> > { (yes _) → (k' , comb k new old) ∷ ps<br>
> > ; (no _) → (k' , old) ∷ (insertWithKey comb (k , new) ps) }<br>
> ><br>
> > ----------------------------------------------------------------------<br>
> > ins-kv∘ins-ku-eq :<br>
> > (comb : CombineKVV) → ∀ k u v ps →<br>
> > (∀ {w} → comb k v (comb k u w) =v comb k (comb k v u) w) →<br>
> > let ins = insertWithKey comb<br>
> > in<br>
> > ins (k , v) (ins (k , u) ps) =pn ins (k , comb k v u) ps<br>
> ><br>
> > -- Example: it fits comb _ u v = f u v with any Associative f.<br>
> ><br>
> > ins-kv∘ins-ku-eq _ k _ _ [] _ with k ≟ k<br>
> > ... | yes _ = =pn-refl<br>
> > ... | no k≉k = ⊥-elim $ k≉k ≈refl<br>
> ><br>
> > ins-kv∘ins-ku-eq comb k u v ((k' , w) ∷ ps) sym-assoc-comb =<br>
> > prove (k ≟ k')<br>
> > where<br>
> > ins = insertWithKey comb<br>
> > kv = (k , v)<br>
> > ku = (k , u)<br>
> > k'w = (k' , w)<br>
> > ckuw = comb k u w<br>
> > ckvu = comb k v u<br>
> ><br>
> > -------------------------------------------------------------------<br>
> > case≈ : k ≈ k' →<br>
> > ins kv (ins ku (k'w ∷ ps)) =pn ins (k , ckvu) (k'w ∷ ps)<br>
> ><br>
> > case≈ k≈k' =<br>
> > begin-pn<br>
> > ins kv (ins ku (k'w ∷ ps)) =pn[ =pn-reflexive $<br>
> > PE.cong (ins kv) e1<br>
> > ]<br>
> > ins kv ((k' , ckuw) ∷ ps) =pn[ =pn-reflexive e2 ]<br>
> > (k' , comb k v ckuw) ∷ ps =pn[ e0 ∷pn =pn-refl ]<br>
> > (k' , comb k ckvu w) ∷ ps =pn[ =pn-reflexive $ PE.sym e3 ]<br>
> > ins (k , ckvu) (k'w ∷ ps)<br>
> > end-pn<br>
> > where<br>
> > e0 : (k' , comb k v ckuw) =p (k' , comb k ckvu w)<br>
> > e0 = (≈refl , sym-assoc-comb)<br>
> ><br>
> > e1 : ins ku ((k' , w) ∷ ps) ≡ (k' , ckuw) ∷ ps<br>
> > e1 with k ≟ k'<br>
> > ... | yes _ = PE.refl<br>
> > ... | no k≉k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > e2 : ins kv ((k' , ckuw) ∷ ps) ≡ (k' , comb k v ckuw) ∷ ps<br>
> > e2 with k ≟ k'<br>
> > ... | yes _ = PE.refl<br>
> > ... | no k≉k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > e3 : ins (k , ckvu) (k'w ∷ ps) ≡ (k' , comb k ckvu w) ∷ ps<br>
> > e3 with k ≟ k'<br>
> > ... | yes _ = PE.refl<br>
> > ... | no k≉k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > -------------------------------------------------------------------<br>
> > case≉ : ¬ k ≈ k' →<br>
> > ins kv (ins ku (k'w ∷ ps)) =pn ins (k , ckvu) (k'w ∷ ps)<br>
> ><br>
> > case≉ k≉k' =<br>
> > begin-pn<br>
> > ins kv (ins ku (k'w ∷ ps)) =pn[ =pn-reflexive $<br>
> > PE.cong (ins kv) e1 ]<br>
> > ins kv (k'w ∷ (ins ku ps)) =pn[ =pn-reflexive e2 ]<br>
> > k'w ∷ (ins kv $ ins ku ps) =pn[ =p-refl ∷pn e0 ]<br>
> > k'w ∷ (ins (k , ckvu) ps) =pn[ =pn-reflexive e3 ]<br>
> > ins (k , ckvu) (k'w ∷ ps)<br>
> > end-pn<br>
> > where<br>
> > e0 : (ins kv (ins ku ps)) =pn (ins (k , ckvu) ps)<br>
> > e0 = ins-kv∘ins-ku-eq comb k u v ps sym-assoc-comb<br>
> ><br>
> > e1 : ins ku (k'w ∷ ps) ≡ k'w ∷ (ins ku ps)<br>
> > e1 with k ≟ k'<br>
> > ... | no _ = PE.refl<br>
> > ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > e2 : ins kv (k'w ∷ ins ku ps) ≡ k'w ∷ (ins kv $ ins ku ps)<br>
> > e2 with k ≟ k'<br>
> > ... | no _ = PE.refl<br>
> > ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > e3 : k'w ∷ (ins (k , ckvu) ps) ≡ ins (k , ckvu) (k'w ∷ ps)<br>
> > e3 with k ≟ k'<br>
> > ... | no _ = PE.refl<br>
> > ... | yes k≈k' = ⊥-elim $ k≉k' k≈k'<br>
> ><br>
> > -----------------------------------------------------------------<br>
> > prove : Dec (k ≈ k') → ins kv (ins ku (k'w ∷ ps)) =pn<br>
> > ins (k , comb k v u) (k'w ∷ ps)<br>
> > prove (no k≉k') = case≉ k≉k'<br>
> > prove (yes k≈k') = case≈ k≈k'<br>
> ><br>
> > -------------------------------------------------------------------------------<br>
> ><br>
> ><br>
> ><br>
> ><br>
><br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br><div class="gmail_signature"><div dir="ltr"><div>Christopher Jenkins<br>Computer Science 2013<br>Trinity University</div></div></div>
</div>