Agda证明整除加法封闭性时约束求解失败求助

在使用Agda证明自然数整除的加法封闭性（∣-plus）时，遇到了约束求解失败的问题，以下是相关代码、错误信息及尝试过的解决思路：

初始代码 #

module div where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.Nat.Properties using (+-assoc)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; cong; sym; trans)

data _∣_ : ℕ → ℕ → Set where
    0∣0 : zero ∣ zero
    m∣0 : ∀ {d} → suc d ∣ zero
    m∣n : ∀ {d m} → suc d ∣ m → suc d ∣ suc (m + d)

infix 4 _∣_

∣-refl : ∀ a → a ∣ a
∣-refl zero = 0∣0
∣-refl (suc a) = m∣n m∣0

+zero : ∀ m → m + zero ≡ m
+zero zero = refl
+zero (suc m) rewrite +zero m = refl

+n : ∀ {m n : ℕ} → m + suc n ≡ suc (m + n)
+n {zero} {n} = refl
+n {suc m} {n} = cong suc (+n)

d-suc : ∀ {m n : ℕ} → suc (m + suc n) ≡ suc (suc (m + n))
d-suc = cong suc (+n)


∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus _ (suc w) .zero (m∣n r₁) m∣0 rewrite +zero w = m∣n r₁
∣-plus (suc d) .(suc (_ + _)) .(suc (_ + _)) (m∣n r₁) (m∣n r₂) = {!   !} 

错误信息 #

运行Agda后，最后一行出现如下约束求解失败错误：

Failed to solve the following constraints:
  _63 + _64 = m + d : ℕ (blocked on _63)
  _61 + _62 = m₁ + d : ℕ (blocked on _61)

尝试的修改与问题 #

修改模式匹配 #

我尝试将最后一行的模式匹配改为：

∣-plus (suc d) (suc (m₁ + d)) (suc (m₂ + d)) (m∣n r₁) (m∣n r₂) = ?

此时目标应为?0 : suc d ∣ suc (m₁ + d + suc (m₂ + d))，理论上可通过d-suc转换目标，但因约束错误无法获取m₁和m₂，无法证明等式suc (suc(m₁ + d + (m₂ + d))) ≡ suc (suc(m₁ + m₂ + d + d))。

简化证明逻辑 #

后续我简化了证明结构：

∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus .(suc _) .(suc _) c (m∣n r₁) r₂ = ?

目标变为0? : suc d ∣ suc (m + d + c)，虽可通过m∣n (∣-plus _ _ _ r₁ r₂)得到suc d ∣ suc (m + c + d)，但缺少d和m的绑定，无法应用加法交换等式m + d + c = m + c + d。

添加交换引理 #

之后我添加了自定义的加法交换引理++ex：

open import Data.Nat.Properties using (+-assoc; +-comm; +-identityʳ)

++ex : ∀ {a b c : ℕ} → a + b + c ≡ a + c + b
++ex {zero} {b} {c} rewrite +-comm b c = refl
++ex {suc a} {b} {c} = cong suc (++ex {a} {b} {c})

∣-plus : ∀ a b c → a ∣ b → a ∣ c → a ∣ b + c
∣-plus .zero .zero c 0∣0 r₂ = r₂
∣-plus .(suc _) .zero c m∣0 r₂ = r₂
∣-plus (suc d) .(suc _) c (m∣n r₁) r₂ with m∣n (∣-plus _ _ _ r₁ r₂)
... | s rewrite ++ex {_} {c} {d} = {!  !}

但依旧无法获取m来应用该引理，请问该如何解决这个问题？

内容的提问来源于stack exchange，提问作者maplgebra