终止检查未能证明 ∃-even′ : ∀ {n : ℕ} → ∃[ m ] ( 2 * m ≡ n) → even n

问题描述

PLFA 练习：如果我们在量词章节 (https://plfa.github.io/Quantifiers/) 中更“自然地”编写算术会怎样？

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

我已经把类型弄对了。但是有以下功能的终止检查失败：

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 ⟩)

对于普通版本，相同的相互递归定义可以正常工作。

∃-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 ⟩)

解决方法

暂无找到可以解决该程序问题的有效方法，小编努力寻找整理中！

如果你已经找到好的解决方法，欢迎将解决方案带上本链接一起发送给小编。

小编邮箱:dio#foxmail.com (将#修改为@）

agda termination