<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body text="#000000" bgcolor="#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="moz-cite-prefix">On 07/04/2018 08:41 PM, Jason -Zhong
Sheng- Hu wrote:<br>
</div>
<blockquote type="cite"
cite="mid:YTXPR0101MB14724DFEE18E4AC305C39A85AF400@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">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="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"
face="Calibri, sans-serif" color="#000000"><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 4, 2018 8:01:16 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> [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>
<a class="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"
moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</blockquote>
<br>
<pre class="moz-signature" cols="72">--
rick</pre>
</body>
</html>