[Agda] unification using more complex with abstractions

[rick]

Jason,


Thanks again for pointing me in the right direction on this.


To answer your questions :


1. By your case analysis I mean "a priori" rather than from using 
pattern matching.


2. Now that I have some experience I see that pattern matching in 2.5.3 
generated the inductive term


mapid' (x ,- xs) | x₁ ,- xss | s = {!s!}


which required reduction on s to generate


mapid' (x ,- .(x₁ ,- xss)) | x₁ ,- xss
   | refl .((x₁ ,- xss) ,- []) = refl ((x ,- (x₁ ,- xss)) ,- [])


which matches your inductive term modulo renaming.


Thanks again. I'm good for now.


--

Rick


On 07/05/2018 08:25 PM, Jason -Zhong Sheng- Hu wrote:
>
> Hi Rick,
>
>
> 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.
>
>
> *Sincerely Yours,
> *
> *
> Jason Hu*
> ------------------------------------------------------------------------
> *From:* Agda <agda-bounces at lists.chalmers.se> on behalf of rick 
> <rick at rickmurphy.org>
> *Sent:* July 5, 2018 7:32:39 PM
> *To:* agda at lists.chalmers.se
> *Subject:* Re: [Agda] unification using more complex with abstractions
>
> Thanks Jason. That gives me a place to start.
>
>
> I am working through some examples and will ask a few more questions 
> next week.
>
>
> BTW - That's your case analysis, right? The pattern matching I get 
> from 2.5.3 is different.
>
>
> --
>
> Rick
>
>
> On 07/04/2018 08:41 PM, Jason -Zhong Sheng- Hu wrote:
>>
>> Hi rick,
>>
>>
>> I proved your lemma as following:
>>
>>
>> mapid' : ∀ {X : Set} -> (xs : List X) -> wrap (mapList id xs) == wrap xs
>> mapid' [] = refl ([] ,- [])
>> mapid' (x ,- xs) with mapList id xs | mapid' xs
>> mapid' (x ,- []) | [] | _ = refl ((x ,- []) ,- [])
>> mapid' (x ,- (x₁ ,- xs)) | [] | ()
>> mapid' (x ,- []) | y ,- ys | ()
>> mapid' (x ,- (x₁ ,- xs)) | y ,- ys | refl _ = refl _
>>
>> There are a number of points here why agda doesn't want to unify your 
>> previous terms:
>>
>>
>>  1. 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;
>>  2. 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.
>>  3. 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.
>>
>>
>> *Sincerely Yours,
>> *
>> *
>> Jason Hu*
>> ------------------------------------------------------------------------
>> *From:* Agda <agda-bounces at lists.chalmers.se> 
>> <mailto:agda-bounces at lists.chalmers.se> on behalf of rick 
>> <rick at rickmurphy.org> <mailto:rick at rickmurphy.org>
>> *Sent:* July 4, 2018 8:01:16 PM
>> *To:* agda at lists.chalmers.se <mailto:agda at lists.chalmers.se>
>> *Subject:* [Agda] unification using more complex with abstractions
>> I am able to use simple with and rewrite expressions like the following:
>>
>> data List (X : Set) : Set where
>>   [] : List X
>>   _,-_ : (x : X)(xs : List X) -> List X
>>
>> mapList : {X Y : Set} -> (X -> Y) -> List X -> List Y
>> mapList f [] = []
>> mapList f (x ,- xs) = f x ,- mapList f xs
>>
>> id : {X : Set} -> X -> X
>> id x = x
>>
>> data _==_ {X : Set} : X -> X -> Set where
>>   refl : (x : X) -> x == x
>>
>> {-# BUILTIN EQUALITY _==_ #-}
>>
>> mapid : ∀ {X : Set} {x : X} -> (id x == x)
>>    -> (xs : List X) -> mapList id xs == xs
>> mapid p [] = refl []
>> mapid p (x ,- xs) with mapList id xs | mapid p xs
>> mapid (refl x₁) (x ,- xs) | .xs | refl .xs = refl (x ,- xs)
>>
>> I proved the same result using rewrite.
>>
>> Now I am building intuition around more complex with abstractions. For
>> example I am trying to prove the following :
>>
>> [_] : {X : Set} -> X -> List X
>> [ x ] = x ,- []
>>
>> wrap : ∀{A} -> List A -> List (List A)
>> wrap [] = [ [] ]
>> wrap (x ,- xs) = [ x ,- xs ]
>>
>> mapid' : ∀ {X : Set} {x : X} -> (id x == x)
>>    -> (xs : List X) -> wrap (mapList id xs) == wrap xs
>> mapid' p [] = refl [ [] ]
>> mapid' p (xs ,- xss) with wrap (mapList id xss) | mapid' p xss
>> mapid' (refl x) (xs ,- xss) | .(wrap xss) | refl .(wrap xss) = {! ((xs
>> ,- mapList (λ x₁ → x₁) xss) ,- []) == ((xs ,- xss) ,- []) !}
>>
>> I have only added a layer around the previous reflexive proof using
>> wrap. However, the goal no longer unifies the more complex expression
>> listed in the goal.
>>
>> How do I proceed with these more complex expressions?
>>
>> -- 
>> rick
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>
> -- 
> rick

-- 
rick

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180718/3a9d83b3/attachment.html>