[Agda] unification using more complex with abstractions

[rick]

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> on behalf of rick 
> <rick at rickmurphy.org>
> *Sent:* July 4, 2018 8:01:16 PM
> *To:* 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
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
rick

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180705/98e184c5/attachment.html>