idris - LTE 整数 (ZZ)

Question

我(为了好玩？)尝试在 Idris 中完成所有如何证明。我需要的属性之一是整数的全排序。 idris 已经有了data.ZZ提供基于归纳的整数的模块。我需要添加类似于 Nat 的 LTE 的类型。我似乎无法让自己相信我的实现是正确的(或者 LTE 在这方面是正确的)。如何“检查”我正在处理的 LTEZZ 数据类型是否有效？如何检查 (LTE 4 3) 是否无效？

示例代码如下:

%default total
||| Proof the a is <= b
||| a is the smaller number
||| b is the larger number
data LTEZZ : (a : ZZ) -> (b : ZZ) -> Type where
  ||| Zero is less than any positive
  LTEZero : LTEZZ (Pos Z) (Pos right)
  ||| If both are positive, and n <= m, n+1 <= m+1
  LTEPosSucc : LTEZZ (Pos left) (Pos right) -> LTEZZ (Pos (S left)) (Pos (S right))
  ||| Negative is always less than positive, including zero
  LTENegPos : LTEZZ (NegS left) (Pos right)
  ||| If both are negative and n <= m, n-1 <= m-1
  LTENegSucc: LTEZZ (NegS (S left)) (NegS (S right)) -> LTEZZ (NegS left) (NegS right)

Uninhabited (LTEZZ (Pos n) (NegS m)) where
  uninhabited LTENegPos impossible
Uninhabited (LTEZZ (Pos (S n)) (Pos Z)) where
  uninhabited LTEZero impossible

Answer 1

首先，LTE 将 Nat 转换为全序，如果您关注 this link，您就会看到这一点。 .

但是 LTEZZ 并没有达到预期目的。检查它的方法之一是证明 total order 的属性使用定义。但对于 LTEZZ 来说，您将无法例如证明自反性。

这是修复它的一种方法:

data LTEZZ : (a : ZZ) -> (b : ZZ) -> Type where
  ||| Zero is less than any positive
  LTEZero : LTEZZ (Pos Z) (Pos right)
  ||| If both are positive, and n <= m, n+1 <= m+1
  LTEPosSucc : LTEZZ (Pos left) (Pos right) -> LTEZZ (Pos (S left)) (Pos (S right))
  ||| Negative is always less than positive, including zero
  LTENegPos : LTEZZ (NegS left) (Pos right)
  ||| -1 is the greatest negative number
  LTEMinusOne : LTEZZ (NegS left) (NegS Z)
  ||| If both are negative and n <= m, then n-1 <= m-1
  LTENegSucc: LTEZZ (NegS left) (NegS right) -> LTEZZ (NegS (S left)) (NegS (S right))

我添加了 -1 的情况，并修复了 LTENegSucc 的情况(您希望在每个递归步骤结构上使参数更小，只需就像LTEPosSucc)。

导入和一些辅助引理:

import Data.ZZ
import Decidable.Order

%default total

||| A helper lemma treating the non-negative integers.
lteLtezzPos : m `LTE` n -> Pos m `LTEZZ` Pos n
lteLtezzPos LTEZero = LTEZero
lteLtezzPos (LTESucc x) = LTEPosSucc (lteLtezzPos x)

||| A helper lemma treating the negative integers.
lteLtezzNegS : m `LTE` n -> NegS n `LTEZZ` NegS m
lteLtezzNegS LTEZero = LTEMinusOne
lteLtezzNegS (LTESucc x) = LTENegSucc (lteLtezzNegS x)

自反性:

||| `LTEZZ` is reflexive.
ltezzRefl : z `LTEZZ` z
ltezzRefl {z = (Pos n)} = lteLtezzPos lteRefl
ltezzRefl {z = (NegS n)} = lteLtezzNegS lteRefl

传递性:

||| `LTEZZ` is transitive.
ltezzTransitive : a `LTEZZ` b -> b `LTEZZ` c -> a `LTEZZ` c
ltezzTransitive LTEZero LTEZero = LTEZero
ltezzTransitive LTEZero (LTEPosSucc _) = LTEZero
ltezzTransitive (LTEPosSucc x) (LTEPosSucc y) = LTEPosSucc (ltezzTransitive x y)
ltezzTransitive LTENegPos LTEZero = LTENegPos
ltezzTransitive LTENegPos (LTEPosSucc x) = LTENegPos
ltezzTransitive LTEMinusOne LTENegPos = LTENegPos
ltezzTransitive LTEMinusOne LTEMinusOne = LTEMinusOne
ltezzTransitive (LTENegSucc x) LTENegPos = LTENegPos
ltezzTransitive (LTENegSucc x) LTEMinusOne = LTEMinusOne
ltezzTransitive (LTENegSucc x) (LTENegSucc y) = LTENegSucc (ltezzTransitive x y)

反对称性:

||| `LTEZZ` is antisymmetric.
ltezzAntisymmetric : a `LTEZZ` b -> b `LTEZZ` a -> a = b
ltezzAntisymmetric LTEZero LTEZero = Refl
ltezzAntisymmetric (LTEPosSucc x) (LTEPosSucc y) =
  rewrite (posInjective (ltezzAntisymmetric x y)) in Refl
ltezzAntisymmetric LTEMinusOne LTEMinusOne = Refl
ltezzAntisymmetric (LTENegSucc x) (LTENegSucc y) =
  rewrite (negSInjective (ltezzAntisymmetric x y)) in Refl

总数:

||| `LTEZZ` is total.
ltezzTotal : (a : ZZ) -> (b : ZZ) -> Either (LTEZZ a b) (LTEZZ b a)
ltezzTotal (Pos k) (Pos j) with (order {to=LTE} k j)
  ltezzTotal (Pos k) (Pos j) | (Left pf) = Left $ lteLtezzPos pf
  ltezzTotal (Pos k) (Pos j) | (Right pf) = Right $ lteLtezzPos pf
ltezzTotal (Pos k) (NegS j) = Right LTENegPos
ltezzTotal (NegS k) (Pos j) = Left LTENegPos
ltezzTotal (NegS k) (NegS j) with (order {to=LTE} k j)
  ltezzTotal (NegS k) (NegS j) | (Left pf) = Right $ lteLtezzNegS pf
  ltezzTotal (NegS k) (NegS j) | (Right pf) = Left $ lteLtezzNegS pf