时间戳

首页 > 解决方案 > 在 Idris 中为决策函数构建证明

proof - 在 Idris 中为决策函数构建证明

问题描述

我正在尝试为表示模块化空间中两个连续元素的类型创建一个决策函数。

（此代码源自对我的上一个问题的出色回答。）

data PreceedsN : Nat -> Nat -> Nat -> Type where
    PreceedsS : {auto prf : S a `LT` m} -> PreceedsN m a (S a)
    PreceedsZ : {auto prf : S a = m} -> PreceedsN m a Z

doesPreceedN : (m : Nat) -> (a : Nat) -> (b : Nat) -> Dec (PreceedsN m a b)
doesPreceedN m a b with (S a `cmp` m)
    doesPreceedN (S a + S d) a b     | CmpLT d with (S a `decEq` b)
        doesPreceedN (S a + S d) a b | CmpLT d | Yes prf = Yes ?bIsSa
        doesPreceedN (S a + S d) a b | CmpLT d | No contra = No ?bNotSa
    doesPreceedN (S m) m b     | CmpEQ   with (b `decEq` 0)
        doesPreceedN (S m) m Z | CmpEQ | Yes prf = Yes PreceedsZ
        doesPreceedN (S m) m b | CmpEQ | No contra = No ?saIsmAndbIsNotZ
    doesPreceedN (S m) (m + (S d)) b | CmpGT d = No ?saCannotBeGTm

我已经尽力了，但我的知识还不够丰富，无法自己构建必要的证明，尤其是矛盾的证明。你能告诉我如何填补上面代码中的一个或多个漏洞吗？

另外，如果您使用任何方便的工具，例如absurd、impossible或战术，您能解释一下它们是如何工作的以及它们在证明中所起的作用吗？

标签： proofidristheorem-proving

解决方案

推荐阅读