假设我已2 ^ e ≢ 0针对所有对象进行了显示e：
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
在这里，类型检查器抱怨2 ^ e除数，错误消息为_≢0_6 : Relation.Nullary.Decidable.Core.False ((2 ^ e) ≟ 0)：
有没有办法使决策程序≟使用我的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。
但是我在想，是否可以教类型检查器新的技巧而不是使用替代方法。
除被除数和除数外，还_/_采用一个隐式参数，这是除数不等于0的证明。
如文件中divmod.agda所述，此参数隐式的原因是，当除数的形式suc n为时可以推断出该参数。例如，以下定义类型检查正确，因为2定义上等于suc 1：
four : ℕ
four = 8 / 2
但是，对于给定n，m / n不会直接进行敲击，因为在一般情况下无法推断出证明。如果不能，则需要直接将其作为附加隐式参数的实例传递。
就您而言，除数在命题上不等于0，但在定义上不等于0，这意味着您必须执行以下过程：
postulate lemma : ∀ {m e} → (m / 2 ^ e) {fromWitnessFalse (2^e≢0 {e})} ≤ m
为了能够使用，fromWitnessFalse您需要在文件中添加以下导入：
open import Relation.Nullary.Decidable.Core
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句