[Agda] the recursive definition can not terminate

[mo jia]

While no one answer my question.( I think it is my problem to ask such question)
Finally I work out this problem.
After read https://plfa.github.io/Isomorphism/ I find the `Bin` can
have some same property like Nat
(comm and distrib and +-suc)

What I learn so for:
1. `cong` should apply on a small step ( If left side is (x0 x) you
should cong on (x) ). Otherwise it will not terminate)
2. `inc-b+` is the key to do the problem. So we need to understand the
"Isomorphism" and learn to find the same property (this example is
`+-suc`)

Well. I post my solution and appreciate for any suggestion.


On Thu, Sep 12, 2019 at 6:08 PM mo jia <life.130815 at gmail.com> wrote:
>
> Hi.
>
> I am doing the exercise from the chapter 3 in https://plfa.github.io/Relations/.
>
> The last one:
>
> Can x
> ---------------
> to (from x) ≡ x
>
> seem too difficult for me using what the book said in first 3 chapters.
>
> I have the last try:  use t1 and t2  recursive declaration.
>
> I got error like this:
>
> Termination checking failed for the following functions:
>   t2, t1
> Problematic calls:
>   t1 (x1 x) x1 cx One1
>     (at /Users/jiamo/agda/ylib/src/ylib/can.agda:146,39-41)
>   t2 (x0 x) x0 cx One1
>     (at /Users/jiamo/agda/ylib/src/ylib/can.agda:156,30-32)
>
> The total agda file is self-sufficiency for someone have interest to
> have a look.
>
> https://gist.github.com/jiamo/af8cd8dd5a4702f81ca6dde04f8e00de
>
> And I still wonder this problem should have a very simple answer like
> what I do for
>
> can_inc : ∀ {x : Bin}
> → Can x
> -------------
> → Can (inc x)
> can_inc {_} (Can_One cx) = Can_One(one_inc cx)
> can_inc { (x0 nil) } (Can_Zero) = Can_One(One1)
>
> Appreciate for any suggestion.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: can.agda
Type: application/octet-stream
Size: 10777 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190919/72fb9ae4/attachment.obj>