整数 LTE (ZZ)

Question

我（为了好玩？）尝试在 Idris 中完成所有如何证明它。我需要的属性之一是整数的总排序。伊德里斯已经拥有 data.ZZ module providing inductively based integers. I need to add a type similar to Nat's LTE。我似乎无法说服自己我的实施是正确的（或者 LTE 就此而言是正确的）。我如何 "check" 使我正在处理的 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把Nats变成了一个总的顺序，你跟着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

整数 LTE (ZZ)

LTE for Integers (ZZ)

idris