
<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=ks_c_5601-1987">

<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>

</head>

<body dir="ltr">

<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;font-family:Calibri,Helvetica,sans-serif;" dir="ltr">

<p style="margin-top:0;margin-bottom:0">Hi Rick,</p>

<p style="margin-top:0;margin-bottom:0"><br>

</p>

<p style="margin-top:0;margin-bottom:0">what do you mean by "my case analysis"? Are you saying the definition does not work in 2.5.3? I am indeed using 2.6 but I am not sure version matters here.</p>

<p style="margin-top:0;margin-bottom:0"><br>

</p>

<div id="Signature">

<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif, "EmojiFont", "Apple Color Emoji", "Segoe UI Emoji", NotoColorEmoji, "Segoe UI Symbol", "Android Emoji", EmojiSymbols;">

<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>

</b></span></span></font></div>

<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>

Jason Hu<a target="_blank" id="LPNoLP"></a></b></span></span></font> </div>

</div>

</div>

<hr style="display:inline-block;width:98%" tabindex="-1">

<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of rick <rick@rickmurphy.org><br>

<b>Sent:</b> July 5, 2018 7:32:39 PM<br>

<b>To:</b> agda@lists.chalmers.se<br>

<b>Subject:</b> Re: [Agda] unification using more complex with abstractions</font>

<div> </div>

</div>

<meta content="text/html; charset=utf-8">

<div style="background-color:#FFFFFF">

<p>Thanks Jason. That gives me a place to start.</p>

<p><br>

</p>

<p>I am working through some examples and will ask a few more questions next week.<br>

</p>

<p><br>

</p>

<p>BTW - That's your case analysis, right? The pattern matching I get from 2.5.3 is different.<br>

</p>

<p><br>

</p>

<p>--</p>

<p>Rick<br>

</p>

<br>

<div class="x_moz-cite-prefix">On 07/04/2018 08:41 PM, Jason -Zhong Sheng- Hu wrote:<br>

</div>

<blockquote type="cite"><style type="text/css" style="display:none">

<!--

p

        {margin-top:0;

        margin-bottom:0}

-->

</style>

<div id="x_divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Helvetica,sans-serif">

<p style="margin-top:0; margin-bottom:0">Hi rick,</p>

<p style="margin-top:0; margin-bottom:0"><br>

</p>

<p style="margin-top:0; margin-bottom:0">I proved your lemma as following:</p>

<p style="margin-top:0; margin-bottom:0"><br>

</p>

<div><span style="font-family:"Courier New",monospace">mapid' : вг {X : Set} -> (xs : List X) -> wrap (mapList id xs) == wrap xs</span><br>

<span style="font-family:"Courier New",monospace">mapid' [] = refl ([] ,- [])</span><br>

<span style="font-family:"Courier New",monospace">mapid' (x ,- xs) with mapList id xs | mapid' xs</span><br>

<span style="font-family:"Courier New",monospace">mapid' (x ,- []) | [] | _ = refl ((x ,- []) ,- [])</span><br>

<span style="font-family:"Courier New",monospace">mapid' (x ,- (xй√ ,- xs)) | [] | ()</span><br>

<span style="font-family:"Courier New",monospace">mapid' (x ,- []) | y ,- ys | ()</span><br>

<span style="font-family:"Courier New",monospace">mapid' (x ,- (xй√ ,- xs)) | y ,- ys | refl _ = refl _</span><br>

<br>

</div>

<p style="margin-top:0; margin-bottom:0">There are a number of points here why agda doesn't want to unify your previous terms:</p>

<p style="margin-top:0; margin-bottom:0"><br>

</p>

<ol style="margin-bottom:0px; margin-top:0px">

<li>the wrap is done by (unnecessary) induction. For agda to proceed, you must break the cases, such that the computation rules can proceed and allow you to unify terms(as in the last line). If wrap is defined in the straightforward way, it's easier to prove;

</li><li>In the inductive case, the inductive hypothesis is not directly applicable. You can press C-u C-u C-, to look at normalized term to see why it's the case.<br>

