如何证明除法是可取消的？
How to prove that division is cancellative?
我想用标准库中定义的除法函数在agda中证明(c * a) / (c * b) = a / b。证据不断回到这个很难处理和推理的东西 div-helper。
open import Data.Nat.DivMod using (_/_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; zero)
/-cancelˡ : ∀ c a b {b≢0} {b*c≢0} → ((c * a) / (c * b)) {b*c≢0} ≡ (a / b) {b≢0}
/-cancelˡ (suc c) a (suc b) {b≢0} {b*c≢0} = ?
那个洞简化为：
div-helper 0 (b + c * suc b) (a + c * a) (b + c * suc b) ≡ div-helper 0 b a b
请注意，不变量 div-helper 方面在内置文件 Agda.Builtin.Nat 中有详细说明。你应该陈述一个更通用的引理版本，满足 div-helper.
我可以想出两个不同的证明。
证明 1 完全不知道 div-helper 的结构。它基于标准库中关于除法的引理。它证明了一些关于除法的附加引理，然后用它来证明我们所追求的 属性。这有点复杂，但我认为额外的引理本身很有用。
证明 2 考虑了 div-helper 的结构并证明了 属性 的两个不变量。简洁多了。
这就是我们想要的 属性：
∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
让这看起来有点奇怪的是除法助手用 n（而不是 suc n）代替 a / suc n。这就是 b + n + b * n 的来源 - suc (b + n + b * n) 等于 suc b * suc n.
用 / 而不是除法助手来表示，因此证明表明 (a * suc n) / (suc b * suc n) 等于 a / suc b。
这是证明 1:
module Answer where
open import Relation.Binary.PropositionalEquality as P using (_≡_; cong; refl; subst; sym)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Core
open import Data.Nat.Properties
open import Agda.Builtin.Nat using () renaming (div-helper to divₕ; mod-helper to modₕ)
divₕ′ : ℕ → ℕ → ℕ
divₕ′ a m = divₕ 0 m a m
modₕ′ : ℕ → ℕ → ℕ
modₕ′ a m = modₕ 0 m a m
a<n⇒a[divₕ]n≡0 : ∀ (a n n′ : ℕ) → a ≤ n → divₕ 0 n′ a n ≡ 0
a<n⇒a[divₕ]n≡0 zero _ _ _ = refl
a<n⇒a[divₕ]n≡0 (suc a) (suc n) n′ (s≤s a≤n) = a<n⇒a[divₕ]n≡0 a n n′ a≤n
a*n[modₕ]n≡0 : ∀ (a n : ℕ) → modₕ 0 n (a * suc n) n ≡ 0
a*n[modₕ]n≡0 zero n = refl
a*n[modₕ]n≡0 (suc a) n rewrite +-comm (suc n) (a * suc n) | a+n[modₕ]n≡a[modₕ]n 0 (a * suc n) n = a*n[modₕ]n≡0 a n
a<n⇒a+b*n[divₕ]n≡b : ∀ (a b n : ℕ) → a ≤ n → divₕ 0 n (a + b * suc n) n ≡ b
a<n⇒a+b*n[divₕ]n≡b a b n a≤n =
begin
divₕ′ (a + b * suc n) n
≡⟨ +-distrib-divₕ 0 0 a (b * suc n) n lem₁ ⟩
divₕ′ a n + divₕ′ (b * suc n) n
≡⟨ cong (_+ divₕ′ (b * suc n) n) (a<n⇒a[divₕ]n≡0 a n n a≤n) ⟩
0 + divₕ′ (b * suc n) n
≡⟨ +-identityˡ (divₕ 0 n (b * suc n) n) ⟩
divₕ′ (b * suc n) n
≡⟨ m*n/n≡m b (suc n) ⟩
b
∎
where
open P.≡-Reasoning
≤₁ = a[modₕ]n<n 0 a n
≤₂ = ≤-reflexive (a*n[modₕ]n≡0 b n)
<₃ : n + 0 < suc n
<₃ = s≤s (≤-reflexive (+-identityʳ n))
lem₁ : modₕ′ a n + modₕ′ (b * suc n) n < suc n
lem₁ = <-transʳ (+-mono-≤ ≤₁ ≤₂) <₃
a[divₕ]m*n≡a[divₕ]m[divₕ]n : ∀ (a m n : ℕ) → divₕ 0 (m + n + m * n) a (m + n + m * n) ≡ divₕ 0 n (divₕ 0 m a m) n
a[divₕ]m*n≡a[divₕ]m[divₕ]n a m n =
begin
divₕ′ a mn
≡⟨ cong (λ # → divₕ′ # mn) (div-mod-lemma 0 0 a m) ⟩
divₕ′ (modₕ′ a m + divₕ′ a m * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + # * suc m) mn) (div-mod-lemma 0 0 (divₕ′ a m) n) ⟩
divₕ′ (modₕ′ a m + (modₕ′ (divₕ′ a m) n + divₕ′ (divₕ′ a m) n * suc n) * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + #) mn) (*-distribʳ-+ (suc m) (modₕ′ (divₕ′ a m) n) (divₕ′ (divₕ′ a m) n * suc n)) ⟩
divₕ′ (modₕ′ a m + (modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc n * suc m)) mn
≡⟨ cong (λ # → divₕ′ # mn) (sym (+-assoc (modₕ′ a m) (modₕ′ (divₕ′ a m) n * suc m) (divₕ′ (divₕ′ a m) n * suc n * suc m))) ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc n * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + #) mn) (*-assoc (divₕ′ (divₕ′ a m) n) (suc n) (suc m))⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * (suc n * suc m)) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * #) mn) (*-comm (suc n) (suc m)) ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * (suc m * suc n)) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * #) mn) lem₁ ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc mn) mn
≡⟨ a<n⇒a+b*n[divₕ]n≡b (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m) (divₕ′ (divₕ′ a m) n) mn lem₄ ⟩
divₕ 0 n (divₕ′ a m) n
∎
where
open P.≡-Reasoning
mn = m + n + m * n
lem₁ : suc m * suc n ≡ suc mn
lem₁ rewrite +-comm m n | *-comm m (suc n) | *-comm m n | +-assoc n m (n * m) = refl
lem₂ : m + n * suc m ≡ mn
lem₂ rewrite *-comm n (suc m) | +-assoc m n (m * n) = refl
≤₁ = a[modₕ]n<n 0 a m
≤₂ = a[modₕ]n<n 0 (divₕ 0 m a m) n
≤₃ = ≤-refl {suc m}
lem₃ = +-mono-≤ ≤₁ (*-mono-≤ ≤₂ ≤₃)
lem₄ : modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m ≤ mn
lem₄ = subst (λ # → modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m ≤ #) lem₂ lem₃
a*n[divₕ]b*n≡a[divₕ]b : ∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
a*n[divₕ]b*n≡a[divₕ]b a b n =
begin
divₕ′ na nb
≡⟨ cong (λ # → divₕ′ na #) nb≡bn ⟩
divₕ′ na bn
≡⟨ a[divₕ]m*n≡a[divₕ]m[divₕ]n na n b ⟩
divₕ′ (divₕ′ na n) b
≡⟨ cong (λ # → divₕ′ (divₕ′ # n) b) lem₁ ⟩
divₕ′ (divₕ′ (a * suc n) n) b
≡⟨ cong (λ # → divₕ′ # b) (a*n[divₕ]n≡a 0 a n) ⟩
divₕ 0 b a b
∎
where
open P.≡-Reasoning
na = a + n * a
nb = b + n + b * n
bn = n + b + n * b
nb≡bn : nb ≡ bn
nb≡bn rewrite +-comm n b | *-comm n b = refl
lem₁ : na ≡ a * suc n
lem₁ rewrite *-comm a (suc n) = refl
现在让我们看看证明2。只需将其附加到上面的代码中，这样我就不必重复imports:
a*n[divₕ]b*n≡a[divₕ]b′ : ∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
a*n[divₕ]b*n≡a[divₕ]b′ a b n rewrite +-comm b n | *-comm b n = lem₂ n 0 b a b
where
lem₁ : ∀ (a k m n j : ℕ) → divₕ k m (a + n) (a + j) ≡ divₕ k m n j
lem₁ zero k m n j = refl
lem₁ (suc a) k m n j = lem₁ a k m n j
lem₂ : ∀ (a k m n j : ℕ) → divₕ k (a + m + a * m) (suc a * n) (a + j + a * j) ≡ divₕ k m n j
lem₂ a k m zero j rewrite *-zeroʳ a = refl
lem₂ a k m (suc n) zero
rewrite *-zeroʳ a
| +-identityʳ a
| *-suc a n
| P.sym (+-assoc n a (a * n))
| +-comm n a
| +-assoc a n (a * n)
| P.sym (+-suc a (n + a * n))
| lem₁ a k (a + m + a * m) (suc (n + a * n)) 0
= lem₂ a (suc k) m n m
lem₂ a k m (suc n) (suc j)
rewrite *-suc a n
| P.sym (+-assoc n a (a * n))
| +-comm n a
| +-assoc a n (a * n)
| P.sym (+-suc a (n + a * n))
| +-assoc a (suc j) (a * suc j)
| lem₁ a k (a + m + a * m) (suc (n + a * n)) (suc j + a * suc j)
| *-suc a j
| P.sym (+-assoc j a (a * j))
| +-comm j a
= lem₂ a k m n j
第一个引理是一个不变量，表示我们可以将相同的值 a 添加到 div-helper、n 和 j 的最后两个参数。它被第二个引理使用，这是更有趣的引理。
第二个引理是一个不变量，表示您可以将最后三个参数 m、n 和 j 与相同的值 a 相乘.它是对最后两个参数 n 和 j 的归纳证明。这使得它紧密遵循 div-helper.
的结构
因此，证明涵盖了 div-helper 的三个定义方程中出现的相同三种不同情况：
n 为零n 为非零，但 j 为零n 和 j 都非零
我们之后的 属性 直接来自第二个引理。这基本上是其他响应中概述的想法，其中第二个引理是我们所追求的 属性 的更一般版本。
我想用标准库中定义的除法函数在agda中证明(c * a) / (c * b) = a / b。证据不断回到这个很难处理和推理的东西 div-helper。
open import Data.Nat.DivMod using (_/_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Nat using (ℕ; suc; zero)
/-cancelˡ : ∀ c a b {b≢0} {b*c≢0} → ((c * a) / (c * b)) {b*c≢0} ≡ (a / b) {b≢0}
/-cancelˡ (suc c) a (suc b) {b≢0} {b*c≢0} = ?
那个洞简化为：
div-helper 0 (b + c * suc b) (a + c * a) (b + c * suc b) ≡ div-helper 0 b a b
请注意，不变量 div-helper 方面在内置文件 Agda.Builtin.Nat 中有详细说明。你应该陈述一个更通用的引理版本，满足 div-helper.
我可以想出两个不同的证明。
证明 1 完全不知道
div-helper的结构。它基于标准库中关于除法的引理。它证明了一些关于除法的附加引理，然后用它来证明我们所追求的 属性。这有点复杂，但我认为额外的引理本身很有用。证明 2 考虑了
div-helper的结构并证明了 属性 的两个不变量。简洁多了。
这就是我们想要的 属性：
∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
让这看起来有点奇怪的是除法助手用 n（而不是 suc n）代替 a / suc n。这就是 b + n + b * n 的来源 - suc (b + n + b * n) 等于 suc b * suc n.
用 / 而不是除法助手来表示，因此证明表明 (a * suc n) / (suc b * suc n) 等于 a / suc b。
这是证明 1:
module Answer where
open import Relation.Binary.PropositionalEquality as P using (_≡_; cong; refl; subst; sym)
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Nat.DivMod.Core
open import Data.Nat.Properties
open import Agda.Builtin.Nat using () renaming (div-helper to divₕ; mod-helper to modₕ)
divₕ′ : ℕ → ℕ → ℕ
divₕ′ a m = divₕ 0 m a m
modₕ′ : ℕ → ℕ → ℕ
modₕ′ a m = modₕ 0 m a m
a<n⇒a[divₕ]n≡0 : ∀ (a n n′ : ℕ) → a ≤ n → divₕ 0 n′ a n ≡ 0
a<n⇒a[divₕ]n≡0 zero _ _ _ = refl
a<n⇒a[divₕ]n≡0 (suc a) (suc n) n′ (s≤s a≤n) = a<n⇒a[divₕ]n≡0 a n n′ a≤n
a*n[modₕ]n≡0 : ∀ (a n : ℕ) → modₕ 0 n (a * suc n) n ≡ 0
a*n[modₕ]n≡0 zero n = refl
a*n[modₕ]n≡0 (suc a) n rewrite +-comm (suc n) (a * suc n) | a+n[modₕ]n≡a[modₕ]n 0 (a * suc n) n = a*n[modₕ]n≡0 a n
a<n⇒a+b*n[divₕ]n≡b : ∀ (a b n : ℕ) → a ≤ n → divₕ 0 n (a + b * suc n) n ≡ b
a<n⇒a+b*n[divₕ]n≡b a b n a≤n =
begin
divₕ′ (a + b * suc n) n
≡⟨ +-distrib-divₕ 0 0 a (b * suc n) n lem₁ ⟩
divₕ′ a n + divₕ′ (b * suc n) n
≡⟨ cong (_+ divₕ′ (b * suc n) n) (a<n⇒a[divₕ]n≡0 a n n a≤n) ⟩
0 + divₕ′ (b * suc n) n
≡⟨ +-identityˡ (divₕ 0 n (b * suc n) n) ⟩
divₕ′ (b * suc n) n
≡⟨ m*n/n≡m b (suc n) ⟩
b
∎
where
open P.≡-Reasoning
≤₁ = a[modₕ]n<n 0 a n
≤₂ = ≤-reflexive (a*n[modₕ]n≡0 b n)
<₃ : n + 0 < suc n
<₃ = s≤s (≤-reflexive (+-identityʳ n))
lem₁ : modₕ′ a n + modₕ′ (b * suc n) n < suc n
lem₁ = <-transʳ (+-mono-≤ ≤₁ ≤₂) <₃
a[divₕ]m*n≡a[divₕ]m[divₕ]n : ∀ (a m n : ℕ) → divₕ 0 (m + n + m * n) a (m + n + m * n) ≡ divₕ 0 n (divₕ 0 m a m) n
a[divₕ]m*n≡a[divₕ]m[divₕ]n a m n =
begin
divₕ′ a mn
≡⟨ cong (λ # → divₕ′ # mn) (div-mod-lemma 0 0 a m) ⟩
divₕ′ (modₕ′ a m + divₕ′ a m * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + # * suc m) mn) (div-mod-lemma 0 0 (divₕ′ a m) n) ⟩
divₕ′ (modₕ′ a m + (modₕ′ (divₕ′ a m) n + divₕ′ (divₕ′ a m) n * suc n) * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + #) mn) (*-distribʳ-+ (suc m) (modₕ′ (divₕ′ a m) n) (divₕ′ (divₕ′ a m) n * suc n)) ⟩
divₕ′ (modₕ′ a m + (modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc n * suc m)) mn
≡⟨ cong (λ # → divₕ′ # mn) (sym (+-assoc (modₕ′ a m) (modₕ′ (divₕ′ a m) n * suc m) (divₕ′ (divₕ′ a m) n * suc n * suc m))) ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc n * suc m) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + #) mn) (*-assoc (divₕ′ (divₕ′ a m) n) (suc n) (suc m))⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * (suc n * suc m)) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * #) mn) (*-comm (suc n) (suc m)) ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * (suc m * suc n)) mn
≡⟨ cong (λ # → divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * #) mn) lem₁ ⟩
divₕ′ (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m + divₕ′ (divₕ′ a m) n * suc mn) mn
≡⟨ a<n⇒a+b*n[divₕ]n≡b (modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m) (divₕ′ (divₕ′ a m) n) mn lem₄ ⟩
divₕ 0 n (divₕ′ a m) n
∎
where
open P.≡-Reasoning
mn = m + n + m * n
lem₁ : suc m * suc n ≡ suc mn
lem₁ rewrite +-comm m n | *-comm m (suc n) | *-comm m n | +-assoc n m (n * m) = refl
lem₂ : m + n * suc m ≡ mn
lem₂ rewrite *-comm n (suc m) | +-assoc m n (m * n) = refl
≤₁ = a[modₕ]n<n 0 a m
≤₂ = a[modₕ]n<n 0 (divₕ 0 m a m) n
≤₃ = ≤-refl {suc m}
lem₃ = +-mono-≤ ≤₁ (*-mono-≤ ≤₂ ≤₃)
lem₄ : modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m ≤ mn
lem₄ = subst (λ # → modₕ′ a m + modₕ′ (divₕ′ a m) n * suc m ≤ #) lem₂ lem₃
a*n[divₕ]b*n≡a[divₕ]b : ∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
a*n[divₕ]b*n≡a[divₕ]b a b n =
begin
divₕ′ na nb
≡⟨ cong (λ # → divₕ′ na #) nb≡bn ⟩
divₕ′ na bn
≡⟨ a[divₕ]m*n≡a[divₕ]m[divₕ]n na n b ⟩
divₕ′ (divₕ′ na n) b
≡⟨ cong (λ # → divₕ′ (divₕ′ # n) b) lem₁ ⟩
divₕ′ (divₕ′ (a * suc n) n) b
≡⟨ cong (λ # → divₕ′ # b) (a*n[divₕ]n≡a 0 a n) ⟩
divₕ 0 b a b
∎
where
open P.≡-Reasoning
na = a + n * a
nb = b + n + b * n
bn = n + b + n * b
nb≡bn : nb ≡ bn
nb≡bn rewrite +-comm n b | *-comm n b = refl
lem₁ : na ≡ a * suc n
lem₁ rewrite *-comm a (suc n) = refl
现在让我们看看证明2。只需将其附加到上面的代码中，这样我就不必重复imports:
a*n[divₕ]b*n≡a[divₕ]b′ : ∀ (a b n : ℕ) → divₕ 0 (b + n + b * n) (a + n * a) (b + n + b * n) ≡ divₕ 0 b a b
a*n[divₕ]b*n≡a[divₕ]b′ a b n rewrite +-comm b n | *-comm b n = lem₂ n 0 b a b
where
lem₁ : ∀ (a k m n j : ℕ) → divₕ k m (a + n) (a + j) ≡ divₕ k m n j
lem₁ zero k m n j = refl
lem₁ (suc a) k m n j = lem₁ a k m n j
lem₂ : ∀ (a k m n j : ℕ) → divₕ k (a + m + a * m) (suc a * n) (a + j + a * j) ≡ divₕ k m n j
lem₂ a k m zero j rewrite *-zeroʳ a = refl
lem₂ a k m (suc n) zero
rewrite *-zeroʳ a
| +-identityʳ a
| *-suc a n
| P.sym (+-assoc n a (a * n))
| +-comm n a
| +-assoc a n (a * n)
| P.sym (+-suc a (n + a * n))
| lem₁ a k (a + m + a * m) (suc (n + a * n)) 0
= lem₂ a (suc k) m n m
lem₂ a k m (suc n) (suc j)
rewrite *-suc a n
| P.sym (+-assoc n a (a * n))
| +-comm n a
| +-assoc a n (a * n)
| P.sym (+-suc a (n + a * n))
| +-assoc a (suc j) (a * suc j)
| lem₁ a k (a + m + a * m) (suc (n + a * n)) (suc j + a * suc j)
| *-suc a j
| P.sym (+-assoc j a (a * j))
| +-comm j a
= lem₂ a k m n j
第一个引理是一个不变量，表示我们可以将相同的值 a 添加到 div-helper、n 和 j 的最后两个参数。它被第二个引理使用，这是更有趣的引理。
第二个引理是一个不变量，表示您可以将最后三个参数 m、n 和 j 与相同的值 a 相乘.它是对最后两个参数 n 和 j 的归纳证明。这使得它紧密遵循 div-helper.
因此，证明涵盖了 div-helper 的三个定义方程中出现的相同三种不同情况：
n为零n为非零，但j为零n和j都非零
我们之后的 属性 直接来自第二个引理。这基本上是其他响应中概述的想法，其中第二个引理是我们所追求的 属性 的更一般版本。