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
First of all,
LTE
turnsNat
s 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 forLTEZZ
as it is you won't be able e.g. to prove reflexivity.Here is one way of fixing it:
I added the case for
-1
and fixed theLTENegSucc
case (you want to make arguments structurally smaller at every recursive step, just like forLTEPosSucc
).Imports and a couple of helper lemmas:
Reflexivity:
Transitivity:
Antisymmetry:
Totality: