<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>Jason,</p>
<p><br>
</p>
<p>Thanks again for pointing me in the right direction on this. <br>
</p>
<p><br>
</p>
<p>To answer your questions :</p>
<p><br>
</p>
<p>1. By your case analysis I mean "a priori" rather than from using
pattern matching. <br>
</p>
<p><br>
</p>
<p>2. Now that I have some experience I see that pattern matching in
2.5.3 generated the inductive term</p>
<p><br>
</p>
<p>mapid' (x ,- xs) | x₁ ,- xss | s = {!s!} <br>
</p>
<p><br>
</p>
<p>which required reduction on s to generate <br>
</p>
<p><br>
</p>
<p>mapid' (x ,- .(x₁ ,- xss)) | x₁ ,- xss<br>
| refl .((x₁ ,- xss) ,- []) = refl ((x ,- (x₁ ,- xss)) ,- []) <br>
</p>
<p><br>
</p>
<p>which matches your inductive term modulo renaming.</p>
<p><br>
</p>
<p>Thanks again. I'm good for now.<br>
</p>
<p><br>
</p>
<p>--</p>
<p>Rick<br>
</p>
<br>
<div class="moz-cite-prefix">On 07/05/2018 08:25 PM, Jason -Zhong
Sheng- Hu wrote:<br>
</div>
<blockquote type="cite"
cite="mid:YTXPR0101MB1472F96A626CBD1F75DEC777AF470@YTXPR0101MB1472.CANPRD01.PROD.OUTLOOK.COM">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
<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</b></span></span></font> </div>
</div>
</div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt"
color="#000000" face="Calibri, sans-serif"><b>From:</b> Agda
<a class="moz-txt-link-rfc2396E" href="mailto:agda-bounces@lists.chalmers.se"><agda-bounces@lists.chalmers.se></a> on behalf of rick
<a class="moz-txt-link-rfc2396E" href="mailto:rick@rickmurphy.org"><rick@rickmurphy.org></a><br>
<b>Sent:</b> July 5, 2018 7:32:39 PM<br>
<b>To:</b> <a class="moz-txt-link-abbreviated" href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a><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 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</b></span></span></font> </div>
</div>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="x_divRplyFwdMsg" dir="ltr"><font
style="font-size:11pt" color="#000000" face="Calibri,
sans-serif"><b>From:</b> Agda
<a class="x_moz-txt-link-rfc2396E"
href="mailto:agda-bounces@lists.chalmers.se"
moz-do-not-send="true"><agda-bounces@lists.chalmers.se></a>
on behalf of rick
<a class="x_moz-txt-link-rfc2396E"
href="mailto:rick@rickmurphy.org" moz-do-not-send="true"><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"
moz-do-not-send="true">
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"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a
href="https://lists.chalmers.se/mailman/listinfo/agda"
moz-do-not-send="true">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>
</blockquote>
<br>
<pre class="moz-signature" cols="72">--
rick</pre>
</body>
</html>