LTE整數（ZZ）

我是（爲了好玩嗎？）試圖通過所有如何證明它在伊德里斯工作。我將要求的其中一個屬性是整數的總排序。伊德里斯已經有了提供基於感應的整數的模塊data.ZZ。我需要添加一個類似於Nat的LTE的類型。我似乎無法說服我自己，我的實施是正確的（或者說LTE是正確的）。如何「檢查」我正在處理的LTEZZ數據類型是否有效？如何檢查(LTE 4 3)無效？LTE整數（ZZ）

示例代碼如下：

所有的

%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

來源

2017-09-06 rfliam

首先，LTE變成Nat s轉換爲全序，你可以看到，如果你遵循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

來源

2017-09-06 14:34:27

回答

相關問題