
<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">I proved your lemma as following:</p>

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

</p>

<p style="margin-top:0;margin-bottom:0"></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></p>

<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="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 4, 2018 8:01:16 PM<br>

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

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

<div> </div>

</div>

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

<div class="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>

Agda@lists.chalmers.se<br>

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

</div>

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

</body>

</html>