如何证明分裂是可取消的？

Question

我想使用标准库中定义的除法函数来证明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

Answer 1

请注意，在内置文件div-helper中阐明了不变式Agda.Builtin.Nat方面。您应该通过Agda.Builtin.Nat声明更通用的引理。