</li><li>I don't know why you add a condition (id x == x). to begin with, Agda is able to figure out `id x` definitionally equals to `x`. You pattern match it to refl in your proof of `mapid`, and that means you are using K when it's not necessary.<br>

</li></ol>

<p style="margin-top:0; margin-bottom:0"><br>

</p>

<div id="x_Signature">

<div id="x_divtagdefaultwrapper" dir="ltr" style="">

<div><font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>

</b></span></span></font></div>

<font size="3" style="font-size:12pt"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>

Jason Hu</b></span></span></font> </div>

</div>

</div>

<hr tabindex="-1" style="display:inline-block; width:98%">

<div id="x_divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" color="#000000" style="font-size:11pt"><b>From:</b> Agda

<a class="x_moz-txt-link-rfc2396E" href="mailto:agda-bounces@lists.chalmers.se"><agda-bounces@lists.chalmers.se></a> on behalf of rick

<a class="x_moz-txt-link-rfc2396E" href="mailto:rick@rickmurphy.org"><rick@rickmurphy.org></a><br>

<b>Sent:</b> July 4, 2018 8:01:16 PM<br>

<b>To:</b> <a class="x_moz-txt-link-abbreviated" href="mailto:agda@lists.chalmers.se">

agda@lists.chalmers.se</a><br>

<b>Subject:</b> [Agda] unification using more complex with abstractions</font>

<div> </div>

</div>

<div class="x_BodyFragment"><font size="2"><span style="font-size:11pt">

<div class="x_PlainText">I am able to use simple with and rewrite expressions like the following:<br>

<br>

data List (X : Set) : Set where<br>

  [] : List X<br>

  _,-_ : (x : X)(xs : List X) -> List X<br>

<br>

mapList : {X Y : Set} -> (X -> Y) -> List X -> List Y<br>

mapList f [] = []<br>

mapList f (x ,- xs) = f x ,- mapList f xs<br>

<br>

id : {X : Set} -> X -> X<br>

id x = x<br>

<br>

data _==_ {X : Set} : X -> X -> Set where<br>

  refl : (x : X) -> x == x<br>

<br>

{-# BUILTIN EQUALITY _==_ #-}<br>

<br>

mapid : вг {X : Set} {x : X} -> (id x == x)<br>

   -> (xs : List X) -> mapList id xs == xs<br>

mapid p [] = refl []<br>

mapid p (x ,- xs) with mapList id xs | mapid p xs<br>

mapid (refl xй√) (x ,- xs) | .xs | refl .xs = refl (x ,- xs)<br>

<br>

I proved the same result using rewrite.<br>

<br>

Now I am building intuition around more complex with abstractions. For <br>

example I am trying to prove the following :<br>

<br>

[_] : {X : Set} -> X -> List X<br>

[ x ] = x ,- []<br>

<br>

wrap : вг{A} -> List A -> List (List A)<br>

wrap [] = [ [] ]<br>

wrap (x ,- xs) = [ x ,- xs ]<br>

<br>

mapid' : вг {X : Set} {x : X} -> (id x == x)<br>

   -> (xs : List X) -> wrap (mapList id xs) == wrap xs<br>

mapid' p [] = refl [ [] ]<br>

mapid' p (xs ,- xss) with wrap (mapList id xss) | mapid' p xss<br>

mapid' (refl x) (xs ,- xss) | .(wrap xss) | refl .(wrap xss) = {! ((xs <br>

,- mapList (еы xй√ бц xй√) xss) ,- []) == ((xs ,- xss) ,- []) !}<br>

<br>

I have only added a layer around the previous reflexive proof using <br>

wrap. However, the goal no longer unifies the more complex expression <br>

listed in the goal.<br>

<br>

How do I proceed with these more complex expressions?<br>

<br>

-- <br>

rick<br>

<br>

_______________________________________________<br>

Agda mailing list<br>

<a class="x_moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>

<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>

</div>

</span></font></div>

</blockquote>

<br>

<pre class="x_moz-signature" cols="72">-- 

rick</pre>

</div>

</body>

</html>