[Agda] Komencenta demando.

[Andreas Abel]

You can try to help the termination checker by proving the superficially 
more general

proof¹′ : ∀ n m → m ≡ conv⁰→ n → conv⁰← m ≡ n
proof¹′ zero .0 refl = refl
proof¹′ (2k n) m p = {!!}
proof¹′ (2k+1 n) .(suc (conv⁰→ n + conv⁰→ n)) refl = begin
   conv⁰← (conv⁰→ (2k+1 n)) ≡[ refl ]
   conv⁰← (conv⁰→ (suc⁰ (2k n))) ≡[ refl ]
   conv⁰← (suc (conv⁰→ (2k n))) ≡[ refl ]
   suc⁰ (conv⁰← (conv⁰→ (2k n))) ≡[ cong suc⁰ (proof¹′ (2k n) (conv⁰→ n 
+ conv⁰→ n) refl) ]
   suc⁰ (2k n) ≡[ refl ]
   2k+1 n
   ∎

and then get your final result by

proof¹ : ∀ n → conv⁰← (conv⁰→ n) ≡ n
proof¹ n = proof¹′ n (conv⁰→ n) refl

I did not complete the hole you left, so I do not know whether it works 
in the end...

The idea is that Agda can now also use the descent on m, in this case,

   (suc (conv⁰→ n + conv⁰→ n)) > (conv⁰→ n + conv⁰→ n)

to convince herself of termination.

Cheers,
Andreas

On 01.12.2015 22:13, Serge Leblanc wrote:
> open import Data.Nat
> open import Data.Nat.Properties.Simple using (+-comm; +-suc)
> open import Relation.Binary.PropositionalEquality as PropEq using (_≡_;
> refl; cong; cong₂)
> open PropEq.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_)
>
> data ℕ⁰ : Set where
>    zero : ℕ⁰
>    2k : ℕ⁰ → ℕ⁰
>    2k+1 : ℕ⁰ → ℕ⁰
>
> suc⁰ : ℕ⁰ → ℕ⁰
> suc⁰ zero = 2k+1 zero
> suc⁰ (2k n) = 2k+1 n
> suc⁰ (2k+1 n) = 2k (suc⁰ n)
>
> conv⁰→ : ℕ⁰ → ℕ
> conv⁰→ zero = zero
> conv⁰→ (2k n) = conv⁰→ n + conv⁰→ n
> conv⁰→ (2k+1 n) = suc (conv⁰→ n + conv⁰→ n)
>
> conv⁰← : ℕ → ℕ⁰
> conv⁰← zero = zero
> conv⁰← (suc n) = suc⁰ (conv⁰← n)
>
> suc-conv : (n : ℕ⁰) → conv⁰→ (suc⁰ n) ≡ suc (conv⁰→ n)
> suc-conv zero = refl
> suc-conv (2k n) = refl
> suc-conv (2k+1 n) = begin
>                      conv⁰→ (suc⁰ (2k+1 n)) ≡[ refl ]
>                      conv⁰→ (2k (suc⁰ n)) ≡[ refl ]
>                      conv⁰→ (suc⁰ n) + conv⁰→ (suc⁰ n) ≡[ cong₂ _+_ (suc-conv
> n) (suc-conv n) ]
>                      suc (conv⁰→ n) + suc (conv⁰→ n) ≡[ cong suc (+-suc
> (conv⁰→ n) (conv⁰→ n)) ]
>                      suc (suc (conv⁰→ n + conv⁰→ n)) ≡[ refl ]
>                      suc (conv⁰→ (2k+1 n))
>                      ∎
>
> proof⁰ : ∀ n → conv⁰→ (conv⁰← n) ≡ n
> proof⁰ zero = refl
> proof⁰ (suc n) = begin
>                   conv⁰→ (conv⁰← (suc n)) ≡[ refl ]
>                   conv⁰→ (suc⁰ (conv⁰← n)) ≡[ suc-conv (conv⁰← n) ]
>                   suc (conv⁰→ (conv⁰← n)) ≡[ cong suc (proof⁰ n) ]
>                   suc n
>                   ∎
>
> proof¹ : ∀ n → conv⁰← (conv⁰→ n) ≡ n
> proof¹ zero = refl
> proof¹ (2k n) = {! !}
> proof¹ (2k+1 n) = begin
>    conv⁰← (conv⁰→ (2k+1 n)) ≡[ refl ]
>    conv⁰← (conv⁰→ (suc⁰ (2k n))) ≡[ refl ]
>    conv⁰← (suc (conv⁰→ (2k n))) ≡[ refl ]
>    suc⁰ (conv⁰← (conv⁰→ (2k n))) ≡[ cong suc⁰ (proof¹ (2k n)) ]
>    suc⁰ (2k n) ≡[ refl ]
>    2k+1 n
>    ∎


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/