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

Question

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

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

你的递归调用是:

• ∃-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) 重写:

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

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