Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module Order
%access public export
%default total
ltLte : m `LT` n -> m `LTE` n
ltLte (LTESucc x) = lteSuccRight x
ltLteTransitive : m `LT` n -> n `LTE` p -> m `LT` p
ltLteTransitive (LTESucc x) (LTESucc y) = LTESucc $ lteTransitive x y
plusLtMonoLeft : (p:Nat) -> m `LT` n -> p + m `LT` p + n
plusLtMonoLeft Z ltmn = ltmn
plusLtMonoLeft (S p) ltmn = LTESucc (plusLtMonoLeft p ltmn)
plusLteMonoLeft : (p:Nat) -> m `LTE` n -> p + m `LTE` p + n
plusLteMonoLeft Z x = x
plusLteMonoLeft (S k) x = LTESucc (plusLteMonoLeft k x)
plusLtMonoRight : (p:Nat) -> m `LT` n -> m + p `LT` n + p
plusLtMonoRight {m=m} {n=n} p ltmn =
rewrite plusCommutative m p in
rewrite plusCommutative n p in
plusLtMonoLeft p ltmn
plusLtLteMono : m `LT` n -> p `LTE` q -> m + p `LT` n + q
plusLtLteMono {n} {p} ltmn ltepq =
let prf = plusLtMonoRight p ltmn in
let prf' = plusLteMonoLeft n ltepq in
ltLteTransitive prf prf'
plusLtMono : m `LT` n -> p `LT` q -> m + p `LT` n + q
plusLtMono ltmn ltpq = plusLtLteMono ltmn (ltLte ltpq)
multLtMonoLeft : 0 `LT` p -> m `LT` n -> p * m `LT` p * n
multLtMonoLeft {p = S Z} {m} _ ltmn@(LTESucc {right = r} y) =
rewrite multOneLeftNeutral m in
rewrite multOneLeftNeutral r in
ltmn
multLtMonoLeft {p = S (S p)} _ ltmn =
let IH = multLtMonoLeft {p = S p} (LTESucc LTEZero) ltmn in
plusLtMono ltmn IH
multLtSelfRight : (k : Nat) -> 0 `LT` m -> 1 `LT` k -> m `LT` m * k
multLtSelfRight {m} k zeroLtM oneLtK =
let prf = multLtMonoLeft zeroLtM oneLtK in
replace {P = \x => Nat.LT x (m*k)} (multOneRightNeutral m) prf
multLtNonZeroArgumentsLeft : 0 `LT` m * n -> 0 `LT` m
multLtNonZeroArgumentsLeft {m = Z} x = absurd x
multLtNonZeroArgumentsLeft {m = (S k)} x = LTESucc LTEZero
multLtNonZeroArgumentsRight : 0 `LT` m * n -> 0 `LT` n
multLtNonZeroArgumentsRight {n = Z} {m} x = replace (multZeroRightZero m) x
multLtNonZeroArgumentsRight {n = (S k)} x = LTESucc LTEZero
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment