[Agda] Komencenta demando.

[Andrés Sicard-Ramírez]

On 29 November 2015 at 07:56, Serge Leblanc <33dbqnxpy7if at gmail.com> wrote:
> Kial la serĉo de la finaĵo fiaskas en sekva ekzemplo?
> Why the termination checking fail in following example?
>
> module Recursive where
>
> 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
>   ∎
>
>
> Sinceran dankan pro via venonta helpo.

For the same reason that the termination checker fails in the following example:

  data Foo : Set where
    a : Foo → Foo
    b : Foo → Foo

  bar : Foo → Foo
  bar (a f) = a f
  bar (b f) = bar (a f)

That is, in the recursive call to `bar`, the argument `a f` is not
structurally smaller than the argument `b f`.


-- 
Andrés