[Agda] unification using more complex with abstractions

[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-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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180705/88c89e63/attachment.html>