Termination checking failed to prove ∃-even′ : ∀ {n : ℕ} → ∃[ m ] ( 2 * m ≡ n) → even n

Question

The PLFA exercise: what if we write the arithmetic more "naturally" in Quantifiers chapter (https://plfa.github.io/Quantifiers/) ?

∃-even′ : ∀ {n : ℕ} → ∃[ m ] (    2 * m ≡ n) → even n
∃-odd′  : ∀ {n : ℕ} → ∃[ m ] (2 * m + 1 ≡ n) →  odd n

I have make the type right. But have got Termination checking failed for the following functions:

dbl≡2* : ∀ n → n + n ≡ 2 * n
dbl≡2* n = cong (n +_) (sym (+-identityʳ n))

+-suc1 : ∀ (m : ℕ) → m + 1 ≡ suc m
+-suc1 m =
  begin
    m + 1
    ≡⟨⟩
    m + (suc zero)
    ≡⟨ +-suc m zero ⟩
    suc (m + zero)
    ≡⟨ cong suc (+-identityʳ m) ⟩
    suc m
    ∎ 

help1 : ∀ m → 2 * m + 1 ≡ suc (m + m)
help1 m =
  begin
    2 * m + 1
    ≡⟨  sym ( cong (_+ 1) (dbl≡2* m) ) ⟩
    m + m + 1  -- must use every rule
    ≡⟨ +-assoc m m 1 ⟩
    m + (m + 1)
    ≡⟨ cong (m +_) (+-suc1 m) ⟩
    m + suc m
    ≡⟨ +-suc m m ⟩
    suc (m + m)
    ∎

∃-even′ ⟨ zero , refl ⟩ = even-zero
∃-even′ ⟨ suc m , refl ⟩ rewrite +-identityʳ m
                | +-suc m m
                = even-suc (∃-odd′ ⟨ (m) ,  help1 m ⟩)

∃-odd′ ⟨ m , refl ⟩ rewrite +-suc (2 * m) 0
                | +-identityʳ m
                | +-identityʳ (m + m)
                | dbl≡2* m
                = odd-suc (∃-even′ ⟨ m , refl ⟩)

For the normal version, the same mutually-recursive define can work fine.

∃-even : ∀ {n : ℕ} → ∃[ m ] (    m * 2 ≡ n) → even n
∃-odd  : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) →  odd n

∃-even ⟨ zero , refl ⟩ = even-zero
∃-even ⟨ suc x , refl ⟩ = even-suc (∃-odd ⟨ x , refl ⟩)
∃-odd ⟨ x , refl ⟩ = odd-suc (∃-even ⟨ x , refl ⟩)

Answer 1

∃-even′ ⟨ zero , refl ⟩ = even-zero
∃-even′ ⟨ suc m , refl ⟩ rewrite +-identityʳ m
                | +-suc m m
                = even-suc (∃-odd′ ⟨ m ,  help1 m ⟩)

∃-odd′ ⟨ m , refl ⟩ rewrite +-suc (2 * m) 0
                | +-identityʳ m
                | +-identityʳ (m + m)
                | dbl≡2* m
                = odd-suc (∃-even′ ⟨ m , refl ⟩)

Your recursive calls are:

• ∃-even′ ⟨ suc m , refl ⟩ -> ∃-odd′ ⟨ m , help1 m ⟩
• ∃-odd′ ⟨ m , refl ⟩ -> ∃-even′ ⟨ m , refl ⟩

In the first one, suc m -> m decreases, but refl -> help1 m (on its surface) increases. If you passed refl as the second argument to ∃-odd′, then the termination checker would accept it, since it means the second argument stays the same, while the first one strictly monotonically decreases over a complete chain of two calls.

So how can we change that first recursive call to ∃-odd′ ⟨ m , refl ⟩? By rewriting by sym (help1 m):

∃-even′ ( suc m , refl ) rewrite +-identityʳ m
                | +-suc m m
                | sym (help1 m)
                = even-suc (∃-odd′ (m ,  refl))

This code is then accepted by the termination checker.