[Agda] unification using more complex with abstractions

[rick]

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

[Jason -Zhong Sheng- Hu]

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

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

--
rick

[Jason -Zhong Sheng- Hu]

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


--
rick

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

--
rick