整数LTE (ZZ)

Question

我是(为了好玩？)试着研究如何在伊德里斯证明这一点。我需要的属性之一是整数的全序。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转换为一个完整的顺序，如果您遵循此链接，您可以看到。

但是LTEZZ并没有做我们想做的事情。检查它的方法之一是使用定义证明总订货的属性。但是对于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