如何在 Idris2 中生成可判定不等式证明？

Question

我知道

Decidable.Equality

有

decDeq

用于生成关于平等的证明。例如，从这个SO问题中，可以使用

decEq

来确定List的长度是否等于目标Vect的长度，然后如果长度相等则将List转换为Vect（代码复制如下).

我正在尝试扩展它并生成不平等证明。给定一个列表，我想获取第一个

n

元素，前提是它的元素数量 大于或等于

n

。

decEq 的原始代码是：

import Decidable.Equality
total
fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListOfLength n xs with (decEq (length xs) n)
  fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
  fromListOfLength n xs | (No _) = Nothing

我尝试（失败）使其适应不平等，如下所示：

import Decidable.Decidable
total
fromListLenGE : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListLenGE n xs with (decide LTE (length xs) n)
  fromListLenGE n xs | (Yes prf) = ?xxx
  fromListLenGE n xs | (No _) = Nothing

我不知道如何使用

decide

方法来生成不等式证明。这是出于学习目的。

有人可以帮忙解释一下如何在这里生成 LTE 证明，以便获取第一个

n

元素吗？

Answer 1

这是我通过查看 Idris2 基础库中的代码得出的结论。我确信该助手可以显着缩短或删除，但它应该让您了解

decide

如何与

LTE

一起使用。

import Data.Fun
import Data.Nat.Order
import Data.Rel
import Decidable.Decidable

%default total

ltePlusMinus : {x, y : Nat} -> LTE x y -> y = plus x (minus y x)
ltePlusMinus {x=0} LTEZero = rewrite minusZeroRight y in Refl
ltePlusMinus (LTESucc z) = cong S (ltePlusMinus z)

decomposeLTE : (n, o : Nat) -> LTE n o -> (m : Nat ** o = n + m)
decomposeLTE 0 o LTEZero = (o ** Refl)
decomposeLTE (S k) (S j) (LTESucc x) = (minus j k ** cong S (ltePlusMinus x))

decomposeVect : {n, o : Nat} -> LTE n o -> Vect o a -> (m : Nat ** Vect (n + m) a)
decomposeVect LTEZero xs = (o ** xs)
decomposeVect {n=S k} {o=S j} prf@(LTESucc prf') xs with (decomposeLTE (S k) (S j) prf) proof prf'
  decomposeVect {n=S k} {o=S j} prf@(LTESucc prf') xs | ((fst ** snd)) = (fst ** rewrite sym snd in xs)

takeLTE : (n : Nat) -> {m : Nat} -> (prf : LTE n m) -> Vect m a -> Vect n a
takeLTE n prf xs with (decomposeVect prf xs)
  takeLTE n x xs | ((_ ** snd)) = take n snd

fromListLenGE : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListLenGE n xs with (decide {ts = [Nat,Nat]} {p = LTE} n (length xs))
  fromListLenGE n xs | (Yes prf) with (fromList xs)
    fromListLenGE n xs | (Yes prf) | m = Just $ takeLTE n prf m
  fromListLenGE n xs | (No _) = Nothing