LTE for Integers (ZZ)

Question

I am (for fun?) trying to work through all of How To Prove It in Idris. One of the properties I will require is total ordering on the integers. Idris already has the data.ZZ module providing inductively based integers. I need to add a type similar to Nat's LTE. I can't seem to convince myself that my implementation is correct (or that LTE is correct for that matter). How do I "check" that the LTEZZ data type I'm working on works? How do I check that (LTE 4 3) is invalid?

Example code follows:

%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

First of all, LTE turns Nats into a total order as you can see if you follow this link.

But LTEZZ does not do what is intended. One of the ways to check it is to prove the properties of a total order using the definition. But for LTEZZ as it is you won't be able e.g. to prove reflexivity.

Here is one way of fixing it:

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))

I added the case for -1 and fixed the LTENegSucc case (you want to make arguments structurally smaller at every recursive step, just like for LTEPosSucc).

Imports and a couple of helper lemmas:

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)

Reflexivity:

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

Transitivity:

||| `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)

Antisymmetry:

||| `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

Totality:

||| `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