LTE pour les nombres entiers (ZZ)

Question

Je suis (pour le plaisir ?) en train d'essayer de travailler à travers toutes les Comment le prouver à Idris. L'une des propriétés dont j'aurai besoin est l'ordre total sur les entiers. Idris possède déjà la propriété données.ZZ module fournissant des entiers basés sur l'inductivité. J'ai besoin d'ajouter un type similaire à celui de Nat. LTE . Je n'arrive pas à me convaincre que ma mise en œuvre est correcte (ou que la LTE est correcte, d'ailleurs). Comment puis-je "vérifier" que le LTEZZ Le type de données sur lequel je travaille fonctionne ? Comment puis-je vérifier que (LTE 4 3) est invalide ?

Voici un exemple de code :

%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, LTE tourne Nat dans un ordre total comme vous pouvez le voir si vous suivez ce lien .

Mais LTEZZ ne fait pas ce qui est prévu. L'un des moyens de le vérifier est de prouver les propriétés d'une commande totale en utilisant la définition. Mais pour LTEZZ en l'état, vous ne pourrez pas, par exemple, prouver la réflexivité.

Voici une façon d'y remédier :

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 a fixé le LTENegSucc cas (vous voulez faire des arguments structurellement plus petit à chaque étape récursive, tout comme pour le programme LTEPosSucc ).

Importations et quelques 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