LTE pour entiers (ZZ)

Question

Je suis (pour le plaisir?) Essayant de travailler à travers tous Comment le prouver dans Idris. Une des propriétés dont j'ai besoin est l'ordre total sur les entiers. Idris a déjà le module data.ZZ fournissant des nombres entiers inductifs. Je dois ajouter un type similaire à LTE de Nat. Je n'arrive pas à me convaincre que ma mise en œuvre est correcte (ou que LTE est correcte d'ailleurs). Comment puis-je "vérifier" que le type de données LTEZZ sur lequel je travaille fonctionne? Comment puis-je vérifier que (LTE 4 3) est invalide?

code exemple suivant:

%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

Tout d'abord, se LTENat s dans un ordre total que vous pouvez voir si vous suivez this link. Mais LTEZZ ne fait pas ce qui est prévu. Une des façons de le vérifier est de prouver les propriétés d'un total order en utilisant la définition. Mais pour LTEZZ comme il est vous ne serez pas en mesure, par exemple. prouver la réflexivité.

Voici une façon de le fixer:

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

J'ai ajouté le cas pour -1 et fixé le cas LTENegSucc (vous voulez des arguments structurellement plus petites à chaque étape récursive, tout comme pour LTEPosSucc) .

importations et un couple de lemmes d'aide:

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) 

réflexivité:

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

transitivité:

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

antisymétrie:

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

Totalité:

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