教类型检查器2^e≢0

Question

假设我已经为所有e显示了2 ^ e ≢ 0

module Question where

open import Data.Nat
open import Data.Nat.DivMod
open import Relation.Binary.PropositionalEquality

postulate 2^e≢0 : (e : ℕ) → 2 ^ e ≢ 0

我现在希望类型检查器在下面这样的情况下使用这些知识：

postulate lemma : (m e : ℕ) → m / 2 ^ e ≤ m

在这里，类型检查器使用_≢0_6 : Relation.Nullary.Decidable.Core.False ((2 ^ e) ≟ 0)错误消息来抱怨2 ^ e除数

有没有办法让决策过程≟使用我的2^e≢0引理？

我可以想出下面的变通方法，这看起来有点笨拙。我的想法是使用一个明显非零因子的suc x，并证明它等于2 ^ e

postulate lemma′ : (m e x : ℕ) → suc x ≡ 2 ^ e → m / suc x ≤ m

类似地，我可以使用Agda内置的div-helper而不是/，并将x而不是suc x传递给它。

但我想知道，我是否可以教类型检查器新的技巧，而不是使用变通方法。

Answer 1

除了被除数和除数之外，_/_还使用一个隐式参数来证明除数不等于0。

正如文件divmod.agda中所解释的，此参数为隐式参数的原因是，当除数的形式为suc n时，可以推断出该参数。例如，以下定义类型检查正确，因为2在定义上等于suc 1

four : ℕ
four = 8 / 2

然而，对于给定的n，m / n不会直接进行类型检查，因为在一般情况下无法推断证明。如果不能，则需要将其作为附加隐式参数的实例化直接传递。

在你的例子中，你的除数命题上不等于0，但不是确定的，这意味着你必须经历这个过程，如下所示：

postulate lemma : ∀ {m e} → (m / 2 ^ e) {fromWitnessFalse (2^e≢0 {e})} ≤ m

为了能够使用fromWitnessFalse，您需要将以下导入添加到文件中：

open import Relation.Nullary.Decidable.Core