终止检查未能证明 ∃-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 ⟩)

解决方法

bday is in less than a week 2

您的递归调用是：

• ∃-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′ ⟨ suc m,refl ⟩
• ∃-odd′ ⟨ m,help1 m ⟩ -> ∃-odd′ ⟨ m,refl ⟩

在第一个中，∃-even′ ⟨ m,refl ⟩ -> suc m 减少，但 m -> refl（在其表面上）增加。如果您将 help1 m 作为第二个参数传递给 refl，则终止检查器将接受它，因为这意味着第二个参数保持不变，而第一个参数在两个完整的链上严格单调递减电话。

那么我们如何将第一个递归调用更改为 ∃-odd′？由∃-odd′ ⟨ m,refl ⟩重写：

sym (help1 m)

此代码随后被终止检查器接受。