[Agda] the recursive definition can not terminate

[Andreas Abel]

 > While no one answer my question.( I think it is my problem to ask 
such question)

Yes, we cannot help with exercises for the obvious reason.

And please do not post solutions to exercises publicly, also for the 
obvious reason.

Best, Andreas

On 2019-09-19 14:50, mo jia wrote:
> 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.
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda